From 8d3c142ec750612b7d02777ff2d6fd5286fb683d Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 28 Apr 2014 09:41:41 +0200
Subject: 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.
---
tools/coqdoc/cpretty.mll | 20 ++++++++++----------
tools/coqdoc/output.ml | 29 ++++++++++++++++++++++++++---
tools/coqdoc/output.mli | 3 ++-
3 files changed, 38 insertions(+), 14 deletions(-)
(limited to 'tools')
diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll
index d1cb0d3d8f..b4328d7001 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 6582b8c704..6f853926fe 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 "%s" (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 "%s" (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 80f3901100..e7fc6a029b 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
--
cgit v1.2.3