--- 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
--- /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);
+
--- /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;
+
--- 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;
--- 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;
+
--- 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 \
--- 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 *)
--- 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;
-
--- 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 () =
--- 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";
--- 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 *)
--- 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 =
--- 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";
--- /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;
+
--- 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)))
--- 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};
--- 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)
--- 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";
--- 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]
--- 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 = {