diff options
| author |  Arnaud Spiwack <arnaud@spiwack.net> | 2014-06-06 14:42:07 +0200 |
|---|---|---|
| committer | Arnaud Spiwack <arnaud@spiwack.net> | 2014-06-06 17:41:03 +0200 |
| commit | ff89f99bed1ae400c4cba283b17f172ca3fe6eee (patch) | |
| tree | f206d6ce6ddc4ca271723e7808c4508a6b03ec7e /toplevel/vernac.ml | |
| 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/vernac.ml')
| -rw-r--r-- | toplevel/vernac.ml | 10 |
1 files changed, 4 insertions, 6 deletions
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index e887204c3..76d2b89c6 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 |