Revu removeproof

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@567 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

1 files changed, 33 insertions, 0 deletions

diff --git a/doc/removeproofs.mll b/doc/removeproofs.mll
new file mode 100644
index 0000000..d4b2431
--- /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
+}
+