From 38a671f74857aec8e285a6a0bfcab876e3b9a133 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 28 Feb 2018 13:26:53 +0100
Subject: Export the various option localities in the API.

This prevents relying on an underspecified bool option argument.
---
 ide/ide_slave.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'ide')

diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml
index 0ba1b3a4fb..9fe580091b 100644
--- a/ide/ide_slave.ml
+++ b/ide/ide_slave.ml
@@ -340,7 +340,7 @@ let set_options options =
   | IntValue i -> Goptions.set_int_option_value name i
   | StringValue s -> Goptions.set_string_option_value name s
   | StringOptValue (Some s) -> Goptions.set_string_option_value name s
-  | StringOptValue None -> Goptions.unset_option_value_gen None name
+  | StringOptValue None -> Goptions.unset_option_value_gen name
   in
   List.iter iter options
 
-- 
cgit v1.2.3


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 9fe580091b..55b4fa87e6 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