diff options
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/vernacentries.ml | 53 | ||||
| -rw-r--r-- | vernac/vernacprop.ml | 8 |
2 files changed, 30 insertions, 31 deletions
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index ae62fcfeb..814dc1411 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1959,11 +1959,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 @@ -2200,10 +2195,31 @@ 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; program = orig_program_mode; } in - aux ~atts 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; control v @@ -2212,25 +2228,8 @@ let interp ?(verbosely=true) ?proof ~st (loc,c) = | VernacTime (batch, (_loc,v)) -> System.with_time ~batch control v; - and aux ?polymorphism ~atts = function - - | VernacProgram c when not atts.program -> - aux ?polymorphism ~atts:{ atts with program = true } c - - | VernacProgram _ -> - user_err Pp.(str "Program mode specified twice") - - | VernacPolymorphic (b, c) when polymorphism = None -> - aux ~polymorphism:b ~atts:atts 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} c - - | VernacLocal _ -> - user_err Pp.(str "Locality specified twice") + and aux ~polymorphism ~atts : _ -> unit = + function | VernacLoad (_,fname) -> vernac_load control fname 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 |