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 /intf | |
| 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 'intf')
| -rw-r--r-- | intf/vernacexpr.mli | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index 335e04b91..3ffaca113 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: |