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. --- ide/ide_slave.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'ide') diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index 9fe580091..55b4fa87e 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -57,8 +57,8 @@ let coqide_known_option table = List.mem table [ ["Printing";"Unfocused"]] let is_known_option cmd = match Vernacprop.under_control cmd with - | VernacSetOption (o,BoolValue true) - | VernacUnsetOption o -> coqide_known_option o + | VernacSetOption (_, o, BoolValue true) + | VernacUnsetOption (_, o) -> coqide_known_option o | _ -> false (** Check whether a command is forbidden in the IDE *) -- cgit v1.2.3