Fixing/improving management of uniform prefix Local and Global

modifiers (added a "Syntax Checking" phase for raising a non
interpretation error just after a dot is parsed -- maybe exaggerated
complication for what we want to do ?).



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

4 files changed, 30 insertions, 12 deletions

diff --git a/toplevel/protectedtoplevel.ml b/toplevel/protectedtoplevel.ml
index f62d1c81c..db5a5c4c5 100644
--- a/toplevel/protectedtoplevel.ml
+++ b/toplevel/protectedtoplevel.ml
@@ -11,6 +11,7 @@
 open Pp
 open Line_oriented_parser
 open Vernac
+open Vernacexpr
 
 (* The toplevel parsing loop we propose here is more robust to printing
    errors.  The philosophy is that all commands should be individually wrapped
@@ -130,7 +131,8 @@ let rec parse_one_command_group input_channel =
 			      	!global_request_id !count None)
 		       | Some(rank, e) ->
 			   (match e with 
-                    	      	DuringCommandInterp(a,e1) ->
+                    	     | DuringCommandInterp(a,e1)
+			     | Stdpp.Exc_located (a,DuringSyntaxChecking e1) ->
 				  output_results_nl
 				    (acknowledge_command
 				       !global_request_id rank (Some e1))
@@ -164,7 +166,8 @@ let protected_loop input_chan =
       | End_of_file -> exit 0
       | DuringCommandInterp(loc, Vernacexpr.Quit) -> raise Vernacexpr.Quit
       | DuringCommandInterp(loc, Vernacexpr.Drop) -> raise Vernacexpr.Drop
-      | DuringCommandInterp(loc, e) ->
+      | DuringCommandInterp(loc, e)
+      | Stdpp.Exc_located (loc,DuringSyntaxChecking e) ->
 	  explain_and_restart e
       | e -> explain_and_restart e in
     begin
diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml
index 14207b5e5..7f869c166 100644
--- a/toplevel/toplevel.ml
+++ b/toplevel/toplevel.ml
@@ -13,6 +13,7 @@ open Util
 open Flags
 open Cerrors
 open Vernac
+open Vernacexpr
 open Pcoq
 open Protectedtoplevel
 
@@ -262,6 +263,7 @@ let rec is_pervasive_exn = function
   | Error_in_file (_,_,e) -> is_pervasive_exn e
   | Stdpp.Exc_located (_,e) -> is_pervasive_exn e
   | DuringCommandInterp (_,e) -> is_pervasive_exn e
+  | DuringSyntaxChecking e -> is_pervasive_exn e
   | _ -> false
 
 (* Toplevel error explanation, dealing with locations, Drop, Ctrl-D
@@ -270,7 +272,8 @@ let rec is_pervasive_exn = function
 let print_toplevel_error exc =
   let (dloc,exc) =
     match exc with
-      | DuringCommandInterp (loc,ie) ->
+      | DuringCommandInterp (loc,ie)
+      | Stdpp.Exc_located (loc, DuringSyntaxChecking ie) ->
           if loc = dummy_loc then (None,ie) else (Some loc, ie)
       | _ -> (None, exc) 
   in
@@ -321,7 +324,8 @@ let rec discard_to_dot () =
  * in encountered. *)
 
 let process_error = function
-  | DuringCommandInterp _ as e -> e
+  | DuringCommandInterp _ 
+  | Stdpp.Exc_located (_,DuringSyntaxChecking _) as e -> e
   | e ->
       if is_pervasive_exn e then 
 	e
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index cdfa85328..c7224ddaa 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -32,7 +32,8 @@ exception DuringCommandInterp of Util.loc * exn
 let raise_with_file file exc =
   let (cmdloc,re) =
     match exc with
-      | DuringCommandInterp(loc,e) -> (loc,e)
+      | DuringCommandInterp(loc,e)
+      | Stdpp.Exc_located (loc,DuringSyntaxChecking e) -> (loc,e)
       | e -> (dummy_loc,e) 
   in
   let (inner,inex) =
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index 14bcb1ef7..5ea0235a5 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -338,6 +338,14 @@ type vernac_expr =
 
 and located_vernac_expr = loc * vernac_expr
 
+(* Locating errors raised just after the dot is parsed but before the
+   interpretation phase *)
+
+exception DuringSyntaxChecking of exn
+
+let syntax_checking_error s = 
+  raise (DuringSyntaxChecking (UserError ("",Pp.str s)))
+
 (* Managing locality *)
 
 let locality_flag = ref None
@@ -346,9 +354,9 @@ let local_of_bool = function true -> Local | false -> Global
 
 let check_locality () =
   if !locality_flag = Some true then
-    error "This command does not support the \"Local\" prefix";
+    syntax_checking_error "This command does not support the \"Local\" prefix.";
   if !locality_flag = Some false then
-    error "This command does not support the \"Global\" prefix"
+    syntax_checking_error "This command does not support the \"Global\" prefix."
 
 let use_locality () =
   let local = match !locality_flag with Some true -> true | _ -> false in
@@ -373,9 +381,10 @@ let enforce_locality () =
   let local =
     match !locality_flag with 
     | Some false ->
-	error "Cannot be simultaneously Local and Global"
+	error "Cannot be simultaneously Local and Global."
     | _ -> 
-	Flags.if_verbose Pp.warning "Obsolete syntax: use \"Local\" prefix"; 
+	Flags.if_verbose
+	  Pp.warning "Obsolete syntax: use \"Local\" as a prefix."; 
 	true in
   locality_flag := None;
   local
@@ -386,12 +395,13 @@ let enforce_locality_of local =
   let local = 
     match !locality_flag with 
     | Some false when local ->
-	error "Cannot be simultaneously Local and Global"
+	error "Cannot be simultaneously Local and Global."
     | Some true when local ->
-	error "Use only prefix \"Local\""
+	error "Use only prefix \"Local\"."
     | None ->
 	if local then
-	  Flags.if_verbose Pp.warning "Obsolete syntax: use \"Local\" prefix";
+	  Flags.if_verbose
+	    Pp.warning "Obsolete syntax: use \"Local\" as a prefix.";
 	local
     | Some b -> b in
   locality_flag := None;