From 68881dcdf8be4c4ee8368574cf20cd2a38d383f9 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Wed, 19 Mar 2008 09:53:21 +0000
Subject: Revu removeproof

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@567 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 doc/removeproofs.mll | 33 +++++++++++++++++++++++++++++++++
 1 file changed, 33 insertions(+)
 create mode 100644 doc/removeproofs.mll

(limited to 'doc/removeproofs.mll')

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
+}
+
-- 
cgit