diff options
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/vernacentries.ml | 56 | ||||
| -rw-r--r-- | vernac/vernacinterp.ml | 1 | ||||
| -rw-r--r-- | vernac/vernacinterp.mli | 1 | ||||
| -rw-r--r-- | vernac/vernacprop.ml | 8 |
4 files changed, 33 insertions, 33 deletions
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index bccde169f..3358951f4 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1958,11 +1958,6 @@ let interp ?proof ~atts ~st c = (* This one is possible to handle here *) | VernacAbort id -> CErrors.user_err (str "Abort cannot be used through the Load command") - (* Handled elsewhere *) - | VernacProgram _ - | VernacPolymorphic _ - | VernacLocal _ -> assert false - (* Syntax *) | VernacSyntaxExtension (infix, sl) -> vernac_syntax_extension atts infix sl @@ -2199,10 +2194,30 @@ let with_fail st b f = let interp ?(verbosely=true) ?proof ~st (loc,c) = let orig_univ_poly = Flags.is_universe_polymorphism () in let orig_program_mode = Flags.is_program_mode () in + let flags f atts = + List.fold_left + (fun (polymorphism, atts) f -> + match f with + | VernacProgram when not atts.program -> + (polymorphism, { atts with program = true }) + | VernacProgram -> + user_err Pp.(str "Program mode specified twice") + | VernacPolymorphic b when polymorphism = None -> + (Some b, atts) + | VernacPolymorphic _ -> + user_err Pp.(str "Polymorphism specified twice") + | VernacLocal b when Option.is_empty atts.locality -> + (polymorphism, { atts with locality = Some b }) + | VernacLocal _ -> + user_err Pp.(str "Locality specified twice") + ) + (None, atts) + f + in let rec control = function - | VernacExpr v -> - let atts = { loc; locality = None; polymorphic = false; } in - aux ~atts orig_program_mode v + | VernacExpr (f, v) -> + let (polymorphism, atts) = flags f { loc; locality = None; polymorphic = false; program = orig_program_mode; } in + aux ~polymorphism ~atts v | VernacFail v -> with_fail st true (fun () -> control v) | VernacTimeout (n,v) -> current_timeout := Some n; @@ -2212,25 +2227,8 @@ let interp ?(verbosely=true) ?proof ~st (loc,c) = | VernacTime (batch, (_loc,v)) -> System.with_time ~batch control v; - and aux ?polymorphism ~atts isprogcmd = function - - | VernacProgram c when not isprogcmd -> - aux ?polymorphism ~atts true c - - | VernacProgram _ -> - user_err Pp.(str "Program mode specified twice") - - | VernacPolymorphic (b, c) when polymorphism = None -> - aux ~polymorphism:b ~atts:atts isprogcmd c - - | VernacPolymorphic (b, c) -> - user_err Pp.(str "Polymorphism specified twice") - - | VernacLocal (b, c) when Option.is_empty atts.locality -> - aux ?polymorphism ~atts:{atts with locality = Some b} isprogcmd c - - | VernacLocal _ -> - user_err Pp.(str "Locality specified twice") + and aux ~polymorphism ~atts : _ -> unit = + function | VernacLoad (_,fname) -> vernac_load control fname @@ -2239,7 +2237,7 @@ let interp ?(verbosely=true) ?proof ~st (loc,c) = check_vernac_supports_polymorphism c polymorphism; let polymorphic = Option.default (Flags.is_universe_polymorphism ()) polymorphism in Flags.make_universe_polymorphism polymorphic; - Obligations.set_program_mode isprogcmd; + Obligations.set_program_mode atts.program; try vernac_timeout begin fun () -> let atts = { atts with polymorphic } in @@ -2248,7 +2246,7 @@ let interp ?(verbosely=true) ?proof ~st (loc,c) = else Flags.silently (interp ?proof ~atts ~st) c; (* If the command is `(Un)Set Program Mode` or `(Un)Set Universe Polymorphism`, we should not restore the previous state of the flag... *) - if orig_program_mode || not !Flags.program_mode || isprogcmd then + if orig_program_mode || not !Flags.program_mode || atts.program then Flags.program_mode := orig_program_mode; if (Flags.is_universe_polymorphism() = polymorphic) then Flags.make_universe_polymorphism orig_univ_poly; diff --git a/vernac/vernacinterp.ml b/vernac/vernacinterp.ml index c0b93c163..c40ca27db 100644 --- a/vernac/vernacinterp.ml +++ b/vernac/vernacinterp.ml @@ -16,6 +16,7 @@ type atts = { loc : Loc.t option; locality : bool option; polymorphic : bool; + program : bool; } type 'a vernac_command = 'a -> atts:atts -> st:Vernacstate.t -> Vernacstate.t diff --git a/vernac/vernacinterp.mli b/vernac/vernacinterp.mli index ab3d4bfc5..c5e610f89 100644 --- a/vernac/vernacinterp.mli +++ b/vernac/vernacinterp.mli @@ -14,6 +14,7 @@ type atts = { loc : Loc.t option; locality : bool option; polymorphic : bool; + program : bool; } type 'a vernac_command = 'a -> atts:atts -> st:Vernacstate.t -> Vernacstate.t diff --git a/vernac/vernacprop.ml b/vernac/vernacprop.ml index 4fdc78dd2..3932d1c7b 100644 --- a/vernac/vernacprop.ml +++ b/vernac/vernacprop.ml @@ -12,14 +12,14 @@ open Vernacexpr let rec under_control = function - | VernacExpr c -> c + | VernacExpr (_, c) -> c | VernacRedirect (_,(_,c)) | VernacTime (_,(_,c)) | VernacFail c | VernacTimeout (_,c) -> under_control c let rec has_Fail = function - | VernacExpr c -> false + | VernacExpr _ -> false | VernacRedirect (_,(_,c)) | VernacTime (_,(_,c)) | VernacTimeout (_,c) -> has_Fail c @@ -45,8 +45,8 @@ let rec is_deep_navigation_vernac = function (* NB: Reset is now allowed again as asked by A. Chlipala *) let is_reset = function - | VernacExpr VernacResetInitial - | VernacExpr (VernacResetName _) -> true + | VernacExpr ( _, VernacResetInitial) + | VernacExpr (_, VernacResetName _) -> true | _ -> false let is_debug cmd = match under_control cmd with |