Program: avoid staying in program mode after a failed Program command

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

5 files changed, 22 insertions, 25 deletions

diff --git a/lib/flags.ml b/lib/flags.ml
index 29e01bac39..2f41c772ab 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -66,6 +66,11 @@ let auto_intros = ref true
 let make_auto_intros flag = auto_intros := flag
 let is_auto_intros () = version_strictly_greater V8_2 && !auto_intros
 
+(** [program_cmd] indicates that the current command is a Program one.
+    [program_mode] tells that Program mode has been activated, either
+    globally via [Set Program] or locally via the Program command prefix. *)
+
+let program_cmd = ref false
 let program_mode = ref false
 let is_program_mode () = !program_mode
 
diff --git a/lib/flags.mli b/lib/flags.mli
index 94c8795d45..b96bd402d4 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -47,6 +47,11 @@ val if_verbose : ('a -> unit) -> 'a -> unit
 val make_auto_intros : bool -> unit
 val is_auto_intros : unit -> bool
 
+(** [program_cmd] indicates that the current command is a Program one.
+    [program_mode] tells that Program mode has been activated, either
+    globally via [Set Program] or locally via the Program command prefix. *)
+
+val program_cmd : bool ref
 val program_mode : bool ref
 val is_program_mode : unit -> bool
 
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 336d1e1786..320ca4eb05 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -80,10 +80,10 @@ GEXTEND Gram
   vernac_aux:
     (* Better to parse "." here: in case of failure (e.g. in coerce_to_var), *)
     (* "." is still in the stream and discard_to_dot works correctly         *)
-    [ [ IDENT "Program"; g = gallina; "." -> program_flag := true; g
-      | IDENT "Program"; g = gallina_ext; "." -> program_flag := true; g
-      | g = gallina; "." -> g
-      | g = gallina_ext; "." -> g
+    [ [ IDENT "Program"; g = gallina; "." -> Flags.program_cmd := true; g
+      | IDENT "Program"; g = gallina_ext; "." -> Flags.program_cmd := true; g
+      | g = gallina; "." -> Flags.program_cmd := false; g
+      | g = gallina_ext; "." -> Flags.program_cmd := false; g
       | c = command; "." -> c
       | c = syntax; "." -> c
       | "["; l = LIST1 located_vernac; "]"; "." -> VernacList l
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 22ac6e90c1..4c12b4e7ba 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1620,12 +1620,15 @@ let interp c = match c with
   (* Extensions *)
   | VernacExtend (opn,args) -> Vernacinterp.call (opn,args)
 
-let interp c = 
+let interp c =
   let mode = Flags.is_program_mode () in
-    (try Obligations.set_program_mode !program_flag
-     with e -> program_flag := false; raise e);
+  let isprogcmd = !Flags.program_cmd in
+  Flags.program_cmd := false;
+  Obligations.set_program_mode isprogcmd;
+  try
     interp c; check_locality ();
-    program_flag := false;
     Flags.program_mode := mode
-  (* with_program_flag (fun () -> interp c ; check_locality ()) *)
+  with e ->
+    Flags.program_mode := mode;
+    raise e
 
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index c8729bfa97..95384c1c94 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -495,19 +495,3 @@ let use_module_locality () =
 
 let enforce_module_locality local =
   make_module_locality (enforce_locality_full local)
-
-(**********************************************************************)
-
-(**********************************************************************)
-(* Managing the Program extension. *)
-
-let program_flag = ref false
-let with_program_flag m = 
-  if Flags.is_program_mode () then
-    (program_flag := false; m ())
-  else if !program_flag then 
-    (Flags.program_mode := true; 
-     m ();
-     Flags.program_mode := false;
-     program_flag := false)
-