Make Program a regular attribute

We remove all calls to `Flags.is_program_mode` except one (to compute
the default value of the attribute). Everything else is passed
explicitely, and we remove the special logic in the interpretation loop
to set/unset the flag.

This is especially important since the value of the flag has an impact on
proof modes, so on the separation of parsing and execution phases.

1 files changed, 15 insertions, 1 deletions

diff --git a/vernac/attributes.ml b/vernac/attributes.ml
index 4f238f38e6..9b8c4efb37 100644
--- a/vernac/attributes.ml
+++ b/vernac/attributes.ml
@@ -125,11 +125,25 @@ let qualify_attribute qual (parser:'a attribute) : 'a attribute =
     let extra = if rem = [] then extra else (qual, VernacFlagList rem) :: extra in
     extra, v
 
+(** [program_mode] tells that Program mode has been activated, either
+    globally via [Set Program] or locally via the Program command prefix. *)
+
+let program_mode_option_name = ["Program";"Mode"]
+let program_mode = ref false
+
+let () = let open Goptions in
+  declare_bool_option
+    { optdepr  = false;
+      optname  = "use of the program extension";
+      optkey   = program_mode_option_name;
+      optread  = (fun () -> !program_mode);
+      optwrite = (fun b -> program_mode:=b) }
+
 let program_opt = bool_attribute ~name:"Program mode" ~on:"program" ~off:"noprogram"
 
 let program = program_opt >>= function
   | Some b -> return b
-  | None -> return (Flags.is_program_mode())
+  | None -> return (!program_mode)
 
 let locality = bool_attribute ~name:"Locality" ~on:"local" ~off:"global"