--- a/src/HOL/Tools/Nitpick/kodkod.ML Sat Nov 27 14:32:08 2010 +0100
+++ b/src/HOL/Tools/Nitpick/kodkod.ML Sat Nov 27 15:28:00 2010 +0100
@@ -983,7 +983,7 @@
let
val dir = getenv "ISABELLE_TMP"
val _ = if !created_temp_dir then ()
- else (created_temp_dir := true; File.mkdir (Path.explode dir))
+ else (created_temp_dir := true; Isabelle_System.mkdirs (Path.explode dir))
in (serial_string (), dir) end
(* The fudge term below is to account for Kodkodi's slow start-up time, which
--- a/src/Pure/General/file.ML Sat Nov 27 14:32:08 2010 +0100
+++ b/src/Pure/General/file.ML Sat Nov 27 15:28:00 2010 +0100
@@ -13,13 +13,9 @@
val pwd: unit -> Path.T
val full_path: Path.T -> Path.T
val tmp_path: Path.T -> Path.T
- val isabelle_tool: string -> string -> int
val exists: Path.T -> bool
val check: Path.T -> unit
val rm: Path.T -> unit
- val rm_tree: Path.T -> unit
- val mkdir: Path.T -> unit
- val mkdir_leaf: Path.T -> unit
val open_input: (TextIO.instream -> 'a) -> Path.T -> 'a
val open_output: (TextIO.outstream -> 'a) -> Path.T -> 'a
val open_append: (TextIO.outstream -> 'a) -> Path.T -> 'a
@@ -32,7 +28,6 @@
val write_buffer: Path.T -> Buffer.T -> unit
val eq: Path.T * Path.T -> bool
val copy: Path.T -> Path.T -> unit
- val copy_dir: Path.T -> Path.T -> unit
end;
structure File: FILE =
@@ -62,25 +57,6 @@
Path.append (Path.variable "ISABELLE_TMP") (Path.base path);
-(* system commands *)
-
-fun isabelle_tool name args =
- (case space_explode ":" (getenv "ISABELLE_TOOLS") |> get_first (fn dir =>
- let val path = dir ^ "/" ^ name in
- if can OS.FileSys.modTime path andalso
- not (OS.FileSys.isDir path) andalso
- OS.FileSys.access (path, [OS.FileSys.A_READ, OS.FileSys.A_EXEC])
- then SOME path
- else NONE
- end handle OS.SysErr _ => NONE) of
- SOME path => bash (shell_quote path ^ " " ^ args)
- | NONE => (writeln ("Unknown Isabelle tool: " ^ name); 2));
-
-fun system_command cmd =
- if bash cmd <> 0 then error ("System command failed: " ^ cmd)
- else ();
-
-
(* directory entries *)
val exists = can OS.FileSys.modTime o platform_path;
@@ -91,12 +67,6 @@
val rm = OS.FileSys.remove o platform_path;
-fun rm_tree path = system_command ("rm -r " ^ shell_path path);
-
-fun mkdir path = system_command ("mkdir -p " ^ shell_path path);
-
-fun mkdir_leaf path = (check (Path.dir path); mkdir path);
-
fun is_dir path =
the_default false (try OS.FileSys.isDir (platform_path path));
@@ -163,8 +133,4 @@
let val target = if is_dir dst then Path.append dst (Path.base src) else dst
in write target (read src) end;
-fun copy_dir src dst =
- if eq (src, dst) then ()
- else (system_command ("cp -r -f " ^ shell_path src ^ "/. " ^ shell_path dst); ());
-
end;
--- a/src/Pure/IsaMakefile Sat Nov 27 14:32:08 2010 +0100
+++ b/src/Pure/IsaMakefile Sat Nov 27 15:28:00 2010 +0100
@@ -188,6 +188,7 @@
Syntax/syntax.ML \
Syntax/type_ext.ML \
System/isabelle_process.ML \
+ System/isabelle_system.ML \
System/isar.ML \
System/session.ML \
Thy/html.ML \
--- a/src/Pure/Isar/isar_cmd.ML Sat Nov 27 14:32:08 2010 +0100
+++ b/src/Pure/Isar/isar_cmd.ML Sat Nov 27 15:28:00 2010 +0100
@@ -291,11 +291,11 @@
fun display_drafts files = Toplevel.imperative (fn () =>
let val outfile = File.shell_path (Present.drafts (getenv "ISABELLE_DOC_FORMAT") files)
- in File.isabelle_tool "display" ("-c " ^ outfile ^ " &"); () end);
+ in Isabelle_System.isabelle_tool "display" ("-c " ^ outfile ^ " &"); () end);
fun print_drafts files = Toplevel.imperative (fn () =>
let val outfile = File.shell_path (Present.drafts "ps" files)
- in File.isabelle_tool "print" ("-c " ^ outfile); () end);
+ in Isabelle_System.isabelle_tool "print" ("-c " ^ outfile); () end);
(* print parts of theory and proof context *)
--- a/src/Pure/ROOT.ML Sat Nov 27 14:32:08 2010 +0100
+++ b/src/Pure/ROOT.ML Sat Nov 27 15:28:00 2010 +0100
@@ -233,6 +233,7 @@
use "Isar/toplevel.ML";
(*theory documents*)
+use "System/isabelle_system.ML";
use "Thy/present.ML";
use "Thy/term_style.ML";
use "Thy/thy_output.ML";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/System/isabelle_system.ML Sat Nov 27 15:28:00 2010 +0100
@@ -0,0 +1,51 @@
+(* Title: Pure/System/isabelle_system.ML
+ Author: Makarius
+
+Isabelle system support.
+*)
+
+signature ISABELLE_SYSTEM =
+sig
+ val isabelle_tool: string -> string -> int
+ val rm_tree: Path.T -> unit
+ val mkdirs: Path.T -> unit
+ val mkdir_leaf: Path.T -> unit
+ val copy_dir: Path.T -> Path.T -> unit
+end;
+
+structure Isabelle_System: ISABELLE_SYSTEM =
+struct
+
+(* system commands *)
+
+fun isabelle_tool name args =
+ (case space_explode ":" (getenv "ISABELLE_TOOLS") |> get_first (fn dir =>
+ let val path = dir ^ "/" ^ name in
+ if can OS.FileSys.modTime path andalso
+ not (OS.FileSys.isDir path) andalso
+ OS.FileSys.access (path, [OS.FileSys.A_READ, OS.FileSys.A_EXEC])
+ then SOME path
+ else NONE
+ end handle OS.SysErr _ => NONE) of
+ SOME path => bash (File.shell_quote path ^ " " ^ args)
+ | NONE => (writeln ("Unknown Isabelle tool: " ^ name); 2));
+
+fun system_command cmd =
+ if bash cmd <> 0 then error ("System command failed: " ^ cmd)
+ else ();
+
+
+(* directory operations *)
+
+fun rm_tree path = system_command ("rm -r " ^ File.shell_path path);
+
+fun mkdirs path = system_command ("mkdir -p " ^ File.shell_path path);
+
+fun mkdir_leaf path = (File.check (Path.dir path); mkdirs path); (* FIXME ? *)
+
+fun copy_dir src dst =
+ if File.eq (src, dst) then ()
+ else (system_command ("cp -r -f " ^ File.shell_path src ^ "/. " ^ File.shell_path dst); ());
+
+end;
+
--- a/src/Pure/Thy/present.ML Sat Nov 27 14:32:08 2010 +0100
+++ b/src/Pure/Thy/present.ML Sat Nov 27 15:28:00 2010 +0100
@@ -94,7 +94,7 @@
val _ = writeln "Displaying graph ...";
val path = File.tmp_path (Path.explode "tmp.graph");
val _ = write_graph gr path;
- val _ = File.isabelle_tool "browser" ("-c " ^ File.shell_path path ^ " &");
+ val _ = Isabelle_System.isabelle_tool "browser" ("-c " ^ File.shell_path path ^ " &");
in () end;
@@ -344,7 +344,7 @@
val args = "-o " ^ File.shell_path pdf_path ^ " " ^ File.shell_path gr_path;
in
write_graph graph gr_path;
- if File.isabelle_tool "browser" args <> 0 orelse
+ if Isabelle_System.isabelle_tool "browser" args <> 0 orelse
not (File.exists eps_path) orelse not (File.exists pdf_path)
then error "Failed to prepare dependency graph"
else
@@ -384,9 +384,9 @@
else NONE;
fun prepare_sources cp path =
- (File.mkdir path;
- if cp then File.copy_dir document_path path else ();
- File.isabelle_tool "latex"
+ (Isabelle_System.mkdirs path;
+ if cp then Isabelle_System.copy_dir document_path path else ();
+ Isabelle_System.isabelle_tool "latex"
("-o sty " ^ File.shell_path (Path.append path (Path.basic "root.tex")));
(case opt_graphs of NONE => () | SOME (pdf, eps) =>
(File.write (Path.append path graph_pdf_path) pdf;
@@ -395,14 +395,14 @@
List.app (finish_tex path) thys);
in
if info then
- (File.mkdir (Path.append html_prefix session_path);
+ (Isabelle_System.mkdirs (Path.append html_prefix session_path);
File.write_buffer (Path.append html_prefix pre_index_path) (index_buffer html_index);
File.write (Path.append html_prefix session_entries_path) "";
create_index html_prefix;
if length path > 1 then update_index parent_html_prefix name else ();
(case readme of NONE => () | SOME path => File.copy path html_prefix);
write_graph sorted_graph (Path.append html_prefix graph_path);
- File.isabelle_tool "browser" "-b";
+ Isabelle_System.isabelle_tool "browser" "-b";
File.copy (Path.explode "~~/lib/browser/GraphBrowser.jar") html_prefix;
List.app (fn (a, txt) => File.write (Path.append html_prefix (Path.basic a)) txt)
(HTML.applet_pages name (Url.File index_path, name));
@@ -509,11 +509,11 @@
val doc_path = File.tmp_path document_path;
val result_path = Path.append doc_path Path.parent;
- val _ = File.mkdir doc_path;
+ val _ = Isabelle_System.mkdirs doc_path;
val root_path = Path.append doc_path (Path.basic "root.tex");
val _ = File.copy (Path.explode "~~/lib/texinputs/draft.tex") root_path;
- val _ = File.isabelle_tool "latex" ("-o sty " ^ File.shell_path root_path);
- val _ = File.isabelle_tool "latex" ("-o syms " ^ File.shell_path root_path);
+ val _ = Isabelle_System.isabelle_tool "latex" ("-o sty " ^ File.shell_path root_path);
+ val _ = Isabelle_System.isabelle_tool "latex" ("-o syms " ^ File.shell_path root_path);
fun known name =
let val ss = split_lines (File.read (Path.append doc_path (Path.basic name)))
--- a/src/Tools/Code/code_haskell.ML Sat Nov 27 14:32:08 2010 +0100
+++ b/src/Tools/Code/code_haskell.ML Sat Nov 27 15:28:00 2010 +0100
@@ -353,7 +353,7 @@
val _ = File.check destination;
val filepath = (Path.append destination o Path.ext "hs" o Path.explode o implode
o separate "/" o Long_Name.explode) module_name;
- val _ = File.mkdir_leaf (Path.dir filepath);
+ val _ = Isabelle_System.mkdir_leaf (Path.dir filepath);
in
(File.write filepath o format [] width o Pretty.chunks2)
[str "{-# OPTIONS_GHC -fglasgow-exts #-}", content]
--- a/src/Tools/cache_io.ML Sat Nov 27 14:32:08 2010 +0100
+++ b/src/Tools/cache_io.ML Sat Nov 27 15:28:00 2010 +0100
@@ -44,9 +44,9 @@
fun with_tmp_dir name f =
let
val path = File.tmp_path (Path.explode (name ^ serial_string ()))
- val _ = File.mkdir path
+ val _ = Isabelle_System.mkdirs path
val x = Exn.capture f path
- val _ = try File.rm_tree path
+ val _ = try Isabelle_System.rm_tree path
in Exn.release x end
type result = {