diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2010-03-09 15:13:00 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2010-03-09 15:13:00 +0000 |
commit | 261103b5bfd89335d028bf800af3f0a1ab1b70e5 (patch) | |
tree | 8777745c993ce221a859763328ef2106390d867c /doc/removeproofs.mll | |
parent | a24cfb086163ab359735392340acfe03e133be64 (diff) | |
download | compcert-261103b5bfd89335d028bf800af3f0a1ab1b70e5.tar.gz compcert-261103b5bfd89335d028bf800af3f0a1ab1b70e5.zip |
New HTML documentation generator
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1286 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'doc/removeproofs.mll')
-rw-r--r-- | doc/removeproofs.mll | 35 |
1 files changed, 0 insertions, 35 deletions
diff --git a/doc/removeproofs.mll b/doc/removeproofs.mll deleted file mode 100644 index 7fb37bb0..00000000 --- a/doc/removeproofs.mll +++ /dev/null @@ -1,35 +0,0 @@ -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 -} - |