From 6f393734e54146c4d26325aea006368380d97280 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Mon, 5 Sep 2016 16:23:09 +0200
Subject: Summary: simpler API for process-local storage

---
 library/summary.ml  | 25 +++++++++++++++++++++++++
 library/summary.mli | 11 +++++++++++
 2 files changed, 36 insertions(+)

(limited to 'library')

diff --git a/library/summary.ml b/library/summary.ml
index 4fef06438d..6efa07f388 100644
--- a/library/summary.ml
+++ b/library/summary.ml
@@ -186,4 +186,29 @@ let ref ?(freeze=fun _ r -> r) ~name x =
       init_function = (fun () -> r := x) };
   r
 
+module Local = struct
+
+type 'a local_ref = ('a CEphemeron.key * string) ref
+
+let (:=) r v = r := (CEphemeron.create v, snd !r)
+
+let (!) r =
+  let key, name = !r in
+  try CEphemeron.get key
+  with CEphemeron.InvalidKey ->
+    let _, { init_function } =
+      Int.Map.find (String.hash (mangle name)) !summaries in
+    init_function ();
+    CEphemeron.get (fst !r)
+
+let ref ?(freeze=fun x -> x) ~name init =
+  let r = Pervasives.ref (CEphemeron.create init, name) in
+  declare_summary name
+    { freeze_function = (fun _ -> freeze !r);
+      unfreeze_function = ((:=) r);
+      init_function = (fun () -> r := init) };
+  r
+
+end
+
 let dump = Dyn.dump
diff --git a/library/summary.mli b/library/summary.mli
index 27889cab27..1b57613cb7 100644
--- a/library/summary.mli
+++ b/library/summary.mli
@@ -42,6 +42,17 @@ val declare_summary : string -> 'a summary_declaration -> unit
 
 val ref : ?freeze:(marshallable -> 'a -> 'a) -> name:string -> 'a -> 'a ref
 
+(* As [ref] but the value is local to a process, i.e. not sent to, say, proof
+ * workers.  It is useful to implement a local cache for example. *)
+module Local : sig
+
+  type 'a local_ref
+  val ref : ?freeze:('a -> 'a) -> name:string -> 'a -> 'a local_ref
+  val (:=) : 'a local_ref -> 'a -> unit
+  val (!) : 'a local_ref -> 'a
+
+end
+
 (** Special name for the summary of ML modules.  This summary entry is
     special because its unfreeze may load ML code and hence add summary
     entries.  Thus is has to be recognizable, and handled appropriately *)
-- 
cgit v1.2.3


From 977e91d0aa5cfece962fc82e3fd42402918663c8 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 6 Sep 2016 18:42:52 +0200
Subject: A proposal to unify the messages given by Test and Print Options
 (#5062).

---
 library/goptions.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'library')

diff --git a/library/goptions.ml b/library/goptions.ml
index 0459417fbb..1cf25987b1 100644
--- a/library/goptions.ml
+++ b/library/goptions.ml
@@ -365,8 +365,8 @@ let set_string_option_value = set_string_option_value_gen None
 
 let msg_option_value (name,v) =
   match v with
-    | BoolValue true  -> str "true"
-    | BoolValue false -> str "false"
+    | BoolValue true  -> str "on"
+    | BoolValue false -> str "off"
     | IntValue (Some n) -> int n
     | IntValue None   -> str "undefined"
     | StringValue s   -> str s
-- 
cgit v1.2.3