# HG changeset patch
# User wenzelm
# Date 1290887286 -3600
# Node ID 782399904d9cc97b8cfe6f5754c59740d2745366
# Parent  d73659e8ccdd4ff1f193b0668d2b2b62d15ef9d1# Parent  2064991db2aced26b155b7064861cf7789bc1cd0
merged

diff -r d73659e8ccdd -r 782399904d9c src/HOL/Tools/Nitpick/kodkod.ML
--- a/src/HOL/Tools/Nitpick/kodkod.ML	Sat Nov 27 18:51:15 2010 +0100
+++ b/src/HOL/Tools/Nitpick/kodkod.ML	Sat Nov 27 20:48:06 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 d73659e8ccdd -r 782399904d9c src/Pure/Concurrent/bash.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Concurrent/bash.ML	Sat Nov 27 20:48:06 2010 +0100
@@ -0,0 +1,83 @@
+(*  Title:      Pure/Concurrent/bash.ML
+    Author:     Makarius
+
+GNU bash processes, with propagation of interrupts.
+*)
+
+val bash_output = uninterruptible (fn restore_attributes => fn script =>
+  let
+    datatype result = Wait | Signal | Result of int;
+    val result = Synchronized.var "bash_result" Wait;
+
+    val id = serial_string ();
+    val script_path = File.tmp_path (Path.basic ("bash_script" ^ id));
+    val output_path = File.tmp_path (Path.basic ("bash_output" ^ id));
+    val pid_path = File.tmp_path (Path.basic ("bash_pid" ^ id));
+
+    val system_thread =
+      Simple_Thread.fork false (fn () =>
+        Multithreading.with_attributes Multithreading.private_interrupts (fn _ =>
+          let
+            val _ = File.write script_path script;
+            val status =
+              OS.Process.system
+                ("exec \"$ISABELLE_HOME/lib/scripts/process\" group " ^
+                  File.shell_path pid_path ^ " script \"exec bash " ^
+                  File.shell_path script_path ^ " > " ^
+                  File.shell_path output_path ^ "\"");
+            val res =
+              (case Posix.Process.fromStatus status of
+                Posix.Process.W_EXITED => Result 0
+              | Posix.Process.W_EXITSTATUS 0wx82 => Signal
+              | Posix.Process.W_EXITSTATUS w => Result (Word8.toInt w)
+              | Posix.Process.W_SIGNALED s =>
+                  if s = Posix.Signal.int then Signal
+                  else Result (256 + LargeWord.toInt (Posix.Signal.toWord s))
+              | Posix.Process.W_STOPPED s =>
+                  Result (512 + LargeWord.toInt (Posix.Signal.toWord s)));
+          in Synchronized.change result (K res) end
+          handle _ (*sic*) => Synchronized.change result (fn Wait => Signal | res => res)));
+
+    fun terminate () =
+      let
+        val sig_test = Posix.Signal.fromWord 0w0;
+
+        fun kill_group pid s =
+          (Posix.Process.kill
+            (Posix.Process.K_GROUP (Posix.Process.wordToPid (LargeWord.fromInt pid)), s); true)
+          handle OS.SysErr _ => false;
+
+        fun kill s =
+          (case Int.fromString (File.read pid_path) of
+            NONE => true
+          | SOME pid => (kill_group pid s; kill_group pid sig_test))
+          handle IO.Io _ => true;
+
+        fun multi_kill count s =
+          count = 0 orelse
+            kill s andalso (OS.Process.sleep (seconds 0.1); multi_kill (count - 1) s);
+        val _ =
+          multi_kill 10 Posix.Signal.int andalso
+          multi_kill 10 Posix.Signal.term andalso
+          multi_kill 10 Posix.Signal.kill;
+      in () end;
+
+    fun cleanup () =
+     (terminate ();
+      Simple_Thread.interrupt system_thread;
+      try File.rm script_path;
+      try File.rm output_path;
+      try File.rm pid_path);
+  in
+    let
+      val _ =
+        restore_attributes (fn () =>
+          Synchronized.guarded_access result (fn Wait => NONE | x => SOME ((), x))) ();
+
+      val output = the_default "" (try File.read output_path);
+      val rc = (case Synchronized.value result of Signal => Exn.interrupt () | Result rc => rc);
+      val _ = cleanup ();
+    in (output, rc) end
+    handle exn => (cleanup (); reraise exn)
+  end);
+
diff -r d73659e8ccdd -r 782399904d9c src/Pure/Concurrent/bash_sequential.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Concurrent/bash_sequential.ML	Sat Nov 27 20:48:06 2010 +0100
@@ -0,0 +1,34 @@
+(*  Title:      Pure/Concurrent/bash_sequential.ML
+    Author:     Makarius
+
+Generic GNU bash processes (no provisions to propagate interrupts, but
+could work via the controlling tty).
+*)
+
+fun bash_output script =
+  let
+    val id = serial_string ();
+    val script_path = File.tmp_path (Path.basic ("bash_script" ^ id));
+    val output_path = File.tmp_path (Path.basic ("bash_output" ^ id));
+    fun cleanup () = (try File.rm script_path; try File.rm output_path);
+  in
+    let
+      val _ = File.write script_path script;
+      val status =
+        OS.Process.system
+          ("exec \"$ISABELLE_HOME/lib/scripts/process\" no_group /dev/null" ^
+            " script \"exec bash " ^ File.shell_path script_path ^ " > " ^
+            File.shell_path output_path ^ "\"");
+      val rc =
+        (case Posix.Process.fromStatus status of
+          Posix.Process.W_EXITED => 0
+        | Posix.Process.W_EXITSTATUS w => Word8.toInt w
+        | Posix.Process.W_SIGNALED s => 256 + LargeWord.toInt (Posix.Signal.toWord s)
+        | Posix.Process.W_STOPPED s => 512 + LargeWord.toInt (Posix.Signal.toWord s));
+
+      val output = the_default "" (try File.read output_path);
+      val _ = cleanup ();
+    in (output, rc) end
+    handle exn => (cleanup (); reraise exn)
+  end;
+
diff -r d73659e8ccdd -r 782399904d9c src/Pure/General/file.ML
--- a/src/Pure/General/file.ML	Sat Nov 27 18:51:15 2010 +0100
+++ b/src/Pure/General/file.ML	Sat Nov 27 20:48:06 2010 +0100
@@ -13,16 +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
-  eqtype ident
-  val rep_ident: ident -> string
-  val ident: Path.T -> ident option
   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
@@ -35,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 =
@@ -45,7 +37,11 @@
 
 val platform_path = Path.implode o Path.expand;
 
-val shell_quote = enclose "'" "'";
+fun shell_quote s =
+  if exists_string (fn c => c = "'") s then
+    error ("Illegal single quote in path specification: " ^ quote s)
+  else enclose "'" "'" s;
+
 val shell_path = shell_quote o platform_path;
 
 
@@ -65,66 +61,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 ();
-
-
-(* file identification *)
-
-local
-  val ident_cache =
-    Unsynchronized.ref (Symtab.empty: {time_stamp: string, id: string} Symtab.table);
-in
-
-fun check_cache (path, time) =
-  (case Symtab.lookup (! ident_cache) path of
-    NONE => NONE
-  | SOME {time_stamp, id} => if time_stamp = time then SOME id else NONE);
-
-fun update_cache (path, (time, id)) = CRITICAL (fn () =>
-  Unsynchronized.change ident_cache
-    (Symtab.update (path, {time_stamp = time, id = id})));
-
-end;
-
-datatype ident = Ident of string;
-fun rep_ident (Ident s) = s;
-
-fun ident path =
-  let val physical_path = perhaps (try OS.FileSys.fullPath) (platform_path path) in
-    (case try (Time.toString o OS.FileSys.modTime) physical_path of
-      NONE => NONE
-    | SOME mod_time => SOME (Ident
-        (case getenv "ISABELLE_FILE_IDENT" of
-          "" => physical_path ^ ": " ^ mod_time
-        | cmd =>
-            (case check_cache (physical_path, mod_time) of
-              SOME id => id
-            | NONE =>
-                let val (id, rc) =  (*potentially slow*)
-                  bash_output ("\"$ISABELLE_HOME/lib/scripts/fileident\" " ^ shell_quote physical_path)
-                in
-                  if id <> "" andalso rc = 0 then (update_cache (physical_path, (mod_time, id)); id)
-                  else error ("Failed to identify file " ^ quote (Path.implode path) ^ " by " ^ cmd)
-                end))))
-  end;
-
-
 (* directory entries *)
 
 val exists = can OS.FileSys.modTime o platform_path;
@@ -135,15 +71,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));
-
 
 (* open files *)
 
@@ -201,14 +128,13 @@
     SOME ids => is_equal (OS.FileSys.compare ids)
   | NONE => false);
 
+fun is_dir path =
+  the_default false (try OS.FileSys.isDir (platform_path path));
+
 fun copy src dst =
   if eq (src, dst) then ()
   else
     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 d73659e8ccdd -r 782399904d9c src/Pure/General/secure.ML
--- a/src/Pure/General/secure.ML	Sat Nov 27 18:51:15 2010 +0100
+++ b/src/Pure/General/secure.ML	Sat Nov 27 20:48:06 2010 +0100
@@ -15,8 +15,6 @@
   val toplevel_pp: string list -> string -> unit
   val PG_setup: unit -> unit
   val commit: unit -> unit
-  val bash_output: string -> string * int
-  val bash: string -> int
 end;
 
 structure Secure: SECURE =
@@ -58,20 +56,6 @@
 fun PG_setup () =
   use_global "val change = Unsynchronized.change; structure ThyLoad = ProofGeneral.ThyLoad;";
 
-
-(* shell commands *)
-
-fun secure_shell () = deny_secure "Cannot execute shell commands in secure mode";
-
-val orig_bash_output = bash_output;
-
-fun bash_output s = (secure_shell (); orig_bash_output s);
-
-fun bash s =
-  (case bash_output s of
-    ("", rc) => rc
-  | (out, rc) => (writeln (perhaps (try (unsuffix "\n")) out); rc));
-
 end;
 
 (*override previous toplevel bindings!*)
@@ -80,5 +64,4 @@
 fun use s = Secure.use_file ML_Parse.global_context true s
   handle ERROR msg => (writeln msg; error "ML error");
 val toplevel_pp = Secure.toplevel_pp;
-val bash_output = Secure.bash_output;
-val bash = Secure.bash;
+
diff -r d73659e8ccdd -r 782399904d9c src/Pure/IsaMakefile
--- a/src/Pure/IsaMakefile	Sat Nov 27 18:51:15 2010 +0100
+++ b/src/Pure/IsaMakefile	Sat Nov 27 20:48:06 2010 +0100
@@ -22,7 +22,6 @@
 BOOTSTRAP_FILES = 					\
   General/exn.ML					\
   General/timing.ML					\
-  ML-Systems/bash.ML 					\
   ML-Systems/compiler_polyml-5.2.ML			\
   ML-Systems/compiler_polyml-5.3.ML			\
   ML-Systems/ml_name_space.ML				\
@@ -55,6 +54,8 @@
 Pure: $(OUT)/Pure
 
 $(OUT)/Pure: $(BOOTSTRAP_FILES)				\
+  Concurrent/bash.ML 					\
+  Concurrent/bash_sequential.ML				\
   Concurrent/cache.ML					\
   Concurrent/future.ML					\
   Concurrent/lazy.ML					\
@@ -188,6 +189,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 d73659e8ccdd -r 782399904d9c src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Sat Nov 27 18:51:15 2010 +0100
+++ b/src/Pure/Isar/isar_cmd.ML	Sat Nov 27 20:48:06 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 d73659e8ccdd -r 782399904d9c src/Pure/ML-Systems/bash.ML
--- a/src/Pure/ML-Systems/bash.ML	Sat Nov 27 18:51:15 2010 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,43 +0,0 @@
-(*  Title:      Pure/ML-Systems/bash.ML
-    Author:     Makarius
-
-Generic GNU bash processes (no provisions to propagate interrupts, but
-could work via the controlling tty).
-*)
-
-local
-
-fun read_file name =
-  let val is = TextIO.openIn name
-  in Exn.release (Exn.capture TextIO.inputAll is before TextIO.closeIn is) end;
-
-fun write_file name txt =
-  let val os = TextIO.openOut name
-  in Exn.release (Exn.capture TextIO.output (os, txt) before TextIO.closeOut os) end;
-
-in
-
-fun bash_output script =
-  let
-    val script_name = OS.FileSys.tmpName ();
-    val _ = write_file script_name script;
-
-    val output_name = OS.FileSys.tmpName ();
-
-    val status =
-      OS.Process.system ("exec \"$ISABELLE_HOME/lib/scripts/process\" no_group /dev/null" ^
-        " script \"exec bash " ^ script_name ^ " > " ^ output_name ^ "\"");
-    val rc =
-      (case Posix.Process.fromStatus status of
-        Posix.Process.W_EXITED => 0
-      | Posix.Process.W_EXITSTATUS w => Word8.toInt w
-      | Posix.Process.W_SIGNALED s => 256 + LargeWord.toInt (Posix.Signal.toWord s)
-      | Posix.Process.W_STOPPED s => 512 + LargeWord.toInt (Posix.Signal.toWord s));
-
-    val output = read_file output_name handle IO.Io _ => "";
-    val _ = OS.FileSys.remove script_name handle OS.SysErr _ => ();
-    val _ = OS.FileSys.remove output_name handle OS.SysErr _ => ();
-  in (output, rc) end;
-
-end;
-
diff -r d73659e8ccdd -r 782399904d9c src/Pure/ML-Systems/multithreading_polyml.ML
--- a/src/Pure/ML-Systems/multithreading_polyml.ML	Sat Nov 27 18:51:15 2010 +0100
+++ b/src/Pure/ML-Systems/multithreading_polyml.ML	Sat Nov 27 20:48:06 2010 +0100
@@ -8,7 +8,6 @@
 sig
   val interruptible: ('a -> 'b) -> 'a -> 'b
   val uninterruptible: ((('c -> 'd) -> 'c -> 'd) -> 'a -> 'b) -> 'a -> 'b
-  val bash_output: string -> string * int
   structure TimeLimit: TIME_LIMIT
 end;
 
@@ -42,20 +41,6 @@
 fun enabled () = max_threads_value () > 1;
 
 
-(* misc utils *)
-
-fun show "" = "" | show name = " " ^ name;
-fun show' "" = "" | show' name = " [" ^ name ^ "]";
-
-fun read_file name =
-  let val is = TextIO.openIn name
-  in Exn.release (Exn.capture TextIO.inputAll is before TextIO.closeIn is) end;
-
-fun write_file name txt =
-  let val os = TextIO.openOut name
-  in Exn.release (Exn.capture TextIO.output (os, txt) before TextIO.closeOut os) end;
-
-
 (* thread attributes *)
 
 val no_interrupts =
@@ -156,71 +141,6 @@
 end;
 
 
-(* GNU bash processes, with propagation of interrupts *)
-
-fun bash_output script = with_attributes no_interrupts (fn orig_atts =>
-  let
-    val script_name = OS.FileSys.tmpName ();
-    val _ = write_file script_name script;
-
-    val pid_name = OS.FileSys.tmpName ();
-    val output_name = OS.FileSys.tmpName ();
-
-    (*result state*)
-    datatype result = Wait | Signal | Result of int;
-    val result = ref Wait;
-    val lock = Mutex.mutex ();
-    val cond = ConditionVar.conditionVar ();
-    fun set_result res =
-      (Mutex.lock lock; result := res; ConditionVar.signal cond; Mutex.unlock lock);
-
-    val _ = Mutex.lock lock;
-
-    (*system thread*)
-    val system_thread = Thread.fork (fn () =>
-      let
-        val status =
-          OS.Process.system ("exec \"$ISABELLE_HOME/lib/scripts/process\" group " ^ pid_name ^
-            " script \"exec bash " ^ script_name ^ " > " ^ output_name ^ "\"");
-        val res =
-          (case Posix.Process.fromStatus status of
-            Posix.Process.W_EXITED => Result 0
-          | Posix.Process.W_EXITSTATUS 0wx82 => Signal
-          | Posix.Process.W_EXITSTATUS w => Result (Word8.toInt w)
-          | Posix.Process.W_SIGNALED s =>
-              if s = Posix.Signal.int then Signal
-              else Result (256 + LargeWord.toInt (Posix.Signal.toWord s))
-          | Posix.Process.W_STOPPED s => Result (512 + LargeWord.toInt (Posix.Signal.toWord s)));
-      in set_result res end handle _ (*sic*) => set_result (Result 2), []);
-
-    (*main thread -- proxy for interrupts*)
-    fun kill n =
-      (case Int.fromString (read_file pid_name) of
-        SOME pid =>
-          Posix.Process.kill
-            (Posix.Process.K_GROUP (Posix.Process.wordToPid (LargeWord.fromInt pid)),
-              Posix.Signal.int)
-      | NONE => ())
-      handle OS.SysErr _ => () | IO.Io _ =>
-        (OS.Process.sleep (seconds 0.1); if n > 0 then kill (n - 1) else ());
-
-    val _ =
-      while ! result = Wait do
-        let val res =
-          sync_wait (SOME orig_atts)
-            (SOME (Time.+ (Time.now (), seconds 0.1))) cond lock
-        in if Exn.is_interrupt_exn res then kill 10 else () end;
-
-    (*cleanup*)
-    val output = read_file output_name handle IO.Io _ => "";
-    val _ = OS.FileSys.remove script_name handle OS.SysErr _ => ();
-    val _ = OS.FileSys.remove pid_name handle OS.SysErr _ => ();
-    val _ = OS.FileSys.remove output_name handle OS.SysErr _ => ();
-    val _ = Thread.interrupt system_thread handle Thread _ => ();
-    val rc = (case ! result of Signal => Exn.interrupt () | Result rc => rc);
-  in (output, rc) end);
-
-
 (* critical section -- may be nested within the same thread *)
 
 local
@@ -229,6 +149,9 @@
 val critical_thread = ref (NONE: Thread.thread option);
 val critical_name = ref "";
 
+fun show "" = "" | show name = " " ^ name;
+fun show' "" = "" | show' name = " [" ^ name ^ "]";
+
 in
 
 fun self_critical () =
diff -r d73659e8ccdd -r 782399904d9c src/Pure/ML-Systems/polyml_common.ML
--- a/src/Pure/ML-Systems/polyml_common.ML	Sat Nov 27 18:51:15 2010 +0100
+++ b/src/Pure/ML-Systems/polyml_common.ML	Sat Nov 27 20:48:06 2010 +0100
@@ -14,7 +14,6 @@
 use "ML-Systems/multithreading.ML";
 use "ML-Systems/time_limit.ML";
 use "General/timing.ML";
-use "ML-Systems/bash.ML";
 use "ML-Systems/ml_pretty.ML";
 use "ML-Systems/use_context.ML";
 
diff -r d73659e8ccdd -r 782399904d9c src/Pure/ML-Systems/proper_int.ML
--- a/src/Pure/ML-Systems/proper_int.ML	Sat Nov 27 18:51:15 2010 +0100
+++ b/src/Pure/ML-Systems/proper_int.ML	Sat Nov 27 20:48:06 2010 +0100
@@ -165,6 +165,15 @@
   val fromInt = Word.fromInt o dest_int;
 end;
 
+structure Word8 =
+struct
+  open Word8;
+  val wordSize = mk_int Word8.wordSize;
+  val toInt = mk_int o Word8.toInt;
+  val toIntX = mk_int o Word8.toIntX;
+  val fromInt = Word8.fromInt o dest_int;
+end;
+
 structure Word32 =
 struct
   open Word32;
@@ -174,6 +183,15 @@
   val fromInt = Word32.fromInt o dest_int;
 end;
 
+structure LargeWord =
+struct
+  open LargeWord;
+  val wordSize = mk_int LargeWord.wordSize;
+  val toInt = mk_int o LargeWord.toInt;
+  val toIntX = mk_int o LargeWord.toIntX;
+  val fromInt = LargeWord.fromInt o dest_int;
+end;
+
 
 (* Real *)
 
diff -r d73659e8ccdd -r 782399904d9c src/Pure/ML-Systems/smlnj.ML
--- a/src/Pure/ML-Systems/smlnj.ML	Sat Nov 27 18:51:15 2010 +0100
+++ b/src/Pure/ML-Systems/smlnj.ML	Sat Nov 27 20:48:06 2010 +0100
@@ -14,7 +14,6 @@
 use "ML-Systems/thread_dummy.ML";
 use "ML-Systems/multithreading.ML";
 use "General/timing.ML";
-use "ML-Systems/bash.ML";
 use "ML-Systems/ml_name_space.ML";
 use "ML-Systems/ml_pretty.ML";
 structure PolyML = struct end;
@@ -170,11 +169,6 @@
 val pwd = OS.FileSys.getDir;
 
 
-(* system command execution *)
-
-val bash_output = (fn (output, rc) => (output, mk_int rc)) o bash_output;
-
-
 (* getenv *)
 
 fun getenv var =
diff -r d73659e8ccdd -r 782399904d9c src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Sat Nov 27 18:51:15 2010 +0100
+++ b/src/Pure/ROOT.ML	Sat Nov 27 20:48:06 2010 +0100
@@ -72,6 +72,15 @@
 if Multithreading.available then ()
 else use "Concurrent/synchronized_sequential.ML";
 
+if Multithreading.available
+then use "Concurrent/bash.ML"
+else use "Concurrent/bash_sequential.ML";
+
+fun bash s =
+  (case bash_output s of
+    ("", rc) => rc
+  | (out, rc) => (writeln (perhaps (try (unsuffix "\n")) out); rc));
+
 use "Concurrent/mailbox.ML";
 use "Concurrent/task_queue.ML";
 use "Concurrent/future.ML";
@@ -233,6 +242,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 d73659e8ccdd -r 782399904d9c 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 20:48:06 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: 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);
+
+val mkdir = OS.FileSys.mkDir o File.platform_path;
+
+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 d73659e8ccdd -r 782399904d9c src/Pure/Thy/present.ML
--- a/src/Pure/Thy/present.ML	Sat Nov 27 18:51:15 2010 +0100
+++ b/src/Pure/Thy/present.ML	Sat Nov 27 20:48:06 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 d73659e8ccdd -r 782399904d9c src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Sat Nov 27 18:51:15 2010 +0100
+++ b/src/Pure/Thy/thy_info.ML	Sat Nov 27 20:48:06 2010 +0100
@@ -64,8 +64,8 @@
 (* thy database *)
 
 type deps =
- {master: (Path.T * File.ident),  (*master dependencies for thy file*)
-  imports: string list};          (*source specification of imports (partially qualified)*)
+ {master: (Path.T * Thy_Load.file_ident),  (*master dependencies for thy file*)
+  imports: string list};  (*source specification of imports (partially qualified)*)
 
 fun make_deps master imports : deps = {master = master, imports = imports};
 
diff -r d73659e8ccdd -r 782399904d9c src/Pure/Thy/thy_load.ML
--- a/src/Pure/Thy/thy_load.ML	Sat Nov 27 18:51:15 2010 +0100
+++ b/src/Pure/Thy/thy_load.ML	Sat Nov 27 20:48:06 2010 +0100
@@ -17,14 +17,17 @@
 signature THY_LOAD =
 sig
   include BASIC_THY_LOAD
+  eqtype file_ident
+  val pretty_file_ident: file_ident -> Pretty.T
+  val file_ident: Path.T -> file_ident option
   val set_master_path: Path.T -> unit
   val get_master_path: unit -> Path.T
   val master_directory: theory -> Path.T
-  val provide: Path.T * (Path.T * File.ident) -> theory -> theory
-  val check_file: Path.T list -> Path.T -> Path.T * File.ident
-  val check_thy: Path.T -> string -> Path.T * File.ident
+  val provide: Path.T * (Path.T * file_ident) -> theory -> theory
+  val check_file: Path.T list -> Path.T -> Path.T * file_ident
+  val check_thy: Path.T -> string -> Path.T * file_ident
   val deps_thy: Path.T -> string ->
-   {master: Path.T * File.ident, text: string, imports: string list, uses: Path.T list}
+   {master: Path.T * file_ident, text: string, imports: string list, uses: Path.T list}
   val loaded_files: theory -> Path.T list
   val all_current: theory -> bool
   val provide_file: Path.T -> theory -> theory
@@ -36,12 +39,57 @@
 structure Thy_Load: THY_LOAD =
 struct
 
+(* file identification *)
+
+local
+  val file_ident_cache =
+    Synchronized.var "file_ident_cache"
+      (Symtab.empty: {time_stamp: string, id: string} Symtab.table);
+in
+
+fun check_cache (path, time) =
+  (case Symtab.lookup (Synchronized.value file_ident_cache) path of
+    NONE => NONE
+  | SOME {time_stamp, id} => if time_stamp = time then SOME id else NONE);
+
+fun update_cache (path, (time, id)) =
+  Synchronized.change file_ident_cache
+    (Symtab.update (path, {time_stamp = time, id = id}));
+
+end;
+
+datatype file_ident = File_Ident of string;
+
+fun pretty_file_ident (File_Ident s) = Pretty.str (quote s);
+
+fun file_ident path =
+  let val physical_path = perhaps (try OS.FileSys.fullPath) (File.platform_path path) in
+    (case try (Time.toString o OS.FileSys.modTime) physical_path of
+      NONE => NONE
+    | SOME mod_time => SOME (File_Ident
+        (case getenv "ISABELLE_FILE_IDENT" of
+          "" => physical_path ^ ": " ^ mod_time
+        | cmd =>
+            (case check_cache (physical_path, mod_time) of
+              SOME id => id
+            | NONE =>
+                let
+                  val (id, rc) =  (*potentially slow*)
+                    bash_output
+                      ("\"$ISABELLE_HOME/lib/scripts/fileident\" " ^ File.shell_quote physical_path);
+                in
+                  if id <> "" andalso rc = 0 then (update_cache (physical_path, (mod_time, id)); id)
+                  else error ("Failed to identify file " ^ quote (Path.implode path) ^ " by " ^ cmd)
+                end))))
+  end;
+
+
 (* manage source files *)
 
 type files =
- {master_dir: Path.T,                                 (*master directory of theory source*)
-  required: Path.T list,                              (*source path*)
-  provided: (Path.T * (Path.T * File.ident)) list};   (*source path, physical path, identifier*)
+ {master_dir: Path.T,  (*master directory of theory source*)
+  required: Path.T list,  (*source path*)
+  provided: (Path.T * (Path.T * file_ident)) list};  (*source path, physical path, identifier*)
 
 fun make_files (master_dir, required, provided): files =
  {master_dir = master_dir, required = required, provided = provided};
@@ -79,26 +127,26 @@
 (* maintain default paths *)
 
 local
-  val load_path = Unsynchronized.ref [Path.current];
+  val load_path = Synchronized.var "load_path" [Path.current];
   val master_path = Unsynchronized.ref Path.current;
 in
 
-fun show_path () = map Path.implode (! load_path);
+fun show_path () = map Path.implode (Synchronized.value load_path);
 
-fun del_path s =
-  CRITICAL (fn () => Unsynchronized.change load_path (remove (op =) (Path.explode s)));
+fun del_path s = Synchronized.change load_path (remove (op =) (Path.explode s));
 
-fun add_path s =
-  CRITICAL (fn () => (del_path s; Unsynchronized.change load_path (cons (Path.explode s))));
+fun add_path s = Synchronized.change load_path (update (op =) (Path.explode s));
 
 fun path_add s =
-  CRITICAL (fn () =>
-    (del_path s; Unsynchronized.change load_path (fn path => path @ [Path.explode s])));
+  Synchronized.change load_path (fn path =>
+    let val p = Path.explode s
+    in remove (op =) p path @ [p] end);
 
-fun reset_path () = CRITICAL (fn () => load_path := [Path.current]);
+fun reset_path () = Synchronized.change load_path (K [Path.current]);
 
 fun search_path dir path =
-  distinct (op =) (dir :: (if Path.is_basic path then (! load_path) else [Path.current]));
+  distinct (op =)
+    (dir :: (if Path.is_basic path then (Synchronized.value load_path) else [Path.current]));
 
 fun set_master_path path = master_path := path;
 fun get_master_path () = ! master_path;
@@ -115,7 +163,7 @@
   in
     dirs |> get_first (fn dir =>
       let val full_path = File.full_path (Path.append dir path) in
-        (case File.ident full_path of
+        (case file_ident full_path of
           NONE => NONE
         | SOME id => SOME (full_path, id))
       end)
diff -r d73659e8ccdd -r 782399904d9c src/Pure/pure_setup.ML
--- a/src/Pure/pure_setup.ML	Sat Nov 27 18:51:15 2010 +0100
+++ b/src/Pure/pure_setup.ML	Sat Nov 27 20:48:06 2010 +0100
@@ -36,7 +36,7 @@
 toplevel_pp ["Context", "Proof", "context"] "Proof_Display.pp_context";
 toplevel_pp ["Syntax", "ast"] "Syntax.pretty_ast";
 toplevel_pp ["Path", "T"] "Pretty.str o quote o Path.implode";
-toplevel_pp ["File", "ident"] "Pretty.str o quote o File.rep_ident";
+toplevel_pp ["Thy_Load", "file_ident"] "Thy_Load.pretty_file_ident";
 toplevel_pp ["Proof", "state"] "(fn _: Proof.state => Pretty.str \"<Proof.state>\")";
 toplevel_pp ["Toplevel", "state"] "Toplevel.pretty_abstract";
 
diff -r d73659e8ccdd -r 782399904d9c src/Tools/Code/code_haskell.ML
--- a/src/Tools/Code/code_haskell.ML	Sat Nov 27 18:51:15 2010 +0100
+++ b/src/Tools/Code/code_haskell.ML	Sat Nov 27 20:48:06 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 (Path.dir filepath);
           in
             (File.write filepath o format [] width o Pretty.chunks2)
               [str "{-# OPTIONS_GHC -fglasgow-exts #-}", content]
diff -r d73659e8ccdd -r 782399904d9c src/Tools/cache_io.ML
--- a/src/Tools/cache_io.ML	Sat Nov 27 18:51:15 2010 +0100
+++ b/src/Tools/cache_io.ML	Sat Nov 27 20:48:06 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 = {