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

5 files changed, 36 insertions, 8 deletions

diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml
index 519f902ba..702c509dc 100644
--- a/interp/dumpglob.ml
+++ b/interp/dumpglob.ml
@@ -212,6 +212,5 @@ let dump_notation_location posl df (((path,secpath),_),sc) =
     let secpath = Names.string_of_dirpath secpath in
     let df = cook_notation df sc in
     List.iter (fun (bl,el) ->
-      for pos=bl to el do
-	dump_string (Printf.sprintf "R%d %s %s %s not\n" pos path secpath df)
-      done) posl
+      dump_string(Printf.sprintf "R%d:%d %s %s %s not\n" bl el path secpath df))
+      posl
diff --git a/test-suite/complexity/lettuple.v b/test-suite/complexity/lettuple.v
index f97decf0a..0690459fc 100644
--- a/test-suite/complexity/lettuple.v
+++ b/test-suite/complexity/lettuple.v
@@ -26,4 +26,4 @@ Definition f (x : nat * nat) :=
   let (a,b) := x in
   0.
 
-Timeout 5 Print f.
+Timeout 5 Time Print f.
diff --git a/test-suite/coqdoc/links.v b/test-suite/coqdoc/links.v
index b09d64a9a..16028fe17 100644
--- a/test-suite/coqdoc/links.v
+++ b/test-suite/coqdoc/links.v
@@ -19,7 +19,9 @@ Notation "n ++ m" := (plus n m).
 
 Notation "n ++ m" := (mult n m). (* redefinition *)
 
-Notation "n % m" := (plus n m) (at level 60).
+Notation "n ** m" := (plus n m) (at level 60).
+
+Notation "n ▵ m" := (plus n m) (at level 60).
 
 Notation "n '_' ++ 'x' m" := (plus n m) (at level 3).
 
@@ -31,7 +33,7 @@ Definition eq0 := 0 = 0 :> nat.
 
 Notation "( x # y ; .. ; z )" := (pair .. (pair x y) .. z).
 
-Definition p := ((0#0;0) , (0 % 0)).
+Definition b_α := ((0#0;0) , (0 ** 0)).
 
 Notation h := a.
 
@@ -39,7 +41,7 @@ Notation h := a.
 
     Variables b' b2: nat.
 
-    Notation "n + m" := (plus n m) : my_scope.
+    Notation "n + m" := (n ▵ m) : my_scope.
 
     Delimit Scope my_scope with my.
 
diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll
index 779d10e99..af8bac2c1 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 434a8bf5b..889e5d6ff 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)