Small things about coqdoc + fixing lettuple.v test (part of bug #2289)

In coqdoc, made links to utf8 notations working and made
representation of locations for notations more compact

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12896 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 28 insertions, 1 deletions

diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll
index 779d10e99d..af8bac2c10 100644
--- a/tools/coqdoc/cpretty.mll
+++ b/tools/coqdoc/cpretty.mll
@@ -284,6 +284,11 @@ let pfx_id = (id '.')*
 let identifier =
   id | pfx_id id
 
+let utf8_multibyte =
+   [ '\xC0'-'\xDF' ] _
+ | [ '\xE0'-'\xEF' ] _ _
+ | [ '\xF0'-'\xF7' ] _ _ _
+
 (* This misses unicode stuff, and it adds "[" and "]".  It's only an
    approximation of idents - used for detecting whether an underscore
    is part of an identifier or meant to indicate emphasis *)
@@ -1067,6 +1072,16 @@ and body = parse
   | ".."
       { Output.char '.'; Output.char '.';
         body lexbuf }
+  | '"' 
+      { Output.char '"'; 
+        string lexbuf;
+        body lexbuf }
+
+  | utf8_multibyte
+      { let c = lexeme lexbuf in
+	symbol lexbuf c;
+        body lexbuf }
+
   | _ { let c = lexeme_char lexbuf 0 in
 	  Output.char c;
           body lexbuf }
@@ -1093,6 +1108,11 @@ and notation_string = parse
         Output.char c;
         notation_string lexbuf }
 
+and string = parse
+  | "\"\"" { Output.char '"'; Output.char '"'; string lexbuf }
+  | '"'    { Output.char '"' }
+  | _      { let c = lexeme_char lexbuf 0 in Output.char c; string lexbuf }
+
 and skip_hide = parse
   | eof | end_hide { () }
   | _ { skip_hide lexbuf }
diff --git a/tools/coqdoc/index.ml b/tools/coqdoc/index.ml
index 434a8bf5b5..889e5d6ff9 100644
--- a/tools/coqdoc/index.ml
+++ b/tools/coqdoc/index.ml
@@ -314,10 +314,17 @@ let read_glob f =
 	      current_library := !cur_mod
 	  | 'R' ->
 	      (try
+		Scanf.sscanf s "R%d:%d %s %s %s %s"
+		  (fun loc1 loc2 lib_dp sp id ty ->
+		    for loc=loc1 to loc2 do
+		      add_ref !cur_mod loc lib_dp sp id (type_of_string ty)
+		    done)
+	       with _ ->
+	       try
 		Scanf.sscanf s "R%d %s %s %s %s"
 		  (fun loc lib_dp sp id ty ->
 		    add_ref !cur_mod loc lib_dp sp id (type_of_string ty))
-	      with _ -> ())
+	       with _ -> ())
 	  | _ ->
 	      try Scanf.sscanf s "%s %d %s %s"
 		(fun ty loc sp id -> add_def loc (type_of_string ty) sp id)