# HG changeset patch # User wenzelm # Date 1117963884 -7200 # Node ID 28803c418b59c2a073b9376a96317c7bf3e91664 # Parent 4a1f36eafe17e681fc509b464319c240e63f3aff removed sysify_path, quote_sysity_path etc.; added platform_path, shell_path etc.; improved copy: support dir as target; added copy_dir; added isatool; tuned; diff -r 4a1f36eafe17 -r 28803c418b59 src/Pure/General/file.ML --- a/src/Pure/General/file.ML Sun Jun 05 11:31:23 2005 +0200 +++ b/src/Pure/General/file.ML Sun Jun 05 11:31:24 2005 +0200 @@ -7,23 +7,27 @@ signature FILE = sig - val sys_pack_fn: (Path.T -> string) ref - val sys_unpack_fn: (string -> Path.T) ref - val sysify_path: Path.T -> string - val quote_sysify_path: Path.T -> string - val rm: Path.T -> unit + val unpack_platform_path_fn: (string -> Path.T) ref + val unpack_platform_path: string -> Path.T + val platform_path_fn: (Path.T -> string) ref + val platform_path: Path.T -> string + val shell_path_fn: (Path.T -> string) ref + val shell_path: Path.T -> string val cd: Path.T -> unit val pwd: unit -> Path.T val full_path: Path.T -> Path.T val tmp_path: Path.T -> Path.T + val isatool: string -> int + val system_command: string -> unit val read: Path.T -> string val write: Path.T -> string -> unit val append: Path.T -> string -> unit - val system_command: string -> unit val copy: Path.T -> Path.T -> unit + val copy_dir: Path.T -> Path.T -> unit eqtype info val info: Path.T -> info option val exists: Path.T -> bool + val rm: Path.T -> unit val mkdir: Path.T -> unit val use: Path.T -> unit end; @@ -31,35 +35,35 @@ structure File: FILE = struct - -(* system path representations (default: Unix) *) +(* platform specific path representations *) -val sys_pack_fn = ref Path.pack; -val sys_unpack_fn = ref Path.unpack; +val unpack_platform_path_fn = ref Path.unpack; +fun unpack_platform_path s = ! unpack_platform_path_fn s; -fun sysify_path path = ! sys_pack_fn (Path.expand path); -val quote_sysify_path = enclose "'" "'" o sysify_path; -fun unsysify_path s = ! sys_unpack_fn s; +val platform_path_fn = ref (Path.pack o Path.expand); +fun platform_path path = ! platform_path_fn path; -val rm = OS.FileSys.remove o sysify_path; +val shell_path_fn = ref (enclose "'" "'" o Path.pack o Path.expand); +fun shell_path path = ! shell_path_fn path; (* current path *) -val cd = Library.cd o sysify_path; -val pwd = unsysify_path o Library.pwd; +val cd = Library.cd o platform_path; +val pwd = unpack_platform_path o Library.pwd; fun norm_absolute p = let val p' = pwd (); fun norm p = if can cd p then pwd () else Path.append (norm (Path.dir p)) (Path.base p); - val p'' = norm p + val p'' = norm p; in (cd p'; p'') end -fun full_path path = norm_absolute +fun full_path path = (if Path.is_absolute path then path - else Path.append (pwd ()) path); + else Path.append (pwd ()) path) + |> norm_absolute; (* tmp_path *) @@ -68,48 +72,65 @@ Path.append (Path.variable "ISABELLE_TMP") (Path.base path); +(* system commands *) + +fun isatool cmd = system ("\"$ISATOOL\" " ^ cmd); + +fun system_command cmd = + if system cmd <> 0 then error ("System command failed: " ^ cmd) + else (); + + +(* directory entries *) + +datatype info = Info of string; + +fun info path = + Option.map (Info o Time.toString) (try OS.FileSys.modTime (platform_path path)); + +val exists = is_some o info; + +val rm = OS.FileSys.remove o platform_path; + +fun mkdir path = system_command ("mkdir -p " ^ shell_path path); + +fun is_dir path = + if_none (try OS.FileSys.isDir (platform_path path)) false; + + (* read / write files *) +local + fun fail_safe f g x = let val y = f x handle exn => (g x; raise exn) in g x; y end; - fun output txt stream = TextIO.output (stream, txt); -fun read path = fail_safe TextIO.inputAll TextIO.closeIn (TextIO.openIn (sysify_path path)); -fun write path txt = fail_safe (output txt) TextIO.closeOut (TextIO.openOut (sysify_path path)); -fun append path txt = - fail_safe (output txt) TextIO.closeOut (TextIO.openAppend (sysify_path path)); +in -fun copy inpath outpath = write outpath (read inpath); - +fun read path = + fail_safe TextIO.inputAll TextIO.closeIn (TextIO.openIn (platform_path path)); -(* file info *) - -datatype info = Info of string; +fun write path txt = + fail_safe (output txt) TextIO.closeOut (TextIO.openOut (platform_path path)); -fun info path = - let val name = sysify_path path in - (case file_info name of - "" => NONE - | s => SOME (Info s)) - end; +fun append path txt = + fail_safe (output txt) TextIO.closeOut (TextIO.openAppend (platform_path path)); -val exists = is_some o info; +end; - -(* directories *) +fun copy from to = + let val target = if is_dir to then Path.append to (Path.base from) else to + in write target (read from) end; -fun system_command cmd = - if system cmd <> 0 then error ("System command failed: " ^ cmd) - else (); - -fun mkdir path = system_command ("mkdir -p " ^ quote_sysify_path path); +fun copy_dir from to = + system_command ("cp -r " ^ shell_path from ^ "/. " ^ shell_path to); (* use ML files *) -val use = use o sysify_path; +val use = use o platform_path; end;