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.

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