New cleaning phase of the Local/Global option management

- Clarification and documentation of the different styles of
  Local/Global modifiers in vernacexpr.ml
- Addition of Global in sections for Open/Close Scope.
- Addition of Local for Ltac when not in sections.

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

5 files changed, 99 insertions, 65 deletions

diff --git a/toplevel/protectedtoplevel.ml b/toplevel/protectedtoplevel.ml
index ad1beb553..7abb68eea 100644
--- a/toplevel/protectedtoplevel.ml
+++ b/toplevel/protectedtoplevel.ml
@@ -132,7 +132,7 @@ let rec parse_one_command_group input_channel =
 		       | Some(rank, e) ->
 			   (match e with
                     	     | DuringCommandInterp(a,e1)
-			     | Stdpp.Exc_located (a,DuringSyntaxChecking e1) ->
+			     | DuringSyntaxChecking(a,e1) ->
 				  output_results_nl
 				    (acknowledge_command
 				       !global_request_id rank (Some e1))
@@ -167,7 +167,7 @@ let protected_loop input_chan =
       | DuringCommandInterp(loc, Vernacexpr.Quit) -> raise Vernacexpr.Quit
       | DuringCommandInterp(loc, Vernacexpr.Drop) -> raise Vernacexpr.Drop
       | DuringCommandInterp(loc, e)
-      | Stdpp.Exc_located (loc,DuringSyntaxChecking e) ->
+      | DuringSyntaxChecking(loc, e) ->
 	  explain_and_restart e
       | e -> explain_and_restart e in
     begin
diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml
index d14acaab9..b57b9c1eb 100644
--- a/toplevel/toplevel.ml
+++ b/toplevel/toplevel.ml
@@ -275,7 +275,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
+  | DuringSyntaxChecking (_,e) -> is_pervasive_exn e
   | _ -> false
 
 (* Toplevel error explanation, dealing with locations, Drop, Ctrl-D
@@ -285,7 +285,7 @@ let print_toplevel_error exc =
   let (dloc,exc) =
     match exc with
       | DuringCommandInterp (loc,ie)
-      | Stdpp.Exc_located (loc, DuringSyntaxChecking ie) ->
+      | DuringSyntaxChecking (loc,ie) ->
           if loc = dummy_loc then (None,ie) else (Some loc, ie)
       | _ -> (None, exc)
   in
@@ -337,7 +337,7 @@ let rec discard_to_dot () =
 
 let process_error = function
   | DuringCommandInterp _
-  | Stdpp.Exc_located (_,DuringSyntaxChecking _) as e -> e
+  | DuringSyntaxChecking _ as e -> e
   | e ->
       if is_pervasive_exn e then
 	e
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index a14e8ad45..6d4ecf774 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -33,7 +33,7 @@ let raise_with_file file exc =
   let (cmdloc,re) =
     match exc with
       | DuringCommandInterp(loc,e)
-      | Stdpp.Exc_located (loc,DuringSyntaxChecking e) -> (loc,e)
+      | DuringSyntaxChecking(loc,e) -> (loc,e)
       | e -> (dummy_loc,e)
   in
   let (inner,inex) =
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 664b05f1d..754f58a9c 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -747,7 +747,8 @@ let vernac_backto n = Lib.reset_label n
 (************)
 (* Commands *)
 
-let vernac_declare_tactic_definition = Tacinterp.add_tacdef
+let vernac_declare_tactic_definition (local,x,def) =
+  Tacinterp.add_tacdef local x def
 
 let vernac_create_hintdb local id b =
   Auto.create_hint_db local id full_transparent_state b
@@ -1368,7 +1369,7 @@ let interp c = match c with
   | VernacBackTo n -> vernac_backto n
 
   (* Commands *)
-  | VernacDeclareTacticDefinition (x,l) -> vernac_declare_tactic_definition x l
+  | VernacDeclareTacticDefinition def -> vernac_declare_tactic_definition def
   | VernacCreateHintDb (local,dbname,b) -> vernac_create_hintdb local dbname b
   | VernacHints (local,dbnames,hints) -> vernac_hints local dbnames hints
   | VernacSyntacticDefinition (id,c,l,b) ->vernac_syntactic_definition id c l b
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index 96960540b..cedd20e08 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -293,7 +293,7 @@ type vernac_expr =
 
   (* Commands *)
   | VernacDeclareTacticDefinition of
-      rec_flag * (reference * bool * raw_tactic_expr) list
+      (locality_flag * rec_flag * (reference * bool * raw_tactic_expr) list)
   | VernacCreateHintDb of locality_flag * lstring * bool
   | VernacHints of locality_flag * lstring list * hints_expr
   | VernacSyntacticDefinition of identifier located * (identifier list * constr_expr) *
@@ -344,65 +344,41 @@ 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
+exception DuringSyntaxChecking of exn located
 
-let syntax_checking_error s =
-  raise (DuringSyntaxChecking (UserError ("",Pp.str s)))
+let syntax_checking_error loc s =
+  raise (DuringSyntaxChecking (loc,UserError ("",Pp.str s)))
 
+(**********************************************************************)
 (* Managing locality *)
 
 let locality_flag = ref None
 
 let local_of_bool = function true -> Local | false -> Global
 
-let check_locality () =
-  if !locality_flag = Some true then
-    syntax_checking_error "This command does not support the \"Local\" prefix.";
-  if !locality_flag = Some false then
-    syntax_checking_error "This command does not support the \"Global\" prefix."
-
-let use_locality_full () =
-  let r = !locality_flag in
-  locality_flag := None;
-   r
-
-let use_locality () =
-  match use_locality_full () with Some true -> true | _ -> false
-
-let use_locality_exp () = local_of_bool (use_locality ())
-
-let use_section_locality () =
-  match use_locality_full () with Some b -> b | None -> Lib.sections_are_opened ()
-
-let use_non_locality () =
-  match use_locality_full () with Some false -> false | _ -> true
-
-let use_section_non_locality () =
-  match use_locality_full () with Some b -> b | None -> Lib.sections_are_opened ()
+let is_true = function Some (_,b) -> b | _ -> false
+let is_false = function Some (_,b) -> not b | _ -> false
 
-let enforce_locality () =
-  let local =
-    match !locality_flag with
-    | Some false ->
-	error "Cannot be simultaneously Local and Global."
-    | _ ->
-	Flags.if_verbose
-	  Pp.warning "Obsolete syntax: use \"Local\" as a prefix.";
-	true in
-  locality_flag := None;
-  local
+let check_locality () =
+  match !locality_flag with
+  | Some (loc,true) -> 
+      syntax_checking_error loc
+	"This command does not support the \"Local\" prefix.";
+  | Some (loc,false) -> 
+      syntax_checking_error loc
+	"This command does not support the \"Global\" prefix."
+  | None -> ()
 
-(* [enforce_locality_exp] supports Local (with effect in section) but not
-   Global in section *)
+(** Extracting the locality flag *)
 
-let enforce_locality_exp () = local_of_bool (enforce_locality ())
+(* Commands which supported an inlined Local flag *)
 
-let enforce_full_locality_of local =
+let enforce_locality_full local =
   let local =
     match !locality_flag with
-    | Some false when local ->
+    | Some (_,false) when local ->
 	error "Cannot be simultaneously Local and Global."
-    | Some true when local ->
+    | Some (_,true) when local ->
 	error "Use only prefix \"Local\"."
     | None ->
 	if local then begin
@@ -411,18 +387,75 @@ let enforce_full_locality_of local =
 	  Some true
 	end else
 	None
-    | Some _ as b -> b in
+    | Some (_,b) -> Some b in
   locality_flag := None;
   local
 
-(* [enforce_locality_of] supports Local (with effect if not in
-   section) but not Global in section *)
-
-let enforce_locality_of local =
-  match enforce_full_locality_of local with
-    | Some false ->
-	if Lib.sections_are_opened () then
-	  error "This command does not support the Global option in sections.";
-	false
-    | Some true -> true 
-    | None -> false
+(* Commands which did not supported an inlined Local flag (synonym of
+   [enforce_locality_full false]) *)
+
+let use_locality_full () =
+  let r = Option.map snd !locality_flag in
+  locality_flag := None;
+   r
+
+(** Positioning locality for commands supporting discharging and export
+     outside of modules *)
+
+(* For commands whose default is to discharge and export:
+   Global is the default and is neutral;
+   Local in a section deactivate discharge, 
+   Local not in a section deactivates export *)
+
+let make_locality = function Some true -> true | _ -> false
+
+let use_locality () = make_locality (use_locality_full ())
+
+let use_locality_exp () = local_of_bool (use_locality ())
+
+let enforce_locality local = make_locality (enforce_locality_full local)
+
+let enforce_locality_exp local = local_of_bool (enforce_locality local)
+
+(* For commands whose default is not to discharge and not to export:
+   Global forces discharge and export;
+   Local is the default and is neutral *)
+
+let use_non_locality () =
+  match use_locality_full () with Some false -> false | _ -> true
+
+(* For commands whose default is to not discharge but to export:
+   Global in sections forces discharge, Global not in section is the default;
+   Local in sections is the default, Local not in section forces non-export *)
+
+let make_section_locality =
+  function Some b -> b | None -> Lib.sections_are_opened ()
+
+let use_section_locality () =
+  make_section_locality (use_locality_full ())
+
+let enforce_section_locality local =
+  make_section_locality (enforce_locality_full local)
+
+(** Positioning locality for commands supporting export but not discharge *)
+
+(* For commands whose default is to export (if not in section):
+   Global in sections is forbidden, Global not in section is neutral;
+   Local in sections is the default, Local not in section forces non-export *)
+
+let make_module_locality = function
+  | Some false ->
+      if Lib.sections_are_opened () then
+	error "This command does not support the Global option in sections.";
+      false
+  | Some true -> true
+  | None -> false
+
+let use_module_locality () =
+  make_module_locality (use_locality_full ())
+
+let enforce_module_locality local =
+  make_module_locality (enforce_locality_full local)
+
+(**********************************************************************)
+