From ce83c2b9fd1685e46049ee7f47c8716dcf66dbd1 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Tue, 6 Oct 2015 14:11:19 +0200
Subject: Goptions: new value type: optional string

These options can be set to a string value, but also unset.
Internal data is of type string option.
---
 ide/ide_slave.ml | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'ide/ide_slave.ml')

diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml
index 94f9c9a361..041f2f83b8 100644
--- a/ide/ide_slave.ml
+++ b/ide/ide_slave.ml
@@ -291,11 +291,13 @@ let export_option_value = function
   | Goptions.BoolValue b   -> Interface.BoolValue b
   | Goptions.IntValue x    -> Interface.IntValue x
   | Goptions.StringValue s -> Interface.StringValue s
+  | Goptions.StringOptValue s -> Interface.StringOptValue s
 
 let import_option_value = function
   | Interface.BoolValue b   -> Goptions.BoolValue b
   | Interface.IntValue x    -> Goptions.IntValue x
   | Interface.StringValue s -> Goptions.StringValue s
+  | Interface.StringOptValue s -> Goptions.StringOptValue s
 
 let export_option_state s = {
   Interface.opt_sync  = s.Goptions.opt_sync;
@@ -314,6 +316,8 @@ let set_options options =
   | BoolValue b -> Goptions.set_bool_option_value name b
   | 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
   in
   List.iter iter options
 
-- 
cgit v1.2.3