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 /printing | |
| 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 'printing')
| -rw-r--r-- | printing/ppvernac.ml | 11 |
1 files changed, 6 insertions, 5 deletions
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 |