# HG changeset patch
# User wenzelm
# Date 1290868080 -3600
# Node ID b07a0dbc8a385b33ed4c836fc9ca325e9a48646e
# Parent  dc6439c0b8b1a6b0f60f7b332e32c6ba3190ac1f
more explicit Isabelle_System operations;

diff -r dc6439c0b8b1 -r b07a0dbc8a38 src/HOL/Tools/Nitpick/kodkod.ML
--- 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
diff -r dc6439c0b8b1 -r b07a0dbc8a38 src/Pure/General/file.ML
--- 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;
diff -r dc6439c0b8b1 -r b07a0dbc8a38 src/Pure/IsaMakefile
--- 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						\
diff -r dc6439c0b8b1 -r b07a0dbc8a38 src/Pure/Isar/isar_cmd.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 *)
diff -r dc6439c0b8b1 -r b07a0dbc8a38 src/Pure/ROOT.ML
--- 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";
diff -r dc6439c0b8b1 -r b07a0dbc8a38 src/Pure/System/isabelle_system.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;
+
diff -r dc6439c0b8b1 -r b07a0dbc8a38 src/Pure/Thy/present.ML
--- 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)))
diff -r dc6439c0b8b1 -r b07a0dbc8a38 src/Tools/Code/code_haskell.ML
--- 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]
diff -r dc6439c0b8b1 -r b07a0dbc8a38 src/Tools/cache_io.ML
--- 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 = {