diff options
| -rw-r--r-- | intf/vernacexpr.mli | 5 | ||||
| -rw-r--r-- | parsing/g_vernac.ml4 | 6 | ||||
| -rw-r--r-- | printing/ppvernac.ml | 11 | ||||
| -rw-r--r-- | stm/vernac_classifier.ml | 12 | ||||
| -rw-r--r-- | toplevel/vernac.ml | 10 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 6 |
6 files changed, 29 insertions, 21 deletions
diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index 335e04b91f..3ffaca1138 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -265,9 +265,8 @@ type module_binder = bool option * lident list * module_ast_inl type vernac_expr = (* Control *) - | VernacList of located_vernac_expr list | VernacLoad of verbose_flag * string - | VernacTime of vernac_expr + | VernacTime of vernac_list | VernacTimeout of int * vernac_expr | VernacFail of vernac_expr | VernacError of exn (* always fails *) @@ -431,6 +430,8 @@ type vernac_expr = | VernacPolymorphic of bool * vernac_expr | VernacLocal of bool * vernac_expr +and vernac_list = located_vernac_expr list + and located_vernac_expr = Loc.t * vernac_expr (* A vernac classifier has to tell if a command: diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 05e6549255..3c3caa140b 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -69,7 +69,7 @@ let default_command_entry = GEXTEND Gram GLOBAL: vernac gallina_ext tactic_mode noedit_mode subprf subgoal_command; vernac: FIRST - [ [ IDENT "Time"; v = vernac -> VernacTime v + [ [ IDENT "Time"; l = vernac_list -> VernacTime l | IDENT "Timeout"; n = natural; v = vernac -> VernacTimeout(n,v) | IDENT "Fail"; v = vernac -> VernacFail v @@ -104,10 +104,12 @@ GEXTEND Gram | g = gallina_ext; "." -> g | c = command; "." -> c | c = syntax; "." -> c - | "["; l = LIST1 located_vernac; "]"; "." -> VernacList l | c = subprf -> c ] ] ; + vernac_list: + [ [ c = located_vernac -> [c] ] ] + ; vernac_aux: LAST [ [ prfcom = default_command_entry -> prfcom ] ] ; diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 6d7e3c38d9..16759a3d83 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -531,13 +531,9 @@ let rec pr_vernac = function | VernacRestoreState s -> str"Restore State" ++ spc() ++ qs s (* Control *) - | VernacList l -> - hov 2 (str"[" ++ spc() ++ - prlist (fun v -> pr_located pr_vernac v ++ sep_end (snd v) ++ fnl()) l - ++ spc() ++ str"]") | VernacLoad (f,s) -> str"Load" ++ if f then (spc() ++ str"Verbose" ++ spc()) else spc() ++ qs s - | VernacTime v -> str"Time" ++ spc() ++ pr_vernac v + | VernacTime v -> str"Time" ++ spc() ++ pr_vernac_list v | VernacTimeout(n,v) -> str"Timeout " ++ int n ++ spc() ++ pr_vernac v | VernacFail v -> str"Fail" ++ spc() ++ pr_vernac v | VernacError _ -> str"No-parsing-rule for VernacError" @@ -959,6 +955,11 @@ let rec pr_vernac = function | VernacSubproof (Some i) -> str "BeginSubproof " ++ int i | VernacEndSubproof -> str "}" +and pr_vernac_list l = + hov 2 (str"[" ++ spc() ++ + prlist (fun v -> pr_located pr_vernac v ++ sep_end (snd v) ++ fnl()) l + ++ spc() ++ str"]") + and pr_extend s cl = let pr_arg a = try pr_gen a diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index 8ba01a7b26..05c8fdd0d5 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -56,7 +56,7 @@ let undo_classifier = ref (fun _ -> assert false) let set_undo_classifier f = undo_classifier := f let rec classify_vernac e = - let static_classifier e = match e with + let rec static_classifier e = match e with (* PG compatibility *) | VernacUnsetOption (["Silent"]|["Undo"]|["Printing";"Depth"]) | VernacSetOption ((["Silent"]|["Undo"]|["Printing";"Depth"]),_) @@ -77,7 +77,7 @@ let rec classify_vernac e = make_polymorphic (classify_vernac e) else classify_vernac e | VernacTimeout (_,e) -> classify_vernac e - | VernacTime e -> classify_vernac e + | VernacTime e -> classify_vernac_list e | VernacFail e -> (* Fail Qed or Fail Lemma must not join/fork the DAG *) (match classify_vernac e with | ( VtQuery _ | VtProofStep | VtSideff _ @@ -157,7 +157,6 @@ let rec classify_vernac e = | VernacRegister _ | VernacComments _ -> VtSideff [], VtLater (* Who knows *) - | VernacList _ | VernacLoad _ -> VtSideff [], VtNow (* (Local) Notations have to disappear *) | VernacEndSegment _ -> VtSideff [], VtNow @@ -193,6 +192,13 @@ let rec classify_vernac e = | VernacExtend (s,l) -> try List.assoc s !classifiers l () with Not_found -> anomaly(str"No classifier for"++spc()++str s) + and classify_vernac_list = function + (* spiwack: It would be better to define a monoid on classifiers. + So that the classifier of the list would be the composition of + the classifier of the individual commands. Currently: special + case for singleton lists.*) + | [_,c] -> static_classifier c + | l -> VtUnknown,VtNow in let res = static_classifier e in if Flags.is_universe_polymorphism () then diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index e887204c3c..76d2b89c6c 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -27,12 +27,13 @@ let rec is_navigation_vernac = function | VernacBacktrack _ | VernacBackTo _ | VernacBack _ -> true - | VernacTime c -> is_navigation_vernac c (* Time Back* is harmless *) + | VernacTime l -> + List.exists + (fun (_,c) -> is_navigation_vernac c) l (* Time Back* is harmless *) | c -> is_deep_navigation_vernac c and is_deep_navigation_vernac = function | VernacTimeout (_,c) | VernacFail c -> is_navigation_vernac c - | VernacList l -> List.exists (fun (_,c) -> is_navigation_vernac c) l | _ -> false (* NB: Reset is now allowed again as asked by A. Chlipala *) @@ -234,9 +235,6 @@ let rec vernac_com verbosely checknav (loc,com) = raise reraise end - | VernacList l -> - List.iter (fun (_,v) -> interp v) l - | v when !just_parsing -> () | v -> Stm.interp verbosely (loc,v) @@ -245,7 +243,7 @@ let rec vernac_com verbosely checknav (loc,com) = checknav loc com; if do_beautify () then pr_new_syntax loc (Some com); if !Flags.time then display_cmd_header loc com; - let com = if !Flags.time then VernacTime com else com in + let com = if !Flags.time then VernacTime [loc,com] else com in interp com with reraise -> let reraise = Errors.push reraise in diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 0dbc77b83e..5864c54b6e 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -1669,7 +1669,6 @@ let interp ?proof locality poly c = prerr_endline ("interpreting: " ^ Pp.string_of_ppcmds (Ppvernac.pr_vernac c)); match c with (* Done later in this file *) - | VernacList _ -> assert false | VernacLoad _ -> assert false | VernacFail _ -> assert false | VernacTime _ -> assert false @@ -1960,11 +1959,10 @@ let interp ?(verbosely=true) ?proof (loc,c) = aux ?locality ?polymorphism isprogcmd v | VernacTime v -> let tstart = System.get_time() in - aux ?locality ?polymorphism isprogcmd v; + aux_list ?locality ?polymorphism isprogcmd v; let tend = System.get_time() in let msg = if !Flags.time then "" else "Finished transaction in " in msg_info (str msg ++ System.fmt_time_difference tstart tend) - | VernacList l -> List.iter (aux false) (List.map snd l) | VernacLoad (_,fname) -> vernac_load (aux false) fname | c -> check_vernac_supports_locality c locality; @@ -1991,6 +1989,8 @@ let interp ?(verbosely=true) ?proof (loc,c) = restore_timeout psh; Flags.program_mode := orig_program_mode; raise e + and aux_list ?locality ?polymorphism isprogcmd l = + List.iter (aux false) (List.map snd l) in if verbosely then Flags.verbosely (aux false) c else aux false c |