checked in new version of matita from svn

[helm.git] / helm / matita / matitaMisc.ml

diff --git a/helm/matita/matitaMisc.ml b/helm/matita/matitaMisc.ml
index 094f965e0ae20d02aff1ae0130d82899b4d729a3..58fa388091e7c165ff76783141c82e6d55efd798 100644 (file)
--- a/helm/matita/matitaMisc.ml
+++ b/helm/matita/matitaMisc.ml
@@ -1,4 +1,4 @@
-(* Copyright (C) 2004, HELM Team.
+(* Copyright (C) 2004-2005, HELM Team.
  * 
  * This file is part of HELM, an Hypertextual, Electronic
  * Library of Mathematics, developed at the Computer Science
@@ -24,9 +24,17 @@
  *)
 
 open Printf
+open MatitaTypes 
 
-let is_dir fname = (Unix.stat fname).Unix.st_kind = Unix.S_DIR
-let is_regular fname = (Unix.stat fname).Unix.st_kind = Unix.S_REG
+let is_dir fname =
+  try
+    (Unix.stat fname).Unix.st_kind = Unix.S_DIR
+  with Unix.Unix_error _ -> false
+
+let is_regular fname =
+  try
+    (Unix.stat fname).Unix.st_kind = Unix.S_REG
+  with Unix.Unix_error _ -> false
 
 let input_file fname =
   let size = (Unix.stat fname).Unix.st_size in
@@ -131,19 +139,38 @@ class ['a] browser_history ?memento size init =
     method save = (Array.copy data, hd, tl, cur)
   end
 
-let dbd_instance =
-  let dbd = lazy (
-    Mysql.quick_connect
-      ~host:(Helm_registry.get "db.host")
-      ~user:(Helm_registry.get "db.user")
-      ~database:(Helm_registry.get "db.database")
-      ())
-  in
-  fun () -> Lazy.force dbd
-
 let singleton f =
   let instance = lazy (f ()) in
   fun () -> Lazy.force instance
 
-let mkdirs = List.iter (fun d -> ignore (Unix.system ("mkdir -p " ^ d)))
+let mkdir d =
+  let errmsg = sprintf "Unable to create directory \"%s\"" d in
+  try
+    (match Unix.system ("mkdir -p " ^ d) with
+    | Unix.WEXITED 0 -> ()
+    | _ -> failwith errmsg)
+  with Unix.Unix_error _ -> failwith errmsg
+
+let get_proof_status status =
+  match status.proof_status with
+  | Incomplete_proof s -> s
+  | _ -> statement_error "no ongoing proof"
+
+let get_proof_metasenv status =
+  match status.proof_status with
+  | No_proof -> []
+  | Incomplete_proof ((_, metasenv, _, _), _) -> metasenv
+  | Proof (_, metasenv, _, _) -> metasenv
+  | Intermediate m -> m
+
+let get_proof_context status =
+  match status.proof_status with
+  | Incomplete_proof ((_, metasenv, _, _), goal) ->
+      let (_, context, _) = CicUtil.lookup_meta goal metasenv in
+      context
+  | _ -> []
+  
+let qualify status name = get_string_option status "baseuri" ^ "/" ^ name
+
+let unopt = function None -> failwith "unopt: None" | Some v -> v