X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaMisc.ml;h=97d6cac4738b2b0a12c53ceaaad7cfc99d19dda5;hb=cfda0acfce3f5e0b843bfe2b7ba7c371e5690db0;hp=e3aadd5b5a616d143c17dd22ab71d25f7ac06626;hpb=650e3b3c9ff0b9cafb76a0edf8139a53446937ba;p=helm.git diff --git a/helm/matita/matitaMisc.ml b/helm/matita/matitaMisc.ml index e3aadd5b5..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 @@ -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 @@ -273,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