diff options
Diffstat (limited to 'doc/removeproofs.mll')
-rw-r--r-- | doc/removeproofs.mll | 33 |
1 files changed, 33 insertions, 0 deletions
diff --git a/doc/removeproofs.mll b/doc/removeproofs.mll new file mode 100644 index 00000000..d4b24312 --- /dev/null +++ b/doc/removeproofs.mll @@ -0,0 +1,33 @@ +rule process inproof oc = parse + | "<span class=\"keyword\">Proof</span>" ' '* '.' + { process true oc lexbuf } + | "<span class=\"keyword\">" ("Qed" | "Defined") "</span>" ' '* '.' + { process false oc lexbuf } + | "<a class=\"idref\" href=\"" + [^ '"'] + '#' '"' [^ '\n' '>']* '"' '"' '>' + ([^ '<' '\n']+ as ident) + "</a>" + { if not inproof then output_string oc ident; + process inproof oc lexbuf } + | _ + { if not inproof then output_char oc (Lexing.lexeme_char lexbuf 0); + process inproof oc lexbuf } + | eof + { () } + +{ + +let process_file name = + let ic = open_in name in + Sys.remove name; + let oc = open_out name in + process false oc (Lexing.from_channel ic); + close_out oc; + close_in ic + +let _ = + for i = 1 to Array.length Sys.argv - 1 do + process_file Sys.argv.(i) + done +} + |