ajout de divers fonctions dans lib/

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@82 85f007b7-540e-0410-9357-904b9bb8a0f7

6 files changed, 52 insertions, 1 deletions

diff --git a/lib/dyn.ml b/lib/dyn.ml
index 92fa14f6d4..3d6d43f8c4 100644
--- a/lib/dyn.ml
+++ b/lib/dyn.ml
@@ -10,7 +10,8 @@ type t = string * Obj.t
 let dyntab = ref ([] : string list)
 
 let create s =
-  if List.mem s !dyntab then anomaly "Dyn.create: already declared dynamic";
+  if List.mem s !dyntab then 
+    anomaly ("Dyn.create: already declared dynamic " ^ s);
   dyntab := s :: !dyntab;
   ((fun v -> (s,Obj.repr v)),
    (fun (s',rv) ->
diff --git a/lib/options.ml b/lib/options.ml
new file mode 100644
index 0000000000..4e8597aaf5
--- /dev/null
+++ b/lib/options.ml
@@ -0,0 +1,26 @@
+
+(* $Id$ *)
+
+let batch_mode = ref false
+
+let debug = ref false
+
+let print_emacs = ref false
+
+let emacs_str s = if !print_emacs then s else "" 
+
+(* Silent *)
+let silent = ref false
+let make_silent flag = silent := flag; ()
+let is_silent () = !silent
+
+let silently f x =
+  let oldsilent = !silent in
+  try 
+    silent := true;
+    let rslt = f x in
+    silent := oldsilent; 
+    rslt
+  with e -> begin
+    silent := oldsilent; raise e
+  end
diff --git a/lib/options.mli b/lib/options.mli
new file mode 100644
index 0000000000..2d2a566bf0
--- /dev/null
+++ b/lib/options.mli
@@ -0,0 +1,16 @@
+
+(* $Id$ *)
+
+(* Global options of the system. *)
+
+val batch_mode : bool ref
+
+val debug : bool ref
+
+val print_emacs : bool ref
+val emacs_str : string -> string
+
+val make_silent : bool -> unit
+val is_silent : unit -> bool
+val silently : ('a -> 'b) -> 'a -> 'b
+
diff --git a/lib/system.mli b/lib/system.mli
index f89e128cbc..6b773fdefc 100644
--- a/lib/system.mli
+++ b/lib/system.mli
@@ -8,6 +8,8 @@ val del_path : string -> unit
 
 val find_file_in_path : string -> string
 
+val make_suffix : string -> string -> string
+
 (*s Generic input and output functions, parameterized by a magic number
   and a suffix. The intern functions raise the exception [Bad_magic_number]
   when the check fails, with the full file name. *)
diff --git a/lib/util.ml b/lib/util.ml
index 8e3eb881f6..b010e5e0c8 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -247,6 +247,11 @@ type ('a,'b) union = Inl of 'a | Inr of 'b
 
 module Intset = Set.Make(struct type t = int let compare = compare end)
 
+let out_some = function
+  | Some x -> x
+  | None -> failwith "out_some"
+
+
 let option_app f = function
   | None -> None
   | Some x -> Some (f x)
diff --git a/lib/util.mli b/lib/util.mli
index c8f3eb6db7..b7596e4399 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -72,6 +72,7 @@ type ('a,'b) union = Inl of 'a | Inr of 'b
 
 module Intset : Set.S with type elt = int
 
+val out_some : 'a option -> 'a
 val option_app : ('a -> 'b) -> 'a option -> 'b option
 
 (*s Pretty-printing. *)