diff options
| author | Arnaud Spiwack | 2014-06-06 14:42:07 +0200 |
|---|---|---|
| committer | Arnaud Spiwack | 2014-06-06 17:41:03 +0200 |
| commit | ff89f99bed1ae400c4cba283b17f172ca3fe6eee (patch) | |
| tree | f206d6ce6ddc4ca271723e7808c4508a6b03ec7e /toplevel | |
| parent | fd06eda492de2566ae44777ddbc9cd32744a2633 (diff) | |
Remove the syntax [Vernac1. Vernac2. … Vernacn. ].
It grouped a list of vernac commands as a single one. It was undocumented and unused (and apparently unusable, because the intermediate '.' seem to be parsed as end of phrases by the interfaces). The main application could be to group the commands for Time. There is room for such an application in the syntax, but I unplugged the syntax for the time being.
The syntax would conflict with the use of a standalone dispatching tactical [ t1 | t2 | … | tn ].
I took the opportunity to separate the code dedicated to lists of commands in a separate type from vernac_expr.
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 |