diff options
| author | Lionel Rieg | 2015-06-25 14:58:25 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-06-26 11:33:57 +0200 |
| commit | aac2d2ac490492f8466e1d45ba0079de376fe25a (patch) | |
| tree | a7cde3a9f7bf933a912c37a0882813e85b8051b0 /stm | |
| parent | e7be889cdc86190ab71709a708e4beb6d3040dd8 (diff) | |
Introduction of a "Undelimit Scope" command, undoing "Delimit Scope"
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/texmacspp.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/stm/texmacspp.ml b/stm/texmacspp.ml index 9edc1f1c70..aaa6c2c07d 100644 --- a/stm/texmacspp.ml +++ b/stm/texmacspp.ml @@ -509,8 +509,10 @@ let rec tmpp v loc = | VernacOpenCloseScope (_,(true,name)) -> xmlScope loc "open" name [] | VernacOpenCloseScope (_,(false,name)) -> xmlScope loc "close" name [] - | VernacDelimiters (name,tag) -> + | VernacDelimiters (name,Some tag) -> xmlScope loc "delimit" name ~attr:["delimiter",tag] [] + | VernacDelimiters (name,None) -> + xmlScope loc "undelimit" name ~attr:[] [] | VernacBindScope (name,l) -> xmlScope loc "bind" name (List.map (function |