agda_tree/
extract.rs

1//! The program here extract agda code from `*.agda.tree`
2use std::fs::File;
3use std::io::{self, BufRead};
4use std::path::Path;
5
6use crate::tree::Tree;
7
8/// The function do is
9///
10/// - if match `\agda{`, then open recorder
11/// - if match `}`, then close the recorder
12/// - if recorder is on, then push the content
13///
14/// so one must write `\agda{` and `}` without space and be single line, this might have problem but for now it's good enough.
15pub(crate) fn extract_agda_code<P>(filename: P) -> io::Result<(Tree, Vec<String>)>
16where
17    P: AsRef<Path>,
18{
19    let lines_of_agda_tree = read_lines(filename)?;
20
21    let mut recording = false;
22    let mut buffer = String::new();
23    let mut result = vec![];
24    let mut tree = Tree::new();
25    for line in lines_of_agda_tree {
26        let line = line?;
27        if line == "\\agda{" {
28            recording = true;
29            buffer.push_str("```agda\n");
30        } else if line == "}" && recording {
31            // remember, we must insert these `---` text, to ensure closed
32            //     ```
33            //     ```agda
34            // will not be treated as same HTML node
35            buffer.push_str("```\n---\n");
36            result.push(buffer);
37            buffer = String::new();
38            recording = false;
39            tree.push_agda();
40        } else if recording {
41            buffer.push_str(line.as_str());
42            buffer.push('\n');
43        } else {
44            tree.push(line);
45        }
46    }
47    Ok((tree, result))
48}
49
50fn read_lines<P>(filename: P) -> io::Result<io::Lines<io::BufReader<File>>>
51where
52    P: AsRef<Path>,
53{
54    let file = File::open(filename)?;
55    Ok(io::BufReader::new(file).lines())
56}
agda_tree/extract.rs

agda_tree/
extract.rs
