diff options
| author |  Matej Kosik <m4tej.kosik@gmail.com> | 2015-12-16 12:20:47 +0100 |
|---|---|---|
| committer | Matej Kosik <m4tej.kosik@gmail.com> | 2015-12-18 15:57:32 +0100 |
| commit | e181c9b043e64342c1e51763f4fe88c78bc4736d (patch) | |
| tree | 9dc9faf13b837b6be6704aee7a9241b0abcf5ba9 /stm/texmacspp.ml | |
| parent | 75d74cd7d124f244882b9c4ed200eac144dcbc43 (diff) | |
CLEANUP: Vernacexpr.vernac_expr
Originally, "VernacTime" and "VernacRedirect" were defined like this:
type vernac_expr =
...
| VernacTime of vernac_list
| VernacRedirect of string * vernac_list
...
where
type vernac_list = located_vernac_expr list
Currently, that list always contained one and only one element.
So I propose changing the definition of these two variants in the following way:
| VernacTime of located_vernac_expr
| VernacRedirect of string * located_vernac_expr
which covers all our current needs and enforces the invariant
related to the number of commands that are part of the
"VernacTime" and "VernacRedirect" variants.
Diffstat (limited to 'stm/texmacspp.ml')
| -rw-r--r-- | stm/texmacspp.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/stm/texmacspp.ml b/stm/texmacspp.ml index b91208041..95aaea6f0 100644 --- a/stm/texmacspp.ml +++ b/stm/texmacspp.ml @@ -487,12 +487,12 @@ let rec tmpp v loc = (* Control *) | VernacLoad (verbose,f) -> xmlWithLoc loc "load" ["verbose",string_of_bool verbose;"file",f] [] - | VernacTime l -> + | VernacTime (loc,e) -> xmlApply loc (Element("time",[],[]) :: - List.map (fun(loc,e) ->tmpp e loc) l) - | VernacRedirect (s, l) -> + [tmpp e loc]) + | VernacRedirect (s, (loc,e)) -> xmlApply loc (Element("redirect",["path", s],[]) :: - List.map (fun(loc,e) ->tmpp e loc) l) + [tmpp e loc]) | VernacTimeout (s,e) -> xmlApply loc (Element("timeout",["val",string_of_int s],[]) :: [tmpp e loc]) |