diff options
Diffstat (limited to 'tools/coqdoc/cpretty.mll')
| -rw-r--r-- | tools/coqdoc/cpretty.mll | 71 |
1 files changed, 57 insertions, 14 deletions
diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll index 925f5258..d7b54fd0 100644 --- a/tools/coqdoc/cpretty.mll +++ b/tools/coqdoc/cpretty.mll @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -77,8 +77,17 @@ let in_proof = ref None let in_emph = ref false - let start_emph () = in_emph := true; Output.start_emph () - let stop_emph () = if !in_emph then (Output.stop_emph (); in_emph := false) + let in_env start stop = + let r = ref false in + let start_env () = r := true; start () in + let stop_env () = if !r then stop (); r := false in + (fun x -> !r), start_env, stop_env + + let in_emph, start_emph, stop_emph = in_env Output.start_emph Output.stop_emph + let in_quote, start_quote, stop_quote = in_env Output.start_quote Output.stop_quote + + let url_buffer = Buffer.create 40 + let url_name_buffer = Buffer.create 40 let backtrack lexbuf = lexbuf.lex_curr_pos <- lexbuf.lex_start_pos; lexbuf.lex_curr_p <- lexbuf.lex_start_p @@ -254,7 +263,7 @@ let nbsp,isp = count_spaces s in Output.indentation nbsp; let s = String.sub s isp (String.length s - isp) in - Output.ident s (lexeme_start lexbuf + isp) + Output.keyword s (lexeme_start lexbuf + isp) } @@ -369,13 +378,17 @@ let commands = | "Drop" | "ProtectedLoop" | "Quit" + | "Restart" | "Load" | "Add" | "Remove" space+ "Loadpath" | "Print" | "Inspect" | "About" + | "SearchAbout" + | "SearchRewrite" | "Search" + | "Locate" | "Eval" | "Reset" | "Check" @@ -403,6 +416,14 @@ let prog_kw = | "Obligations" | "Solve" +let hint_kw = + "Extern" | "Rewrite" | "Resolve" | "Immediate" | "Transparent" | "Opaque" | "Unfold" | "Constructors" + +let set_kw = + "Printing" space+ ("Coercions" | "Universes" | "All") + | "Implicit" space+ "Arguments" + + let gallina_kw_to_hide = "Implicit" space+ "Arguments" | "Ltac" @@ -410,15 +431,16 @@ let gallina_kw_to_hide = | "Import" | "Export" | "Load" - | "Hint" + | "Hint" space+ hint_kw | "Open" | "Close" | "Delimit" | "Transparent" | "Opaque" | ("Declare" space+ ("Morphism" | "Step") ) - | ("Set" | "Unset") space+ "Printing" space+ "Coercions" + | ("Set" | "Unset") space+ set_kw | "Declare" space+ ("Left" | "Right") space+ "Step" + | "Debug" space+ ("On" | "Off") let section = "*" | "**" | "***" | "****" @@ -689,7 +711,7 @@ and doc_bol = parse | space* nl+ { Output.paragraph (); doc_bol lexbuf } | "<<" space* - { Output.start_verbatim (); verbatim lexbuf; doc_bol lexbuf } + { Output.start_verbatim false; verbatim false lexbuf; doc_bol lexbuf } | eof { true } | '_' @@ -713,8 +735,8 @@ and doc_list_bol indents = parse backtrack lexbuf; doc_bol lexbuf } | "<<" space* - { Output.start_verbatim (); - verbatim lexbuf; + { Output.start_verbatim false; + verbatim false lexbuf; doc_list_bol indents lexbuf } | "[[" nl { formatted := true; @@ -813,6 +835,7 @@ and doc indents = parse { inf_rules indents lexbuf } | "[]" { Output.proofbox (); doc indents lexbuf } + | "{{" { url lexbuf; doc indents lexbuf } | "[" { if !Cdglobals.plain_comments then Output.char '[' else (brackets := 1; Output.start_inline_coq (); escaped_coq lexbuf; @@ -872,6 +895,15 @@ and doc indents = parse { if !Cdglobals.plain_comments then Output.char '_' else stop_emph () ; Output.char (lexeme_char lexbuf 1); doc indents lexbuf } + | "<<" space* + { Output.start_verbatim true; verbatim true lexbuf; doc_bol lexbuf } + | '"' + { if !Cdglobals.plain_comments + then Output.char '"' + else if in_quote () + then stop_quote () + else start_quote (); + doc indents lexbuf } | eof { false } | _ @@ -898,11 +930,22 @@ and escaped_html = parse | eof { () } | _ { Output.html_char (lexeme_char lexbuf 0); escaped_html lexbuf } -and verbatim = parse - | nl ">>" space* nl { Output.verbatim_char '\n'; Output.stop_verbatim () } - | nl ">>" { Output.verbatim_char '\n'; Output.stop_verbatim () } - | eof { Output.stop_verbatim () } - | _ { Output.verbatim_char (lexeme_char lexbuf 0); verbatim lexbuf } +and verbatim inline = parse + | nl ">>" space* nl { Output.verbatim_char inline '\n'; Output.stop_verbatim inline } + | nl ">>" { Output.verbatim_char inline '\n'; Output.stop_verbatim inline } + | ">>" { Output.stop_verbatim inline } + | eof { Output.stop_verbatim inline } + | _ { Output.verbatim_char inline (lexeme_char lexbuf 0); verbatim inline lexbuf } + +and url = parse + | "}}" { Output.url (Buffer.contents url_buffer) None; Buffer.clear url_buffer } + | "}" { url_name lexbuf } + | _ { Buffer.add_char url_buffer (lexeme_char lexbuf 0); url lexbuf } + +and url_name = parse + | "}" { Output.url (Buffer.contents url_buffer) (Some (Buffer.contents url_name_buffer)); + Buffer.clear url_buffer; Buffer.clear url_name_buffer } + | _ { Buffer.add_char url_name_buffer (lexeme_char lexbuf 0); url_name lexbuf } (*s Coq, inside quotations *) |