X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fmatita%2FmatitaMisc.ml;h=c0277ea46c8c62d89872ea59c1998603f8eb2e9b;hb=619a3a478a4f6b0a50782b620009f6a141c30a53;hp=acaf2123c68690ef7edef457c8b326df963a5e98;hpb=ced6c94c59ba147abbee642dcd3e816ee2e1c1eb;p=helm.git diff --git a/helm/matita/matitaMisc.ml b/helm/matita/matitaMisc.ml index acaf2123c..c0277ea46 100644 --- a/helm/matita/matitaMisc.ml +++ b/helm/matita/matitaMisc.ml @@ -26,6 +26,8 @@ open Printf open MatitaTypes +let safe_remove fname = if Sys.file_exists fname then Sys.remove fname + let is_dir fname = try (Unix.stat fname).Unix.st_kind = Unix.S_DIR @@ -44,6 +46,15 @@ let input_file fname = close_in ic; Buffer.contents buf +let output_file data file = + let oc = open_out file in + output_string oc data; + close_out oc + + +let absolute_path file = + if file.[0] = '/' then file else Unix.getcwd () ^ "/" ^ file + let is_proof_script fname = true (** TODO Zack *) let is_proof_object fname = true (** TODO Zack *) @@ -191,7 +202,7 @@ let get_proof_context status = | _ -> [] let get_proof_aliases status = status.aliases - + let qualify status name = get_string_option status "baseuri" ^ "/" ^ name let unopt = function None -> failwith "unopt: None" | Some v -> v