Autour du parsing:

- Utilisation de notations de type "abbreviation paramétrée" plutôt que
  de notations introduisant des mots-clés, là où c'est possible (cela affecte
  QDen, in_left/in_right, inhabited, S/P dans NZCyclic).
- Extension du lexeur pour qu'il prenne le plus long token valide au
  lieu d'échouer sur un plus long préfixe non valide de token (permet
  notamment de faire passer la notation de Georges "'C_ G ( A )"
  sans invalider toute séquence commençant par 'C et non suivie de _)
- Rajout d'un point final à certains messages d'erreur qui n'en avaient pas.
- Ajout String.copy dans string_of_label ("trou" de mutabilité signalé
  par Georges -- le "trou" lié aux vecteurs des noeuds App restant lui
  ouvert).



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

11 files changed, 60 insertions, 54 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index d2c2b0d6a..6fc65e9fb 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -50,7 +50,7 @@ let for_grammar f x =
 type internalisation_error =
   | VariableCapture of identifier
   | WrongExplicitImplicit
-  | NegativeMetavariable
+  | IllegalMetavariable
   | NotAConstructor of reference
   | UnboundFixName of bool * identifier
   | NonLinearPattern of identifier
@@ -66,8 +66,8 @@ let explain_wrong_explicit_implicit =
   str "Found an explicitly given implicit argument but was expecting" ++
   fnl () ++ str "a regular one"
 
-let explain_negative_metavariable =
-  str "Metavariable numbers must be positive"
+let explain_illegal_metavariable =
+  str "Metavariables allowed only in patterns"
 
 let explain_not_a_constructor ref =
   str "Unknown constructor: " ++ pr_reference ref
@@ -102,7 +102,7 @@ let explain_bad_explicitation_number n po =
 let explain_internalisation_error = function
   | VariableCapture id -> explain_variable_capture id
   | WrongExplicitImplicit -> explain_wrong_explicit_implicit
-  | NegativeMetavariable -> explain_negative_metavariable
+  | IllegalMetavariable -> explain_illegal_metavariable
   | NotAConstructor ref -> explain_not_a_constructor ref
   | UnboundFixName (iscofix,id) -> explain_unbound_fix_name iscofix id
   | NonLinearPattern id -> explain_non_linear_pattern id
@@ -940,7 +940,7 @@ let internalise sigma globalenv env allow_patvar lvar c =
     | CPatVar (loc, n) when allow_patvar ->
 	RPatVar (loc, n)
     | CPatVar (loc, _) ->
-	raise (InternalisationError (loc,NegativeMetavariable))
+	raise (InternalisationError (loc,IllegalMetavariable))
     | CEvar (loc, n, l) ->
 	REvar (loc, n, Option.map (List.map (intern env)) l)
     | CSort (loc, s) ->
@@ -1093,7 +1093,8 @@ let internalise sigma globalenv env allow_patvar lvar c =
     intern env c
   with
       InternalisationError (loc,e) ->
-	user_err_loc (loc,"internalize",explain_internalisation_error e)
+	user_err_loc (loc,"internalize",
+	  explain_internalisation_error e ++ str ".")
 
 (**************************************************************************)
 (* Functions to translate constr_expr into rawconstr                       *)
diff --git a/kernel/names.ml b/kernel/names.ml
index 3d80ad23e..0191880d1 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -103,7 +103,7 @@ let label_of_mbid (_,s,_) = s
 
 
 let mk_label l = l
-let string_of_label l = l
+let string_of_label = string_of_id
 
 let id_of_label l = l
 let label_of_id id = id
diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4
index b04ab971e..d7fa2b575 100644
--- a/parsing/lexer.ml4
+++ b/parsing/lexer.ml4
@@ -324,43 +324,49 @@ let rec comment bp = parser bp2
 (* Parse a special token, using the [token_tree] *)
 
 (* Peek as much utf-8 lexemes as possible *)
-(* then look if a special token is obtained *)
-let rec special tt cs =
-  match Stream.peek cs with
-    | Some c -> progress_from_byte 0 tt cs c
-    | None -> tt.node
-
-  (* nr is the number of char peeked; n the number of char in utf8 block *)
-and progress_utf8 nr n c tt cs =
+(* and retain the longest valid special token obtained *)
+let rec progress_further last nj tt cs =
+  try progress_from_byte last nj tt cs (List.nth (Stream.npeek (nj+1) cs) nj)
+  with Failure _ -> last
+
+and update_longest_valid_token last nj tt cs =
+  match tt.node with
+  | Some _ as last' ->
+      for i=1 to nj do Stream.junk cs done; 
+      progress_further last' 0 tt cs
+  | None ->
+      progress_further last nj tt cs
+
+(* nr is the number of char peeked since last valid token *)
+(* n the number of char in utf8 block *)
+and progress_utf8 last nj n c tt cs =
   try
     let tt = CharMap.find c tt.branch in
-    let tt =
-      if n=1 then tt else
-	match Stream.npeek (n-nr) cs with
-	| l when List.length l = n-nr ->
-	    let l = Util.list_skipn (1-nr) l in
-	    List.iter (check_utf8_trailing_byte cs) l;
-	    List.fold_left (fun tt c -> CharMap.find c tt.branch) tt l
-	| _ -> 
-	    error_utf8 cs
-    in
-    for i=1 to n-nr do Stream.junk cs done;
-    special tt cs
+    if n=1 then
+      update_longest_valid_token last (nj+n) tt cs
+    else
+      match Util.list_skipn (nj+1) (Stream.npeek (nj+n) cs) with
+      | l when List.length l = n-1 ->
+	 List.iter (check_utf8_trailing_byte cs) l;
+	 let tt = List.fold_left (fun tt c -> CharMap.find c tt.branch) tt l in
+	 update_longest_valid_token last (nj+n) tt cs
+      | _ -> 
+	  error_utf8 cs
   with Not_found ->
-    tt.node
+    last
 
-and progress_from_byte nr tt cs = function
+and progress_from_byte last nj tt cs = function
   (* Utf8 leading byte *)
-  | '\x00'..'\x7F' as c -> progress_utf8 nr 1 c tt cs
-  | '\xC0'..'\xDF' as c -> progress_utf8 nr 2 c tt cs
-  | '\xE0'..'\xEF' as c -> progress_utf8 nr 3 c tt cs
-  | '\xF0'..'\xF7' as c -> progress_utf8 nr 4 c tt cs
+  | '\x00'..'\x7F' as c -> progress_utf8 last nj 1 c tt cs
+  | '\xC0'..'\xDF' as c -> progress_utf8 last nj 2 c tt cs
+  | '\xE0'..'\xEF' as c -> progress_utf8 last nj 3 c tt cs
+  | '\xF0'..'\xF7' as c -> progress_utf8 last nj 4 c tt cs
   | _ (* '\x80'..\xBF'|'\xF8'..'\xFF' *) ->
       error_utf8 cs
 
 (* Must be a special token *)
 let process_chars bp c cs =
-  let t = progress_from_byte 1 !token_tree cs c in
+  let t = progress_from_byte None (-1) !token_tree cs c in
   let ep = Stream.count cs in
   match t with
     | Some t -> (("", t), (bp, ep))
diff --git a/theories/Logic/ClassicalDescription.v b/theories/Logic/ClassicalDescription.v
index aa65eb44c..855588602 100644
--- a/theories/Logic/ClassicalDescription.v
+++ b/theories/Logic/ClassicalDescription.v
@@ -21,7 +21,7 @@ Set Implicit Arguments.
 Require Export Classical.
 Require Import ChoiceFacts.
 
-Notation Local "'inhabited' A" := A (at level 200, only parsing).
+Notation Local inhabited A := A.
 
 Axiom constructive_definite_description :
   forall (A : Type) (P : A->Prop), (exists! x : A, P x) -> { x : A | P x }.
diff --git a/theories/Logic/ClassicalFacts.v b/theories/Logic/ClassicalFacts.v
index f3f177a73..6673fa8c9 100644
--- a/theories/Logic/ClassicalFacts.v
+++ b/theories/Logic/ClassicalFacts.v
@@ -119,7 +119,7 @@ Qed.
 
 *)
 
-Definition inhabited (A:Prop) := A.
+Notation Local inhabited A := A.
 
 Lemma prop_ext_A_eq_A_imp_A :
   prop_extensionality -> forall A:Prop, inhabited A -> (A -> A) = A.
@@ -514,8 +514,6 @@ Qed.
     344 of Lecture Notes in Mathematics, Springer-Verlag, 1973.
 *)
 
-Notation Local "'inhabited' A" := A (at level 10, only parsing).
-
 Definition IndependenceOfGeneralPremises :=
   forall (A:Type) (P:A -> Prop) (Q:Prop),
     inhabited A -> (Q -> exists x, P x) -> exists x, Q -> P x.
diff --git a/theories/Logic/ConstructiveEpsilon.v b/theories/Logic/ConstructiveEpsilon.v
index fe571779c..83d5e002a 100644
--- a/theories/Logic/ConstructiveEpsilon.v
+++ b/theories/Logic/ConstructiveEpsilon.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id:$ i*)
+(*i $Id$ i*)
 
 (** This module proves the constructive description schema, which
 infers the sigma-existence (i.e., [Set]-existence) of a witness to a
@@ -53,7 +53,7 @@ of our searching algorithm. *)
 
 Let R (x y : nat) : Prop := x = S y /\ ~ P y.
 
-Notation Local "'acc' x" := (Acc R x) (at level 10).
+Notation Local acc x := (Acc R x).
 
 Lemma P_implies_acc : forall x : nat, P x -> acc x.
 Proof.
diff --git a/theories/Logic/Diaconescu.v b/theories/Logic/Diaconescu.v
index a954cbef7..b96ae30e4 100644
--- a/theories/Logic/Diaconescu.v
+++ b/theories/Logic/Diaconescu.v
@@ -267,7 +267,7 @@ End ProofIrrel_RelChoice_imp_EqEM.
 
 (** Proof sketch from Bell [Bell93] (with thanks to P. Castéran) *)
 
-Notation Local "'inhabited' A" := A (at level 10, only parsing).
+Notation Local inhabited A := A.
 
 Section ExtensionalEpsilon_imp_EM.
 
diff --git a/theories/Numbers/Cyclic/Abstract/NZCyclic.v b/theories/Numbers/Cyclic/Abstract/NZCyclic.v
index 92ada3d74..125fd3f12 100644
--- a/theories/Numbers/Cyclic/Abstract/NZCyclic.v
+++ b/theories/Numbers/Cyclic/Abstract/NZCyclic.v
@@ -89,8 +89,8 @@ Open Local Scope IntScope.
 Notation "x == y"  := (NZeq x y) (at level 70) : IntScope.
 Notation "x ~= y" := (~ NZeq x y) (at level 70) : IntScope.
 Notation "0" := NZ0 : IntScope.
-Notation "'S'" := NZsucc : IntScope.
-Notation "'P'" := NZpred : IntScope.
+Notation S x := (NZsucc x).
+Notation P x := (NZpred x).
 (*Notation "1" := (S 0) : IntScope.*)
 Notation "x + y" := (NZadd x y) : IntScope.
 Notation "x - y" := (NZsub x y) : IntScope.
diff --git a/theories/Program/Utils.v b/theories/Program/Utils.v
index c4a20506c..149901c7b 100644
--- a/theories/Program/Utils.v
+++ b/theories/Program/Utils.v
@@ -42,8 +42,8 @@ Notation dec := sumbool_of_bool.
 
 (** Hide proofs and generates obligations when put in a term. *)
 
-Notation "'in_left'" := (@left _ _ _) : program_scope.
-Notation "'in_right'" := (@right _ _ _) : program_scope.
+Notation in_left := (@left _ _ _).
+Notation in_right := (@right _ _ _).
 
 (** Extraction directives *)
 (*
@@ -53,4 +53,4 @@ Extract Inductive bool => "bool" [ "true" "false" ].
 Extract Inductive sumbool => "bool" [ "true" "false" ].
 (* Extract Inductive prod "'a" "'b" => " 'a * 'b " [ "(,)" ]. *)
 (* Extract Inductive sigT => "prod" [ "" ]. *)
-*)
\ No newline at end of file
+*)
diff --git a/theories/QArith/QArith_base.v b/theories/QArith/QArith_base.v
index 9ebfa19cb..f4b57d5be 100644
--- a/theories/QArith/QArith_base.v
+++ b/theories/QArith/QArith_base.v
@@ -31,7 +31,7 @@ Notation "a # b" := (Qmake a b) (at level 55, no associativity) : Q_scope.
 Definition inject_Z (x : Z) := Qmake x 1.
 Arguments Scope inject_Z [Z_scope].
 
-Notation " 'QDen'  p " := (Zpos (Qden p)) (at level 20, no associativity) : Q_scope.
+Notation QDen p := (Zpos (Qden p)).
 Notation " 0 " := (0#1) : Q_scope.
 Notation " 1 " := (1#1) : Q_scope.
 
diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml
index bad30a849..b11592ba4 100644
--- a/toplevel/cerrors.ml
+++ b/toplevel/cerrors.ml
@@ -34,17 +34,17 @@ let rec explain_exn_default_aux anomaly_string report_fn = function
   | Stream.Failure -> 
       hov 0 (anomaly_string () ++ str "uncaught Stream.Failure.")
   | Stream.Error txt -> 
-      hov 0 (str "Syntax error: " ++ str txt)
+      hov 0 (str "Syntax error: " ++ str txt ++ str ".")
   | Token.Error txt -> 
-      hov 0 (str "Syntax error: " ++ str txt)
+      hov 0 (str "Syntax error: " ++ str txt ++ str ".")
   | Sys_error msg -> 
       hov 0 (anomaly_string () ++ str "uncaught exception Sys_error " ++ str (guill msg) ++ report_fn ())
   | UserError(s,pps) -> 
       hov 1 (str "User error: " ++ where s ++ pps)
   | Out_of_memory -> 
-      hov 0 (str "Out of memory")
+      hov 0 (str "Out of memory.")
   | Stack_overflow -> 
-      hov 0 (str "Stack overflow")
+      hov 0 (str "Stack overflow.")
   | Anomaly (s,pps) -> 
       hov 1 (anomaly_string () ++ where s ++ pps ++ report_fn ())
   | Match_failure(filename,pos1,pos2) ->
@@ -94,10 +94,11 @@ let rec explain_exn_default_aux anomaly_string report_fn = function
       hov 0 (str "Error:" ++ spc () ++
 	       str "The reference" ++ spc () ++ Libnames.pr_qualid q ++
 	       spc () ++ str "was not found" ++ 
-	       spc () ++ str "in the current" ++ spc () ++ str "environment")
+	       spc () ++ str "in the current" ++ spc () ++ str "environment.")
   | Nametab.GlobalizationConstantError q ->
       hov 0 (str "Error:" ++ spc () ++
-	       str "No constant of this name:" ++ spc () ++ Libnames.pr_qualid q)
+	       str "No constant of this name:" ++ spc () ++ 
+               Libnames.pr_qualid q ++ str ".")
   | Refiner.FailError (i,s) ->
       hov 0 (str "Error: Tactic failure" ++ s ++
              if i=0 then mt () else str " (level " ++ int i ++ str").")
@@ -145,7 +146,7 @@ let raise_if_debug e =
 let _ = Tactic_debug.explain_logic_error := explain_exn_default
 
 let _ = Tactic_debug.explain_logic_error_no_anomaly :=
-          explain_exn_default_aux (fun () -> mt()) (fun () -> mt())
+          explain_exn_default_aux (fun () -> mt()) (fun () -> str ".")
 
 let explain_exn_function = ref explain_exn_default