diff options
Diffstat (limited to 'doc')
-rw-r--r-- | doc/coq2html.css | 5 | ||||
-rw-r--r-- | doc/coq2html.mll | 32 |
2 files changed, 31 insertions, 6 deletions
diff --git a/doc/coq2html.css b/doc/coq2html.css index 0f6680e8..c5627bfb 100644 --- a/doc/coq2html.css +++ b/doc/coq2html.css @@ -7,6 +7,7 @@ div.proofscript contents of proof script span.docright contents of (**r *) comments span.bracket contents of [ ] within comments + span.comment contents of (* *) comments span.kwd Coq keyword span.tactic Coq tactic span.id any other identifier @@ -86,6 +87,10 @@ span.kwd { color: #cf1d1d; } +span.comment { + color: #008000; +} + a:visited {color : #416DFF; text-decoration : none; } a:link {color : #416DFF; text-decoration : none; } a:hover {text-decoration : none; } 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" |