agda_tree/
tree.rs

1use std::io::Write;
2use std::{collections::VecDeque, fs::File};
3use Line::{AgdaBlock, Content};
4
5pub(crate) enum Line {
6    AgdaBlock,
7    Content(String),
8}
9
10pub(crate) struct Tree {
11    lines: Vec<Line>,
12}
13
14impl Tree {
15    pub(crate) fn new() -> Tree {
16        Tree { lines: vec![] }
17    }
18
19    pub(crate) fn push(&mut self, content: String) {
20        self.lines.push(Line::Content(content));
21    }
22    pub(crate) fn push_agda(&mut self) {
23        self.lines.push(Line::AgdaBlock);
24    }
25
26    pub fn merge(&self, mut agda_blocks: VecDeque<String>) -> Tree {
27        let mut new_tree = Tree::new();
28        for l in &self.lines {
29            match l {
30                Content(s) => new_tree.push(s.clone()),
31                AgdaBlock => {
32                    let k = agda_blocks.pop_front().expect("agda blocks is not enough");
33                    new_tree.push(k);
34                }
35            }
36        }
37        new_tree
38    }
39
40    pub fn write(&self, mut output: File) {
41        output
42            .write("\\xmlns:html{http://www.w3.org/1999/xhtml}\n".as_bytes())
43            .unwrap();
44        for l in &self.lines {
45            match l {
46                Content(s) => {
47                    let mut content = s.clone();
48                    content.push('\n');
49                    let _ = output.write(content.as_bytes()).unwrap();
50                }
51                AgdaBlock => {}
52            }
53        }
54    }
55}
agda_tree/tree.rs

agda_tree/
tree.rs
