diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-02-28 13:45:04 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-03-09 10:17:21 -0300 |
| commit | 25b07a6f824654be2041152d904507bc62102986 (patch) | |
| tree | 82f9d96e40911f85347ed4e5bc273cc6a15627f9 /printing | |
| parent | 38a671f74857aec8e285a6a0bfcab876e3b9a133 (diff) | |
Implement the Export Set/Unset feature.
This feature has been asked many times by different people, and allows to
have options in a module that are performed when this module is imported.
This supersedes the well-numbered cursed PR #313.
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/ppvernac.ml | 15 |
1 files changed, 6 insertions, 9 deletions
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 2b7d643d6..ea1ca26fb 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -1118,18 +1118,15 @@ open Decl_kinds hov 1 (keyword "Strategy" ++ spc() ++ hv 0 (prlist_with_sep sep pr_line l)) ) - | VernacUnsetOption (na) -> + | VernacUnsetOption (export, na) -> + let export = if export then keyword "Export" ++ spc () else mt () in return ( - hov 1 (keyword "Unset" ++ spc() ++ pr_printoption na None) + hov 1 (export ++ keyword "Unset" ++ spc() ++ pr_printoption na None) ) - | VernacSetOption (na,v) -> + | VernacSetOption (export, na,v) -> + let export = if export then keyword "Export" ++ spc () else mt () in return ( - hov 2 (keyword "Set" ++ spc() ++ pr_set_option na v) - ) - | VernacSetAppendOption (na,v) -> - return ( - hov 2 (keyword "Set" ++ spc() ++ pr_printoption na None ++ - spc() ++ keyword "Append" ++ spc() ++ qs v) + hov 2 (export ++ keyword "Set" ++ spc() ++ pr_set_option na v) ) | VernacAddOption (na,l) -> return ( |