agda_tree/command/
build.rs

1use html_parser::{Dom, Element};
2use std::fs::{self, create_dir_all, File};
3use std::io::{self, Read, Write};
4use std::path::{Path, PathBuf};
5
6pub fn execute(working_dir: &PathBuf, output_dir: &PathBuf) -> io::Result<()> {
7    let agda_generate_trees = fs::read_dir(working_dir.join("html"))?
8        .filter_map(Result::ok)
9        .filter_map(|f| {
10            if let Ok(ft) = f.file_type() {
11                if ft.is_file() && f.path().to_str()?.ends_with(".tree") {
12                    return Some(f.path());
13                }
14            }
15            None
16        })
17        .collect::<Vec<PathBuf>>();
18
19    create_dir_all(output_dir)?;
20
21    for tree_path in agda_generate_trees {
22        let new_content = postprocess(working_dir, tree_path.clone())?;
23
24        let created_path = output_dir
25            .join(tree_path.file_stem().unwrap())
26            .with_extension("tree");
27        println!("Producing {:?}", created_path);
28        let mut out_file = File::create(created_path)?;
29        out_file.write_all(new_content.as_bytes())?;
30    }
31
32    Ok(())
33}
34
35fn postprocess(working_dir: &PathBuf, tree_path: PathBuf) -> io::Result<String> {
36    println!("Processing file: {:?}", tree_path);
37
38    let mut file = File::open(tree_path.clone())?;
39    let mut content = String::new();
40    file.read_to_string(&mut content)?;
41
42    let mut new_content = String::new();
43    let mut html = String::new();
44
45    let mut recording = false;
46    let mut line: usize = 0;
47    let mut last_col_end: usize = 0;
48
49
50    new_content.push_str("\\xmlns:html{http://www.w3.org/1999/xhtml}");
51
52    for cur_line in content.lines() {
53        if cur_line.contains("<pre class=\"Agda\">") {
54            new_content.push_str("\\<html:pre>[class]{Agda}{");
55            recording = true;
56        } else if cur_line.contains("</pre>") {
57            recording = false;
58            let dom = Dom::parse(html.as_str()).unwrap();
59            html.clear();
60
61            for node in dom.children {
62                let elem = node.element().unwrap();
63
64                if line_of_symbol(elem) > line {
65                    for _ in 0..(line_of_symbol(elem) - line) {
66                        new_content.push('\n');
67                    }
68                    last_col_end = 1;
69                }
70                if col_of_symbol(elem) > last_col_end {
71                    for _ in 0..col_of_symbol(elem) - last_col_end {
72                        new_content.push(' ');
73                    }
74                }
75                last_col_end = end_col_of_symbol(elem);
76                line = line_of_symbol(elem);
77
78                new_content.push_str(symbol2forest(working_dir, elem).as_str());
79            }
80
81            new_content.push_str("}\n");
82        } else if recording {
83            html.push_str(cur_line);
84            html.push('\n');
85        } else {
86            new_content.push_str(cur_line);
87            new_content.push('\n');
88        }
89    }
90
91    Ok(new_content)
92}
93
94fn line_of_symbol(elem: &Element) -> usize {
95    elem.source_span.end_line
96}
97fn col_of_symbol(elem: &Element) -> usize {
98    elem.source_span.start_column
99}
100fn end_col_of_symbol(elem: &Element) -> usize {
101    elem.source_span.end_column
102}
103
104fn symbol2forest(working_dir: &PathBuf, elem: &Element) -> String {
105    let mut s = format!("\\<html:{}>", elem.name);
106
107    if elem.id.is_some() {
108        s.push_str(format!("[id]{{{}}}", elem.id.clone().unwrap().as_str()).as_str());
109    }
110    if !elem.classes.is_empty() {
111        s.push_str(format!("[class]{{{}}}", elem.classes[0]).as_str());
112    }
113    for (k, v) in &elem.attributes {
114        let value = v.clone().unwrap();
115        let value = if k == "href" {
116            // value is a xxx.html#id
117            // 1. split at `#`
118            // 2. if there is a `xxx.lagda.tree` in workding dir, replace the path with `xxx.xml`
119            // 3. put `#id` back if exists
120            let split = value.split_terminator('#').collect::<Vec<&str>>();
121            let a_link = split[0];
122            let path = Path::new(a_link);
123            if working_dir.join(path).with_extension("lagda.tree").exists() {
124                let mut s = path.with_extension("xml").to_str().unwrap().to_owned();
125                s.push('#');
126                if split.len() == 2 {
127                    let id_part = split[1];
128                    s.push_str(id_part);
129                }
130                s
131            } else {
132                value
133            }
134        } else {
135            value
136        };
137        s.push_str(format!("[{}]{{{}}}", k, value).as_str());
138    }
139    if elem.children.is_empty() {
140        s.push_str("{}");
141    } else {
142        let childtext = elem.children[0].text().unwrap();
143        // some escape code is useful for HTML, but not for forester
144        let childtext = if childtext.contains("&#39;") {
145            childtext.replace("&#39;", "'")
146        } else {
147            childtext.to_owned()
148        };
149        if childtext.contains('(')
150            || childtext.contains(')')
151            || childtext.contains('{')
152            || childtext.contains('}')
153        {
154            s.push_str(format!("{{\\startverb{}\\stopverb}}", childtext).as_str());
155        } else {
156            s.push_str(format!("{{{}}}", childtext).as_str());
157        }
158    }
159
160    s
161}
agda_tree/command/build.rs

agda_tree/command/
build.rs
