1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52

//! The program here extract agda code from `*.agda.tree`
use std::fs::File;
use std::io::{self, BufRead};
use std::path::Path;

use crate::tree::Tree;

/// The function do is
///
/// - if match `\agda{`, then open recorder
/// - if match `}`, then close the recorder
/// - if recorder is on, then push the content
///
/// so one must write `\agda{` and `}` without space and be single line, this might have problem but for now it's good enough.
pub fn extract_agda_code<P>(filename: P) -> io::Result<(Tree, Vec<String>)>
where
    P: AsRef<Path>,
{
    let lines_of_agda_tree = read_lines(filename)?;

    let mut recording = false;
    let mut buffer = String::new();
    let mut result = vec![];
    let mut tree = Tree::new();
    for line in lines_of_agda_tree {
        let line = line?;
        if line == "\\agda{" {
            recording = true;
            buffer.push_str("```agda\n");
        } else if line == "}" && recording {
            buffer.push_str("```");
            result.push(buffer);
            buffer = String::new();
            recording = false;
            tree.push_agda();
        } else if recording {
            buffer.push_str(line.as_str());
            buffer.push('\n');
        } else {
            tree.push(line);
        }
    }
    Ok((tree, result))
}

fn read_lines<P>(filename: P) -> io::Result<io::Lines<io::BufReader<File>>>
where
    P: AsRef<Path>,
{
    let file = File::open(filename)?;
    Ok(io::BufReader::new(file).lines())
}