diff options
Diffstat (limited to 'tools/coqdoc')
| -rw-r--r-- | tools/coqdoc/cpretty.mll | 20 | ||||
| -rw-r--r-- | tools/coqdoc/output.ml | 29 | ||||
| -rw-r--r-- | tools/coqdoc/output.mli | 3 |
3 files changed, 38 insertions, 14 deletions
diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll index d1cb0d3d8..b4328d700 100644 --- a/tools/coqdoc/cpretty.mll +++ b/tools/coqdoc/cpretty.mll @@ -606,7 +606,7 @@ and coq = parse end else begin - Output.ident s (lexeme_start lexbuf); + Output.ident s None; let eol=body lexbuf in if eol then coq_bol lexbuf else coq lexbuf end } @@ -636,17 +636,17 @@ and coq = parse if eol then coq_bol lexbuf else coq lexbuf } | gallina_kw { let s = lexeme lexbuf in - Output.ident s (lexeme_start lexbuf); + Output.ident s None; let eol = body lexbuf in if eol then coq_bol lexbuf else coq lexbuf } | notation_kw { let s = lexeme lexbuf in - Output.ident s (lexeme_start lexbuf); + Output.ident s None; let eol= start_notation_string lexbuf in if eol then coq_bol lexbuf else coq lexbuf } | prog_kw { let s = lexeme lexbuf in - Output.ident s (lexeme_start lexbuf); + Output.ident s None; let eol = body lexbuf in if eol then coq_bol lexbuf else coq lexbuf } | space+ { Output.char ' '; coq lexbuf } @@ -934,11 +934,11 @@ and escaped_coq = parse | "]" { decr brackets; if !brackets > 0 then - (Output.sublexer ']' (lexeme_start lexbuf); escaped_coq lexbuf) + (Output.sublexer_in_doc ']'; escaped_coq lexbuf) else Tokens.flush_sublexer () } | "[" { incr brackets; - Output.sublexer '[' (lexeme_start lexbuf); escaped_coq lexbuf } + Output.sublexer_in_doc '['; escaped_coq lexbuf } | "(*" { Tokens.flush_sublexer (); comment_level := 1; ignore (comment lexbuf); escaped_coq lexbuf } @@ -948,7 +948,7 @@ and escaped_coq = parse { Tokens.flush_sublexer () } | (identifier '.')* identifier { Tokens.flush_sublexer(); - Output.ident (lexeme lexbuf) (lexeme_start lexbuf); + Output.ident (lexeme lexbuf) None; escaped_coq lexbuf } | space_nl* { let str = lexeme lexbuf in @@ -960,7 +960,7 @@ and escaped_coq = parse else Output.start_inline_coq ()); escaped_coq lexbuf } | _ - { Output.sublexer (lexeme_char lexbuf 0) (lexeme_start lexbuf); + { Output.sublexer_in_doc (lexeme_char lexbuf 0); escaped_coq lexbuf } (*s Coq "Comments" command. *) @@ -1128,11 +1128,11 @@ and body = parse else body lexbuf } | "where" { Tokens.flush_sublexer(); - Output.ident (lexeme lexbuf) (lexeme_start lexbuf); + Output.ident (lexeme lexbuf) None; start_notation_string lexbuf } | identifier { Tokens.flush_sublexer(); - Output.ident (lexeme lexbuf) (lexeme_start lexbuf); + Output.ident (lexeme lexbuf) (Some (lexeme_start lexbuf)); body lexbuf } | ".." { Tokens.flush_sublexer(); Output.char '.'; Output.char '.'; diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml index 6582b8c70..6f853926f 100644 --- a/tools/coqdoc/output.ml +++ b/tools/coqdoc/output.ml @@ -383,6 +383,14 @@ module Latex = struct end; last_was_in := false + let sublexer_in_doc c = + if c = '*' && !last_was_in then begin + Tokens.flush_sublexer (); + output_char '*' + end else + Tokens.output_tagged_symbol_char None c; + last_was_in := false + let initialize () = initialize_tex_html (); Tokens.token_tree := token_tree_latex; @@ -399,8 +407,11 @@ module Latex = struct let ident s loc = last_was_in := s = "in"; try - let tag = Index.find (get_module false) loc in - reference (translate s) tag + match loc with + | None -> raise Not_found + | Some loc -> + let tag = Index.find (get_module false) loc in + reference (translate s) tag with Not_found -> if is_tactic s then printf "\\coqdoctac{%s}" (translate s) @@ -646,6 +657,9 @@ module Html = struct in Tokens.output_tagged_symbol_char tag c + let sublexer_in_doc c = + Tokens.output_tagged_symbol_char None c + let initialize () = initialize_tex_html(); Tokens.token_tree := token_tree_html; @@ -661,7 +675,11 @@ module Html = struct if is_keyword s then begin printf "<span class=\"id\" type=\"keyword\">%s</span>" (translate s) end else begin - try reference (translate s) (Index.find (get_module false) loc) + try + match loc with + | None -> raise Not_found + | Some loc -> + reference (translate s) (Index.find (get_module false) loc) with Not_found -> if is_tactic s then printf "<span class=\"id\" type=\"tactic\">%s</span>" (translate s) @@ -985,6 +1003,9 @@ module TeXmacs = struct let sublexer c l = if !in_doc then Tokens.output_tagged_symbol_char None c else char c + let sublexer_in_doc c = + char c + let initialize () = Tokens.token_tree := token_tree_texmacs; Tokens.outfun := output_sublexer_string @@ -1107,6 +1128,7 @@ module Raw = struct let ident s loc = raw_ident s let sublexer c l = char c + let sublexer_in_doc c = char c let initialize () = Tokens.token_tree := ref Tokens.empty_ttree; @@ -1220,6 +1242,7 @@ let char = select Latex.char Html.char TeXmacs.char Raw.char let keyword = select Latex.keyword Html.keyword TeXmacs.keyword Raw.keyword let ident = select Latex.ident Html.ident TeXmacs.ident Raw.ident let sublexer = select Latex.sublexer Html.sublexer TeXmacs.sublexer Raw.sublexer +let sublexer_in_doc = select Latex.sublexer_in_doc Html.sublexer_in_doc TeXmacs.sublexer_in_doc Raw.sublexer_in_doc let initialize = select Latex.initialize Html.initialize TeXmacs.initialize Raw.initialize let proofbox = select Latex.proofbox Html.proofbox TeXmacs.proofbox Raw.proofbox diff --git a/tools/coqdoc/output.mli b/tools/coqdoc/output.mli index 80f390110..e7fc6a029 100644 --- a/tools/coqdoc/output.mli +++ b/tools/coqdoc/output.mli @@ -61,8 +61,9 @@ val rule : unit -> unit val nbsp : unit -> unit val char : char -> unit val keyword : string -> loc -> unit -val ident : string -> loc -> unit +val ident : string -> loc option -> unit val sublexer : char -> loc -> unit +val sublexer_in_doc : char -> unit val initialize : unit -> unit val proofbox : unit -> unit |