diff options
author | Xavier Leroy <xavier.leroy@inria.fr> | 2015-06-11 16:19:06 +0200 |
---|---|---|
committer | Xavier Leroy <xavier.leroy@inria.fr> | 2015-06-11 16:19:06 +0200 |
commit | 9622c474fd1b51ed7cf29eb7c5ecff5279ac1c73 (patch) | |
tree | c0142107cdb0f6fbf7d72f3239adc44f99cc66f4 /doc/coq2html.mll | |
parent | a3d4f94f470f1ad1b9406c67589c9ebc44c94113 (diff) | |
download | compcert-9622c474fd1b51ed7cf29eb7c5ecff5279ac1c73.tar.gz compcert-9622c474fd1b51ed7cf29eb7c5ecff5279ac1c73.zip |
Preserve ordinary comments within proof scripts.
Diffstat (limited to 'doc/coq2html.mll')
-rw-r--r-- | doc/coq2html.mll | 32 |
1 files changed, 26 insertions, 6 deletions
diff --git a/doc/coq2html.mll b/doc/coq2html.mll index 329e9eaa..2f1bfdbc 100644 --- a/doc/coq2html.mll +++ b/doc/coq2html.mll @@ -206,15 +206,23 @@ let start_verbatim () = let end_verbatim () = fprintf !oc "</pre>\n" +let start_comment () = + fprintf !oc "<span class=\"comment\">(*" + +let end_comment () = + fprintf !oc "*)</span>" + let start_bracket () = fprintf !oc "<span class=\"bracket\">" let end_bracket () = fprintf !oc "</span>" +let in_proof = ref false let proof_counter = ref 0 let start_proof kwd = + in_proof := true; incr proof_counter; fprintf !oc "<div class=\"toggleproof\" onclick=\"toggleDisplay('proof%d')\">%s</div>\n" @@ -222,7 +230,8 @@ let start_proof kwd = fprintf !oc "<div class=\"proofscript\" id=\"proof%d\">\n" !proof_counter let end_proof kwd = - fprintf !oc "%s</div>\n" kwd + fprintf !oc "%s</div>\n" kwd; + in_proof := false let start_html_page modname = fprintf !oc "\ @@ -300,7 +309,8 @@ and coq = parse end_doc_right(); coq lexbuf } | "(*" - { comment lexbuf; + { if !in_proof then start_comment(); + comment lexbuf; coq lexbuf } | path as id { ident (Lexing.lexeme_start lexbuf) id; coq lexbuf } @@ -325,13 +335,23 @@ and bracket = parse and comment = parse | "*)" - { () } + { if !in_proof then end_comment() } | "(*" - { comment lexbuf; comment lexbuf } + { if !in_proof then start_comment(); + comment lexbuf; comment lexbuf } | eof { () } - | _ - { comment lexbuf } + | "\n" + { if !in_proof then newline(); + comment lexbuf } + | space* as s + { if !in_proof then space s; + comment lexbuf } + | eof + { () } + | _ as c + { if !in_proof then character c; + comment lexbuf } and doc_bol = parse | "<<" space* "\n" |