X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fextlib%2FhExtlib.ml;h=24f0dd1967ab3f8711a5538f61058bcc13417fce;hb=249d11773d32add20d665c4f8521b7380e4fec0a;hp=bf3bb2574b7608327129d235974d74f7c4d0f48f;hpb=6dc612f46d3b237d8da9f09b7984e6aa0ddec433;p=helm.git diff --git a/components/extlib/hExtlib.ml b/components/extlib/hExtlib.ml index bf3bb2574..24f0dd196 100644 --- a/components/extlib/hExtlib.ml +++ b/components/extlib/hExtlib.ml @@ -236,6 +236,9 @@ let is_executable fname = (stat.Unix.st_perm land 0o001 > 0) with Unix.Unix_error _ -> false +let chmod mode filename = + Unix.chmod filename mode + let mkdir path = let components = split ~sep:'/' path in let rec aux where = function @@ -244,21 +247,18 @@ let mkdir path = let path = if where = "" then piece else where ^ "/" ^ piece in (try - Unix.mkdir path 0o775 + Unix.mkdir path 0o755; chmod 0o2775 path with | Unix.Unix_error (Unix.EEXIST,_,_) -> () | Unix.Unix_error (e,_,_) -> raise (Failure - ("Unix.mkdir " ^ path ^ " 0o775 :" ^ (Unix.error_message e)))); + ("Unix.mkdir " ^ path ^ " 0o2775 :" ^ (Unix.error_message e)))); aux path tl in let where = if path.[0] = '/' then "/" else "" in aux where components -let chmod mode filename = - Unix.chmod filename mode - (** {2 Filesystem} *) let input_file fname = @@ -403,30 +403,20 @@ let finally at_end f arg = (** {2 Localized exceptions } *) -exception Localized of Token.flocation * exn +exception Localized of Stdpp.location * exn -let loc_of_floc = function - | { Lexing.pos_cnum = loc_begin }, { Lexing.pos_cnum = loc_end } -> - (loc_begin, loc_end) +let loc_of_floc floc = Stdpp.first_pos floc, Stdpp.last_pos floc;; let floc_of_loc (loc_begin, loc_end) = - let floc_begin = - { Lexing.pos_fname = ""; Lexing.pos_lnum = -1; Lexing.pos_bol = -1; - Lexing.pos_cnum = loc_begin } - in - let floc_end = { floc_begin with Lexing.pos_cnum = loc_end } in - (floc_begin, floc_end) + Stdpp.make_loc (loc_begin, loc_end) let dummy_floc = floc_of_loc (-1, -1) let raise_localized_exception ~offset floc exn = - let (x, y) = loc_of_floc floc in + let x, y = loc_of_floc floc in let x = offset + x in let y = offset + y in - let flocb,floce = floc in - let floc = - { flocb with Lexing.pos_cnum = x }, { floce with Lexing.pos_cnum = y } - in + let floc = floc_of_loc (x,y) in raise (Localized (floc, exn)) let estimate_size x =