new tacticals

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

diff --git a/helm/matita/matitaMisc.ml b/helm/matita/matitaMisc.ml
index 9c0c7db33338f6a40e8bc2267d96d43324027c81..17473f38b3826029c62674fa7e8a6e23371ab928 100644 (file)
--- a/helm/matita/matitaMisc.ml
+++ b/helm/matita/matitaMisc.ml
@@ -80,6 +80,28 @@ let is_empty buri =
 
 let safe_remove fname = if Sys.file_exists fname then Sys.remove fname
 
+let is_dir_empty d =
+  try 
+    let od = Unix.opendir d in
+    try 
+      ignore (Unix.readdir od);
+      ignore (Unix.readdir od);
+      ignore (Unix.readdir od);
+      Unix.closedir od;
+      false
+    with End_of_file -> 
+      Unix.closedir od;
+      true
+  with Unix.Unix_error _ -> true
+
+let safe_rmdir d = try Unix.rmdir d with Unix.Unix_error _ -> ()
+
+let rec rmdir_descend d = 
+  if is_dir_empty d then
+    begin
+      safe_rmdir d;
+      rmdir_descend (Filename.dirname d)
+    end
 
 let absolute_path file =
   if file.[0] = '/' then file else Unix.getcwd () ^ "/" ^ file
@@ -93,13 +115,16 @@ let append_phrase_sep s =
   else
     s
 
-let empty_mathml () =
+let empty_mathml = lazy (
   DomMisc.domImpl#createDocument ~namespaceURI:(Some DomMisc.mathml_ns)
-    ~qualifiedName:(Gdome.domString "math") ~doctype:None
+    ~qualifiedName:(Gdome.domString "math") ~doctype:None)
 
-let empty_boxml () =
+let empty_boxml = lazy (
   DomMisc.domImpl#createDocument ~namespaceURI:(Some DomMisc.boxml_ns) 
-    ~qualifiedName:(Gdome.domString "box") ~doctype:None
+    ~qualifiedName:(Gdome.domString "box") ~doctype:None)
+
+let closed_goal_mathml = lazy (
+  DomMisc.domImpl#createDocumentFromURI ~uri:BuildTimeConf.closed_xml ())
 
 exception History_failure
 
@@ -195,31 +220,47 @@ let singleton f =
   let instance = lazy (f ()) in
   fun () -> Lazy.force instance
 
-let get_proof_status status =
+let get_current_proof status =
   match status.proof_status with
-  | Incomplete_proof s -> s
+  | Incomplete_proof { proof = p } -> p
   | _ -> 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
+  | Proof (_, metasenv, _, _)
+  | Incomplete_proof { proof = (_, metasenv, _, _) }
+  | Intermediate metasenv ->
+      metasenv
 
-let get_proof_context status =
+let get_proof_context status goal =
   match status.proof_status with
-  | Incomplete_proof ((_, metasenv, _, _), goal) ->
+  | Incomplete_proof { proof = (_, metasenv, _, _) } ->
       let (_, context, _) = CicUtil.lookup_meta goal metasenv in
       context
   | _ -> []
  
-let get_proof_conclusion status =
+let get_proof_conclusion status goal =
   match status.proof_status with
-  | Incomplete_proof ((_, metasenv, _, _), goal) ->
+  | Incomplete_proof { proof = (_, metasenv, _, _) } ->
       let (_, _, conclusion) = CicUtil.lookup_meta goal metasenv in
       conclusion
   | _ -> statement_error "no ongoing proof"
+
+let get_stack status =
+  match status.proof_status with
+  | Incomplete_proof p -> p.stack
+  | Proof _ -> Continuationals.Stack.empty
+  | _ -> assert false
+
+let set_stack stack status =
+  match status.proof_status with
+  | Incomplete_proof p ->
+      { status with proof_status = Incomplete_proof { p with stack = stack } }
+  | Proof _ ->
+      assert (Continuationals.Stack.is_empty stack);
+      status
+  | _ -> assert false
  
 let qualify status name = get_string_option status "baseuri" ^ "/" ^ name
 
@@ -239,12 +280,6 @@ let obj_file_of_script f =
   let baseuri = baseuri_of_file f in
    obj_file_of_baseuri baseuri
 
-let rec list_uniq = function 
-  | [] -> []
-  | h::[] -> [h]
-  | h1::h2::tl when h1 = h2 -> list_uniq (h2 :: tl) 
-  | h1::tl (* when h1 <> h2 *) -> h1 :: list_uniq tl
-
 let list_tl_at ?(equality=(==)) e l =
   let rec aux =
     function