Imported Upstream version 8.5~beta3+dfsg

1 files changed, 18 insertions, 7 deletions

diff --git a/library/goptions.ml b/library/goptions.ml
index ef25fa59..30d195f8 100644
--- a/library/goptions.ml
+++ b/library/goptions.ml
@@ -20,6 +20,7 @@ type option_value =
   | BoolValue   of bool
   | IntValue    of int option
   | StringValue of string
+  | StringOptValue of string option
 
 (** Summary of an option status *)
 type option_state = {
@@ -35,7 +36,7 @@ type option_state = {
 let nickname table = String.concat " " table
 
 let error_undeclared_key key =
-  error ((nickname key)^": no table or option of this type")
+  errorlabstrm "Goptions" (str (nickname key) ++ str ": no table or option of this type")
 
 (****************************************************************************)
 (* 1- Tables                                                                *)
@@ -293,6 +294,10 @@ let declare_string_option =
   declare_option
     (fun v -> StringValue v)
     (function StringValue v -> v | _ -> anomaly (Pp.str "async_option"))
+let declare_stringopt_option =
+  declare_option
+    (fun v -> StringOptValue v)
+    (function StringOptValue v -> v | _ -> anomaly (Pp.str "async_option"))
 
 (* 3- User accessible commands *)
 
@@ -301,7 +306,9 @@ let declare_string_option =
 let set_option_value locality check_and_cast key v =
   let (name, depr, (_,read,write,lwrite,gwrite)) =
     try get_option key
-    with Not_found -> error ("There is no option "^(nickname key)^".")
+    with Not_found ->
+      errorlabstrm "Goptions.set_option_value"
+        (str "There is no option " ++ str (nickname key) ++ str ".")
   in
   let write = match locality with
     | None -> write
@@ -322,11 +329,13 @@ let check_bool_value v = function
 
 let check_string_value v = function
   | StringValue _ -> StringValue v
+  | StringOptValue _ -> StringOptValue (Some v)
   | _ -> bad_type_error ()
 
 let check_unset_value v = function
   | BoolValue _ -> BoolValue false
   | IntValue _ -> IntValue None
+  | StringOptValue _ -> StringOptValue None
   | _ -> bad_type_error ()
 
 (* Nota: For compatibility reasons, some errors are treated as
@@ -357,6 +366,8 @@ let msg_option_value (name,v) =
     | IntValue (Some n) -> int n
     | IntValue None   -> str "undefined"
     | StringValue s   -> str s
+    | StringOptValue None   -> str"undefined"
+    | StringOptValue (Some s)   -> str s
 (*     | IdentValue r    -> pr_global_env Id.Set.empty r *)
 
 let print_option_value key =
@@ -364,9 +375,9 @@ let print_option_value key =
   let s = read () in
   match s with
     | BoolValue b ->
-	msg_info (str ("The "^name^" mode is "^(if b then "on" else "off")))
+	msg_info (str "The " ++ str name ++ str " mode is " ++ str (if b then "on" else "off"))
     | _ ->
-	msg_info (str ("Current value of "^name^" is ") ++ msg_option_value (name, s))
+	msg_info (str "Current value of " ++ str name ++ str " is " ++ msg_option_value (name, s))
 
 let get_tables () =
   let tables = !value_tab in
@@ -383,7 +394,7 @@ let get_tables () =
 
 let print_tables () =
   let print_option key name value depr =
-    let msg = str ("  "^(nickname key)^": ") ++ msg_option_value (name, value) in
+    let msg = str "  " ++ str (nickname key) ++ str ": " ++ msg_option_value (name, value) in
     if depr then msg ++ str " [DEPRECATED]" ++ fnl ()
     else msg ++ fnl ()
   in
@@ -401,10 +412,10 @@ let print_tables () =
       !value_tab (mt ()) ++
   str "Tables:" ++ fnl () ++
     List.fold_right
-      (fun (nickkey,_) p -> p ++ str ("  "^nickkey) ++ fnl ())
+      (fun (nickkey,_) p -> p ++ str "  " ++ str nickkey ++ fnl ())
       !string_table (mt ()) ++
     List.fold_right
-      (fun (nickkey,_) p -> p ++ str ("  "^nickkey) ++ fnl ())
+      (fun (nickkey,_) p -> p ++ str "  " ++ str nickkey ++ fnl ())
       !ref_table (mt ()) ++
     fnl ()