diff options
author | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-04-28 09:41:41 +0200 |
---|---|---|
committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-04-28 09:41:41 +0200 |
commit | 8d3c142ec750612b7d02777ff2d6fd5286fb683d (patch) | |
tree | 881b08216045c3b4088ccd2f094e0b401142880c | |
parent | 9eaf502657ae63f6b184d527eaf1c3b40be90a79 (diff) |
Fixing coqdoc bug #3292 (unfortunate collision betweens the relative
locations found when parsing expressions in comments and the absolute
locations in the glob file).
As now, the glob file does not parse comment, so I removed the test
for location when parsing expressions in comments, which anyway are
not linkable, precisely because not parsed by coqc.
-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 |