diff options
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/vernac.ml | 10 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 6 |
2 files changed, 7 insertions, 9 deletions
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 |