From 25b07a6f824654be2041152d904507bc62102986 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 28 Feb 2018 13:45:04 +0100 Subject: 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. --- printing/ppvernac.ml | 15 ++++++--------- 1 file changed, 6 insertions(+), 9 deletions(-) (limited to 'printing') 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 ( -- cgit v1.2.3