Function agda_tree::extract::extract_agda_code

pub fn extract_agda_code<P>(filename: P) -> Result<(Tree, Vec<String>)>
where
    P: AsRef<Path>,

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.