X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=helm%2Fmatita%2FmatitaMisc.ml;h=97d6cac4738b2b0a12c53ceaaad7cfc99d19dda5;hb=29a5b18f3da1a3ed648f23709384b7789cb099bf;hp=9ddc268a815265d336cd43348b16caa8b6f5d451;hpb=f37481ee495d25d2e0a0feb1cdf6e443d3e4530c;p=helm.git

diff --git a/helm/matita/matitaMisc.ml b/helm/matita/matitaMisc.ml
index 9ddc268a8..97d6cac47 100644
--- a/helm/matita/matitaMisc.ml
+++ b/helm/matita/matitaMisc.ml
@@ -26,9 +26,11 @@
 open Printf
 open MatitaTypes 
 
-let strip_trailing_slash =
-  let rex = Pcre.regexp "/$" in
-  fun s -> Pcre.replace ~rex s
+(** Functions "imported" from Http_getter_misc *)
+
+let strip_trailing_slash = Http_getter_misc.strip_trailing_slash
+let normalize_dir = Http_getter_misc.normalize_dir
+let strip_suffix = Http_getter_misc.strip_suffix
 
 let baseuri_of_baseuri_decl st =
   match st with
@@ -121,7 +123,7 @@ let mkdir path =
     | piece::tl -> 
         let path = where ^ "/" ^ piece in
         (try
-          Unix.mkdir path 755
+          Unix.mkdir path 0o755
         with 
         | Unix.Unix_error (Unix.EEXIST,_,_) -> ()
         | Unix.Unix_error (e,_,_) -> raise (Failure (Unix.error_message e)));
@@ -129,9 +131,9 @@ let mkdir path =
   in
   aux "" components
 
-let strip_trailing_blanks =
-  let rex = Pcre.regexp "\\s*$" in
-  fun s -> Pcre.replace ~rex s
+let trim_blanks =
+  let rex = Pcre.regexp "^\\s*(.*?)\\s*$" in
+  fun s -> (Pcre.extract ~rex s).(1)
 
 let split ?(char = ' ') s =
   let pieces = ref [] in
@@ -246,26 +248,7 @@ class ['a] browser_history ?memento size init =
 let singleton f =
   let instance = lazy (f ()) in
   fun () -> Lazy.force instance
-(*
-let mkdir d =
-  let errmsg = sprintf "Unable to create directory \"%s\"" d in
-  try
-    let dir = "mkdir -p " ^ d in 
-    (match Unix.system dir with
-    | Unix.WEXITED 0 -> ()
-    | Unix.WEXITED n -> 
-        MatitaLog.error ("'mkdir -p " ^ dir ^ "' failed with "^string_of_int n);
-        failwith errmsg
-    | Unix.WSIGNALED s 
-    | Unix.WSTOPPED s -> 
-        MatitaLog.error 
-          ("'mkdir -p " ^ dir ^ "' signaled with " ^ string_of_int s);
-        failwith errmsg)
-  with Unix.Unix_error _ as exc -> 
-    MatitaLog.error 
-      ("Unix error in makigin dir " ^ (MatitaExcPp.to_string exc));
-    failwith errmsg
-*)
+
 let get_proof_status status =
   match status.proof_status with
   | Incomplete_proof s -> s
@@ -292,8 +275,6 @@ let get_proof_conclusion status =
       conclusion
   | _ -> statement_error "no ongoing proof"
  
-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
@@ -310,8 +291,9 @@ let obj_file_of_baseuri baseuri =
   path ^ ".moo"
 
 let obj_file_of_script f =
- let baseuri = baseuri_of_file f in
-  obj_file_of_baseuri baseuri
+ if f = "coq.ma" then BuildTimeConf.coq_notation_script else
+  let baseuri = baseuri_of_file f in
+   obj_file_of_baseuri baseuri
 
 let rec list_uniq = function 
   | [] -> []