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

agda_tree/command/
build.rs
