1.1 --- a/src/HOL/Tools/Nitpick/kodkod.ML Sat Nov 27 18:51:15 2010 +0100
1.2 +++ b/src/HOL/Tools/Nitpick/kodkod.ML Sat Nov 27 20:48:06 2010 +0100
1.3 @@ -983,7 +983,7 @@
1.4 let
1.5 val dir = getenv "ISABELLE_TMP"
1.6 val _ = if !created_temp_dir then ()
1.7 - else (created_temp_dir := true; File.mkdir (Path.explode dir))
1.8 + else (created_temp_dir := true; Isabelle_System.mkdirs (Path.explode dir))
1.9 in (serial_string (), dir) end
1.10
1.11 (* The fudge term below is to account for Kodkodi's slow start-up time, which
2.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
2.2 +++ b/src/Pure/Concurrent/bash.ML Sat Nov 27 20:48:06 2010 +0100
2.3 @@ -0,0 +1,83 @@
2.4 +(* Title: Pure/Concurrent/bash.ML
2.5 + Author: Makarius
2.6 +
2.7 +GNU bash processes, with propagation of interrupts.
2.8 +*)
2.9 +
2.10 +val bash_output = uninterruptible (fn restore_attributes => fn script =>
2.11 + let
2.12 + datatype result = Wait | Signal | Result of int;
2.13 + val result = Synchronized.var "bash_result" Wait;
2.14 +
2.15 + val id = serial_string ();
2.16 + val script_path = File.tmp_path (Path.basic ("bash_script" ^ id));
2.17 + val output_path = File.tmp_path (Path.basic ("bash_output" ^ id));
2.18 + val pid_path = File.tmp_path (Path.basic ("bash_pid" ^ id));
2.19 +
2.20 + val system_thread =
2.21 + Simple_Thread.fork false (fn () =>
2.22 + Multithreading.with_attributes Multithreading.private_interrupts (fn _ =>
2.23 + let
2.24 + val _ = File.write script_path script;
2.25 + val status =
2.26 + OS.Process.system
2.27 + ("exec \"$ISABELLE_HOME/lib/scripts/process\" group " ^
2.28 + File.shell_path pid_path ^ " script \"exec bash " ^
2.29 + File.shell_path script_path ^ " > " ^
2.30 + File.shell_path output_path ^ "\"");
2.31 + val res =
2.32 + (case Posix.Process.fromStatus status of
2.33 + Posix.Process.W_EXITED => Result 0
2.34 + | Posix.Process.W_EXITSTATUS 0wx82 => Signal
2.35 + | Posix.Process.W_EXITSTATUS w => Result (Word8.toInt w)
2.36 + | Posix.Process.W_SIGNALED s =>
2.37 + if s = Posix.Signal.int then Signal
2.38 + else Result (256 + LargeWord.toInt (Posix.Signal.toWord s))
2.39 + | Posix.Process.W_STOPPED s =>
2.40 + Result (512 + LargeWord.toInt (Posix.Signal.toWord s)));
2.41 + in Synchronized.change result (K res) end
2.42 + handle _ (*sic*) => Synchronized.change result (fn Wait => Signal | res => res)));
2.43 +
2.44 + fun terminate () =
2.45 + let
2.46 + val sig_test = Posix.Signal.fromWord 0w0;
2.47 +
2.48 + fun kill_group pid s =
2.49 + (Posix.Process.kill
2.50 + (Posix.Process.K_GROUP (Posix.Process.wordToPid (LargeWord.fromInt pid)), s); true)
2.51 + handle OS.SysErr _ => false;
2.52 +
2.53 + fun kill s =
2.54 + (case Int.fromString (File.read pid_path) of
2.55 + NONE => true
2.56 + | SOME pid => (kill_group pid s; kill_group pid sig_test))
2.57 + handle IO.Io _ => true;
2.58 +
2.59 + fun multi_kill count s =
2.60 + count = 0 orelse
2.61 + kill s andalso (OS.Process.sleep (seconds 0.1); multi_kill (count - 1) s);
2.62 + val _ =
2.63 + multi_kill 10 Posix.Signal.int andalso
2.64 + multi_kill 10 Posix.Signal.term andalso
2.65 + multi_kill 10 Posix.Signal.kill;
2.66 + in () end;
2.67 +
2.68 + fun cleanup () =
2.69 + (terminate ();
2.70 + Simple_Thread.interrupt system_thread;
2.71 + try File.rm script_path;
2.72 + try File.rm output_path;
2.73 + try File.rm pid_path);
2.74 + in
2.75 + let
2.76 + val _ =
2.77 + restore_attributes (fn () =>
2.78 + Synchronized.guarded_access result (fn Wait => NONE | x => SOME ((), x))) ();
2.79 +
2.80 + val output = the_default "" (try File.read output_path);
2.81 + val rc = (case Synchronized.value result of Signal => Exn.interrupt () | Result rc => rc);
2.82 + val _ = cleanup ();
2.83 + in (output, rc) end
2.84 + handle exn => (cleanup (); reraise exn)
2.85 + end);
2.86 +
3.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
3.2 +++ b/src/Pure/Concurrent/bash_sequential.ML Sat Nov 27 20:48:06 2010 +0100
3.3 @@ -0,0 +1,34 @@
3.4 +(* Title: Pure/Concurrent/bash_sequential.ML
3.5 + Author: Makarius
3.6 +
3.7 +Generic GNU bash processes (no provisions to propagate interrupts, but
3.8 +could work via the controlling tty).
3.9 +*)
3.10 +
3.11 +fun bash_output script =
3.12 + let
3.13 + val id = serial_string ();
3.14 + val script_path = File.tmp_path (Path.basic ("bash_script" ^ id));
3.15 + val output_path = File.tmp_path (Path.basic ("bash_output" ^ id));
3.16 + fun cleanup () = (try File.rm script_path; try File.rm output_path);
3.17 + in
3.18 + let
3.19 + val _ = File.write script_path script;
3.20 + val status =
3.21 + OS.Process.system
3.22 + ("exec \"$ISABELLE_HOME/lib/scripts/process\" no_group /dev/null" ^
3.23 + " script \"exec bash " ^ File.shell_path script_path ^ " > " ^
3.24 + File.shell_path output_path ^ "\"");
3.25 + val rc =
3.26 + (case Posix.Process.fromStatus status of
3.27 + Posix.Process.W_EXITED => 0
3.28 + | Posix.Process.W_EXITSTATUS w => Word8.toInt w
3.29 + | Posix.Process.W_SIGNALED s => 256 + LargeWord.toInt (Posix.Signal.toWord s)
3.30 + | Posix.Process.W_STOPPED s => 512 + LargeWord.toInt (Posix.Signal.toWord s));
3.31 +
3.32 + val output = the_default "" (try File.read output_path);
3.33 + val _ = cleanup ();
3.34 + in (output, rc) end
3.35 + handle exn => (cleanup (); reraise exn)
3.36 + end;
3.37 +
4.1 --- a/src/Pure/General/file.ML Sat Nov 27 18:51:15 2010 +0100
4.2 +++ b/src/Pure/General/file.ML Sat Nov 27 20:48:06 2010 +0100
4.3 @@ -13,16 +13,9 @@
4.4 val pwd: unit -> Path.T
4.5 val full_path: Path.T -> Path.T
4.6 val tmp_path: Path.T -> Path.T
4.7 - val isabelle_tool: string -> string -> int
4.8 - eqtype ident
4.9 - val rep_ident: ident -> string
4.10 - val ident: Path.T -> ident option
4.11 val exists: Path.T -> bool
4.12 val check: Path.T -> unit
4.13 val rm: Path.T -> unit
4.14 - val rm_tree: Path.T -> unit
4.15 - val mkdir: Path.T -> unit
4.16 - val mkdir_leaf: Path.T -> unit
4.17 val open_input: (TextIO.instream -> 'a) -> Path.T -> 'a
4.18 val open_output: (TextIO.outstream -> 'a) -> Path.T -> 'a
4.19 val open_append: (TextIO.outstream -> 'a) -> Path.T -> 'a
4.20 @@ -35,7 +28,6 @@
4.21 val write_buffer: Path.T -> Buffer.T -> unit
4.22 val eq: Path.T * Path.T -> bool
4.23 val copy: Path.T -> Path.T -> unit
4.24 - val copy_dir: Path.T -> Path.T -> unit
4.25 end;
4.26
4.27 structure File: FILE =
4.28 @@ -45,7 +37,11 @@
4.29
4.30 val platform_path = Path.implode o Path.expand;
4.31
4.32 -val shell_quote = enclose "'" "'";
4.33 +fun shell_quote s =
4.34 + if exists_string (fn c => c = "'") s then
4.35 + error ("Illegal single quote in path specification: " ^ quote s)
4.36 + else enclose "'" "'" s;
4.37 +
4.38 val shell_path = shell_quote o platform_path;
4.39
4.40
4.41 @@ -65,66 +61,6 @@
4.42 Path.append (Path.variable "ISABELLE_TMP") (Path.base path);
4.43
4.44
4.45 -(* system commands *)
4.46 -
4.47 -fun isabelle_tool name args =
4.48 - (case space_explode ":" (getenv "ISABELLE_TOOLS") |> get_first (fn dir =>
4.49 - let val path = dir ^ "/" ^ name in
4.50 - if can OS.FileSys.modTime path andalso
4.51 - not (OS.FileSys.isDir path) andalso
4.52 - OS.FileSys.access (path, [OS.FileSys.A_READ, OS.FileSys.A_EXEC])
4.53 - then SOME path
4.54 - else NONE
4.55 - end handle OS.SysErr _ => NONE) of
4.56 - SOME path => bash (shell_quote path ^ " " ^ args)
4.57 - | NONE => (writeln ("Unknown Isabelle tool: " ^ name); 2));
4.58 -
4.59 -fun system_command cmd =
4.60 - if bash cmd <> 0 then error ("System command failed: " ^ cmd)
4.61 - else ();
4.62 -
4.63 -
4.64 -(* file identification *)
4.65 -
4.66 -local
4.67 - val ident_cache =
4.68 - Unsynchronized.ref (Symtab.empty: {time_stamp: string, id: string} Symtab.table);
4.69 -in
4.70 -
4.71 -fun check_cache (path, time) =
4.72 - (case Symtab.lookup (! ident_cache) path of
4.73 - NONE => NONE
4.74 - | SOME {time_stamp, id} => if time_stamp = time then SOME id else NONE);
4.75 -
4.76 -fun update_cache (path, (time, id)) = CRITICAL (fn () =>
4.77 - Unsynchronized.change ident_cache
4.78 - (Symtab.update (path, {time_stamp = time, id = id})));
4.79 -
4.80 -end;
4.81 -
4.82 -datatype ident = Ident of string;
4.83 -fun rep_ident (Ident s) = s;
4.84 -
4.85 -fun ident path =
4.86 - let val physical_path = perhaps (try OS.FileSys.fullPath) (platform_path path) in
4.87 - (case try (Time.toString o OS.FileSys.modTime) physical_path of
4.88 - NONE => NONE
4.89 - | SOME mod_time => SOME (Ident
4.90 - (case getenv "ISABELLE_FILE_IDENT" of
4.91 - "" => physical_path ^ ": " ^ mod_time
4.92 - | cmd =>
4.93 - (case check_cache (physical_path, mod_time) of
4.94 - SOME id => id
4.95 - | NONE =>
4.96 - let val (id, rc) = (*potentially slow*)
4.97 - bash_output ("\"$ISABELLE_HOME/lib/scripts/fileident\" " ^ shell_quote physical_path)
4.98 - in
4.99 - if id <> "" andalso rc = 0 then (update_cache (physical_path, (mod_time, id)); id)
4.100 - else error ("Failed to identify file " ^ quote (Path.implode path) ^ " by " ^ cmd)
4.101 - end))))
4.102 - end;
4.103 -
4.104 -
4.105 (* directory entries *)
4.106
4.107 val exists = can OS.FileSys.modTime o platform_path;
4.108 @@ -135,15 +71,6 @@
4.109
4.110 val rm = OS.FileSys.remove o platform_path;
4.111
4.112 -fun rm_tree path = system_command ("rm -r " ^ shell_path path);
4.113 -
4.114 -fun mkdir path = system_command ("mkdir -p " ^ shell_path path);
4.115 -
4.116 -fun mkdir_leaf path = (check (Path.dir path); mkdir path);
4.117 -
4.118 -fun is_dir path =
4.119 - the_default false (try OS.FileSys.isDir (platform_path path));
4.120 -
4.121
4.122 (* open files *)
4.123
4.124 @@ -201,14 +128,13 @@
4.125 SOME ids => is_equal (OS.FileSys.compare ids)
4.126 | NONE => false);
4.127
4.128 +fun is_dir path =
4.129 + the_default false (try OS.FileSys.isDir (platform_path path));
4.130 +
4.131 fun copy src dst =
4.132 if eq (src, dst) then ()
4.133 else
4.134 let val target = if is_dir dst then Path.append dst (Path.base src) else dst
4.135 in write target (read src) end;
4.136
4.137 -fun copy_dir src dst =
4.138 - if eq (src, dst) then ()
4.139 - else (system_command ("cp -r -f " ^ shell_path src ^ "/. " ^ shell_path dst); ());
4.140 -
4.141 end;
5.1 --- a/src/Pure/General/secure.ML Sat Nov 27 18:51:15 2010 +0100
5.2 +++ b/src/Pure/General/secure.ML Sat Nov 27 20:48:06 2010 +0100
5.3 @@ -15,8 +15,6 @@
5.4 val toplevel_pp: string list -> string -> unit
5.5 val PG_setup: unit -> unit
5.6 val commit: unit -> unit
5.7 - val bash_output: string -> string * int
5.8 - val bash: string -> int
5.9 end;
5.10
5.11 structure Secure: SECURE =
5.12 @@ -58,20 +56,6 @@
5.13 fun PG_setup () =
5.14 use_global "val change = Unsynchronized.change; structure ThyLoad = ProofGeneral.ThyLoad;";
5.15
5.16 -
5.17 -(* shell commands *)
5.18 -
5.19 -fun secure_shell () = deny_secure "Cannot execute shell commands in secure mode";
5.20 -
5.21 -val orig_bash_output = bash_output;
5.22 -
5.23 -fun bash_output s = (secure_shell (); orig_bash_output s);
5.24 -
5.25 -fun bash s =
5.26 - (case bash_output s of
5.27 - ("", rc) => rc
5.28 - | (out, rc) => (writeln (perhaps (try (unsuffix "\n")) out); rc));
5.29 -
5.30 end;
5.31
5.32 (*override previous toplevel bindings!*)
5.33 @@ -80,5 +64,4 @@
5.34 fun use s = Secure.use_file ML_Parse.global_context true s
5.35 handle ERROR msg => (writeln msg; error "ML error");
5.36 val toplevel_pp = Secure.toplevel_pp;
5.37 -val bash_output = Secure.bash_output;
5.38 -val bash = Secure.bash;
5.39 +
6.1 --- a/src/Pure/IsaMakefile Sat Nov 27 18:51:15 2010 +0100
6.2 +++ b/src/Pure/IsaMakefile Sat Nov 27 20:48:06 2010 +0100
6.3 @@ -22,7 +22,6 @@
6.4 BOOTSTRAP_FILES = \
6.5 General/exn.ML \
6.6 General/timing.ML \
6.7 - ML-Systems/bash.ML \
6.8 ML-Systems/compiler_polyml-5.2.ML \
6.9 ML-Systems/compiler_polyml-5.3.ML \
6.10 ML-Systems/ml_name_space.ML \
6.11 @@ -55,6 +54,8 @@
6.12 Pure: $(OUT)/Pure
6.13
6.14 $(OUT)/Pure: $(BOOTSTRAP_FILES) \
6.15 + Concurrent/bash.ML \
6.16 + Concurrent/bash_sequential.ML \
6.17 Concurrent/cache.ML \
6.18 Concurrent/future.ML \
6.19 Concurrent/lazy.ML \
6.20 @@ -188,6 +189,7 @@
6.21 Syntax/syntax.ML \
6.22 Syntax/type_ext.ML \
6.23 System/isabelle_process.ML \
6.24 + System/isabelle_system.ML \
6.25 System/isar.ML \
6.26 System/session.ML \
6.27 Thy/html.ML \
7.1 --- a/src/Pure/Isar/isar_cmd.ML Sat Nov 27 18:51:15 2010 +0100
7.2 +++ b/src/Pure/Isar/isar_cmd.ML Sat Nov 27 20:48:06 2010 +0100
7.3 @@ -291,11 +291,11 @@
7.4
7.5 fun display_drafts files = Toplevel.imperative (fn () =>
7.6 let val outfile = File.shell_path (Present.drafts (getenv "ISABELLE_DOC_FORMAT") files)
7.7 - in File.isabelle_tool "display" ("-c " ^ outfile ^ " &"); () end);
7.8 + in Isabelle_System.isabelle_tool "display" ("-c " ^ outfile ^ " &"); () end);
7.9
7.10 fun print_drafts files = Toplevel.imperative (fn () =>
7.11 let val outfile = File.shell_path (Present.drafts "ps" files)
7.12 - in File.isabelle_tool "print" ("-c " ^ outfile); () end);
7.13 + in Isabelle_System.isabelle_tool "print" ("-c " ^ outfile); () end);
7.14
7.15
7.16 (* print parts of theory and proof context *)
8.1 --- a/src/Pure/ML-Systems/bash.ML Sat Nov 27 18:51:15 2010 +0100
8.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
8.3 @@ -1,43 +0,0 @@
8.4 -(* Title: Pure/ML-Systems/bash.ML
8.5 - Author: Makarius
8.6 -
8.7 -Generic GNU bash processes (no provisions to propagate interrupts, but
8.8 -could work via the controlling tty).
8.9 -*)
8.10 -
8.11 -local
8.12 -
8.13 -fun read_file name =
8.14 - let val is = TextIO.openIn name
8.15 - in Exn.release (Exn.capture TextIO.inputAll is before TextIO.closeIn is) end;
8.16 -
8.17 -fun write_file name txt =
8.18 - let val os = TextIO.openOut name
8.19 - in Exn.release (Exn.capture TextIO.output (os, txt) before TextIO.closeOut os) end;
8.20 -
8.21 -in
8.22 -
8.23 -fun bash_output script =
8.24 - let
8.25 - val script_name = OS.FileSys.tmpName ();
8.26 - val _ = write_file script_name script;
8.27 -
8.28 - val output_name = OS.FileSys.tmpName ();
8.29 -
8.30 - val status =
8.31 - OS.Process.system ("exec \"$ISABELLE_HOME/lib/scripts/process\" no_group /dev/null" ^
8.32 - " script \"exec bash " ^ script_name ^ " > " ^ output_name ^ "\"");
8.33 - val rc =
8.34 - (case Posix.Process.fromStatus status of
8.35 - Posix.Process.W_EXITED => 0
8.36 - | Posix.Process.W_EXITSTATUS w => Word8.toInt w
8.37 - | Posix.Process.W_SIGNALED s => 256 + LargeWord.toInt (Posix.Signal.toWord s)
8.38 - | Posix.Process.W_STOPPED s => 512 + LargeWord.toInt (Posix.Signal.toWord s));
8.39 -
8.40 - val output = read_file output_name handle IO.Io _ => "";
8.41 - val _ = OS.FileSys.remove script_name handle OS.SysErr _ => ();
8.42 - val _ = OS.FileSys.remove output_name handle OS.SysErr _ => ();
8.43 - in (output, rc) end;
8.44 -
8.45 -end;
8.46 -
9.1 --- a/src/Pure/ML-Systems/multithreading_polyml.ML Sat Nov 27 18:51:15 2010 +0100
9.2 +++ b/src/Pure/ML-Systems/multithreading_polyml.ML Sat Nov 27 20:48:06 2010 +0100
9.3 @@ -8,7 +8,6 @@
9.4 sig
9.5 val interruptible: ('a -> 'b) -> 'a -> 'b
9.6 val uninterruptible: ((('c -> 'd) -> 'c -> 'd) -> 'a -> 'b) -> 'a -> 'b
9.7 - val bash_output: string -> string * int
9.8 structure TimeLimit: TIME_LIMIT
9.9 end;
9.10
9.11 @@ -42,20 +41,6 @@
9.12 fun enabled () = max_threads_value () > 1;
9.13
9.14
9.15 -(* misc utils *)
9.16 -
9.17 -fun show "" = "" | show name = " " ^ name;
9.18 -fun show' "" = "" | show' name = " [" ^ name ^ "]";
9.19 -
9.20 -fun read_file name =
9.21 - let val is = TextIO.openIn name
9.22 - in Exn.release (Exn.capture TextIO.inputAll is before TextIO.closeIn is) end;
9.23 -
9.24 -fun write_file name txt =
9.25 - let val os = TextIO.openOut name
9.26 - in Exn.release (Exn.capture TextIO.output (os, txt) before TextIO.closeOut os) end;
9.27 -
9.28 -
9.29 (* thread attributes *)
9.30
9.31 val no_interrupts =
9.32 @@ -156,71 +141,6 @@
9.33 end;
9.34
9.35
9.36 -(* GNU bash processes, with propagation of interrupts *)
9.37 -
9.38 -fun bash_output script = with_attributes no_interrupts (fn orig_atts =>
9.39 - let
9.40 - val script_name = OS.FileSys.tmpName ();
9.41 - val _ = write_file script_name script;
9.42 -
9.43 - val pid_name = OS.FileSys.tmpName ();
9.44 - val output_name = OS.FileSys.tmpName ();
9.45 -
9.46 - (*result state*)
9.47 - datatype result = Wait | Signal | Result of int;
9.48 - val result = ref Wait;
9.49 - val lock = Mutex.mutex ();
9.50 - val cond = ConditionVar.conditionVar ();
9.51 - fun set_result res =
9.52 - (Mutex.lock lock; result := res; ConditionVar.signal cond; Mutex.unlock lock);
9.53 -
9.54 - val _ = Mutex.lock lock;
9.55 -
9.56 - (*system thread*)
9.57 - val system_thread = Thread.fork (fn () =>
9.58 - let
9.59 - val status =
9.60 - OS.Process.system ("exec \"$ISABELLE_HOME/lib/scripts/process\" group " ^ pid_name ^
9.61 - " script \"exec bash " ^ script_name ^ " > " ^ output_name ^ "\"");
9.62 - val res =
9.63 - (case Posix.Process.fromStatus status of
9.64 - Posix.Process.W_EXITED => Result 0
9.65 - | Posix.Process.W_EXITSTATUS 0wx82 => Signal
9.66 - | Posix.Process.W_EXITSTATUS w => Result (Word8.toInt w)
9.67 - | Posix.Process.W_SIGNALED s =>
9.68 - if s = Posix.Signal.int then Signal
9.69 - else Result (256 + LargeWord.toInt (Posix.Signal.toWord s))
9.70 - | Posix.Process.W_STOPPED s => Result (512 + LargeWord.toInt (Posix.Signal.toWord s)));
9.71 - in set_result res end handle _ (*sic*) => set_result (Result 2), []);
9.72 -
9.73 - (*main thread -- proxy for interrupts*)
9.74 - fun kill n =
9.75 - (case Int.fromString (read_file pid_name) of
9.76 - SOME pid =>
9.77 - Posix.Process.kill
9.78 - (Posix.Process.K_GROUP (Posix.Process.wordToPid (LargeWord.fromInt pid)),
9.79 - Posix.Signal.int)
9.80 - | NONE => ())
9.81 - handle OS.SysErr _ => () | IO.Io _ =>
9.82 - (OS.Process.sleep (seconds 0.1); if n > 0 then kill (n - 1) else ());
9.83 -
9.84 - val _ =
9.85 - while ! result = Wait do
9.86 - let val res =
9.87 - sync_wait (SOME orig_atts)
9.88 - (SOME (Time.+ (Time.now (), seconds 0.1))) cond lock
9.89 - in if Exn.is_interrupt_exn res then kill 10 else () end;
9.90 -
9.91 - (*cleanup*)
9.92 - val output = read_file output_name handle IO.Io _ => "";
9.93 - val _ = OS.FileSys.remove script_name handle OS.SysErr _ => ();
9.94 - val _ = OS.FileSys.remove pid_name handle OS.SysErr _ => ();
9.95 - val _ = OS.FileSys.remove output_name handle OS.SysErr _ => ();
9.96 - val _ = Thread.interrupt system_thread handle Thread _ => ();
9.97 - val rc = (case ! result of Signal => Exn.interrupt () | Result rc => rc);
9.98 - in (output, rc) end);
9.99 -
9.100 -
9.101 (* critical section -- may be nested within the same thread *)
9.102
9.103 local
9.104 @@ -229,6 +149,9 @@
9.105 val critical_thread = ref (NONE: Thread.thread option);
9.106 val critical_name = ref "";
9.107
9.108 +fun show "" = "" | show name = " " ^ name;
9.109 +fun show' "" = "" | show' name = " [" ^ name ^ "]";
9.110 +
9.111 in
9.112
9.113 fun self_critical () =
10.1 --- a/src/Pure/ML-Systems/polyml_common.ML Sat Nov 27 18:51:15 2010 +0100
10.2 +++ b/src/Pure/ML-Systems/polyml_common.ML Sat Nov 27 20:48:06 2010 +0100
10.3 @@ -14,7 +14,6 @@
10.4 use "ML-Systems/multithreading.ML";
10.5 use "ML-Systems/time_limit.ML";
10.6 use "General/timing.ML";
10.7 -use "ML-Systems/bash.ML";
10.8 use "ML-Systems/ml_pretty.ML";
10.9 use "ML-Systems/use_context.ML";
10.10
11.1 --- a/src/Pure/ML-Systems/proper_int.ML Sat Nov 27 18:51:15 2010 +0100
11.2 +++ b/src/Pure/ML-Systems/proper_int.ML Sat Nov 27 20:48:06 2010 +0100
11.3 @@ -165,6 +165,15 @@
11.4 val fromInt = Word.fromInt o dest_int;
11.5 end;
11.6
11.7 +structure Word8 =
11.8 +struct
11.9 + open Word8;
11.10 + val wordSize = mk_int Word8.wordSize;
11.11 + val toInt = mk_int o Word8.toInt;
11.12 + val toIntX = mk_int o Word8.toIntX;
11.13 + val fromInt = Word8.fromInt o dest_int;
11.14 +end;
11.15 +
11.16 structure Word32 =
11.17 struct
11.18 open Word32;
11.19 @@ -174,6 +183,15 @@
11.20 val fromInt = Word32.fromInt o dest_int;
11.21 end;
11.22
11.23 +structure LargeWord =
11.24 +struct
11.25 + open LargeWord;
11.26 + val wordSize = mk_int LargeWord.wordSize;
11.27 + val toInt = mk_int o LargeWord.toInt;
11.28 + val toIntX = mk_int o LargeWord.toIntX;
11.29 + val fromInt = LargeWord.fromInt o dest_int;
11.30 +end;
11.31 +
11.32
11.33 (* Real *)
11.34
12.1 --- a/src/Pure/ML-Systems/smlnj.ML Sat Nov 27 18:51:15 2010 +0100
12.2 +++ b/src/Pure/ML-Systems/smlnj.ML Sat Nov 27 20:48:06 2010 +0100
12.3 @@ -14,7 +14,6 @@
12.4 use "ML-Systems/thread_dummy.ML";
12.5 use "ML-Systems/multithreading.ML";
12.6 use "General/timing.ML";
12.7 -use "ML-Systems/bash.ML";
12.8 use "ML-Systems/ml_name_space.ML";
12.9 use "ML-Systems/ml_pretty.ML";
12.10 structure PolyML = struct end;
12.11 @@ -170,11 +169,6 @@
12.12 val pwd = OS.FileSys.getDir;
12.13
12.14
12.15 -(* system command execution *)
12.16 -
12.17 -val bash_output = (fn (output, rc) => (output, mk_int rc)) o bash_output;
12.18 -
12.19 -
12.20 (* getenv *)
12.21
12.22 fun getenv var =
13.1 --- a/src/Pure/ROOT.ML Sat Nov 27 18:51:15 2010 +0100
13.2 +++ b/src/Pure/ROOT.ML Sat Nov 27 20:48:06 2010 +0100
13.3 @@ -72,6 +72,15 @@
13.4 if Multithreading.available then ()
13.5 else use "Concurrent/synchronized_sequential.ML";
13.6
13.7 +if Multithreading.available
13.8 +then use "Concurrent/bash.ML"
13.9 +else use "Concurrent/bash_sequential.ML";
13.10 +
13.11 +fun bash s =
13.12 + (case bash_output s of
13.13 + ("", rc) => rc
13.14 + | (out, rc) => (writeln (perhaps (try (unsuffix "\n")) out); rc));
13.15 +
13.16 use "Concurrent/mailbox.ML";
13.17 use "Concurrent/task_queue.ML";
13.18 use "Concurrent/future.ML";
13.19 @@ -233,6 +242,7 @@
13.20 use "Isar/toplevel.ML";
13.21
13.22 (*theory documents*)
13.23 +use "System/isabelle_system.ML";
13.24 use "Thy/present.ML";
13.25 use "Thy/term_style.ML";
13.26 use "Thy/thy_output.ML";
14.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
14.2 +++ b/src/Pure/System/isabelle_system.ML Sat Nov 27 20:48:06 2010 +0100
14.3 @@ -0,0 +1,51 @@
14.4 +(* Title: Pure/System/isabelle_system.ML
14.5 + Author: Makarius
14.6 +
14.7 +Isabelle system support.
14.8 +*)
14.9 +
14.10 +signature ISABELLE_SYSTEM =
14.11 +sig
14.12 + val isabelle_tool: string -> string -> int
14.13 + val rm_tree: Path.T -> unit
14.14 + val mkdirs: Path.T -> unit
14.15 + val mkdir: Path.T -> unit
14.16 + val copy_dir: Path.T -> Path.T -> unit
14.17 +end;
14.18 +
14.19 +structure Isabelle_System: ISABELLE_SYSTEM =
14.20 +struct
14.21 +
14.22 +(* system commands *)
14.23 +
14.24 +fun isabelle_tool name args =
14.25 + (case space_explode ":" (getenv "ISABELLE_TOOLS") |> get_first (fn dir =>
14.26 + let val path = dir ^ "/" ^ name in
14.27 + if can OS.FileSys.modTime path andalso
14.28 + not (OS.FileSys.isDir path) andalso
14.29 + OS.FileSys.access (path, [OS.FileSys.A_READ, OS.FileSys.A_EXEC])
14.30 + then SOME path
14.31 + else NONE
14.32 + end handle OS.SysErr _ => NONE) of
14.33 + SOME path => bash (File.shell_quote path ^ " " ^ args)
14.34 + | NONE => (writeln ("Unknown Isabelle tool: " ^ name); 2));
14.35 +
14.36 +fun system_command cmd =
14.37 + if bash cmd <> 0 then error ("System command failed: " ^ cmd)
14.38 + else ();
14.39 +
14.40 +
14.41 +(* directory operations *)
14.42 +
14.43 +fun rm_tree path = system_command ("rm -r " ^ File.shell_path path);
14.44 +
14.45 +fun mkdirs path = system_command ("mkdir -p " ^ File.shell_path path);
14.46 +
14.47 +val mkdir = OS.FileSys.mkDir o File.platform_path;
14.48 +
14.49 +fun copy_dir src dst =
14.50 + if File.eq (src, dst) then ()
14.51 + else (system_command ("cp -r -f " ^ File.shell_path src ^ "/. " ^ File.shell_path dst); ());
14.52 +
14.53 +end;
14.54 +
15.1 --- a/src/Pure/Thy/present.ML Sat Nov 27 18:51:15 2010 +0100
15.2 +++ b/src/Pure/Thy/present.ML Sat Nov 27 20:48:06 2010 +0100
15.3 @@ -94,7 +94,7 @@
15.4 val _ = writeln "Displaying graph ...";
15.5 val path = File.tmp_path (Path.explode "tmp.graph");
15.6 val _ = write_graph gr path;
15.7 - val _ = File.isabelle_tool "browser" ("-c " ^ File.shell_path path ^ " &");
15.8 + val _ = Isabelle_System.isabelle_tool "browser" ("-c " ^ File.shell_path path ^ " &");
15.9 in () end;
15.10
15.11
15.12 @@ -344,7 +344,7 @@
15.13 val args = "-o " ^ File.shell_path pdf_path ^ " " ^ File.shell_path gr_path;
15.14 in
15.15 write_graph graph gr_path;
15.16 - if File.isabelle_tool "browser" args <> 0 orelse
15.17 + if Isabelle_System.isabelle_tool "browser" args <> 0 orelse
15.18 not (File.exists eps_path) orelse not (File.exists pdf_path)
15.19 then error "Failed to prepare dependency graph"
15.20 else
15.21 @@ -384,9 +384,9 @@
15.22 else NONE;
15.23
15.24 fun prepare_sources cp path =
15.25 - (File.mkdir path;
15.26 - if cp then File.copy_dir document_path path else ();
15.27 - File.isabelle_tool "latex"
15.28 + (Isabelle_System.mkdirs path;
15.29 + if cp then Isabelle_System.copy_dir document_path path else ();
15.30 + Isabelle_System.isabelle_tool "latex"
15.31 ("-o sty " ^ File.shell_path (Path.append path (Path.basic "root.tex")));
15.32 (case opt_graphs of NONE => () | SOME (pdf, eps) =>
15.33 (File.write (Path.append path graph_pdf_path) pdf;
15.34 @@ -395,14 +395,14 @@
15.35 List.app (finish_tex path) thys);
15.36 in
15.37 if info then
15.38 - (File.mkdir (Path.append html_prefix session_path);
15.39 + (Isabelle_System.mkdirs (Path.append html_prefix session_path);
15.40 File.write_buffer (Path.append html_prefix pre_index_path) (index_buffer html_index);
15.41 File.write (Path.append html_prefix session_entries_path) "";
15.42 create_index html_prefix;
15.43 if length path > 1 then update_index parent_html_prefix name else ();
15.44 (case readme of NONE => () | SOME path => File.copy path html_prefix);
15.45 write_graph sorted_graph (Path.append html_prefix graph_path);
15.46 - File.isabelle_tool "browser" "-b";
15.47 + Isabelle_System.isabelle_tool "browser" "-b";
15.48 File.copy (Path.explode "~~/lib/browser/GraphBrowser.jar") html_prefix;
15.49 List.app (fn (a, txt) => File.write (Path.append html_prefix (Path.basic a)) txt)
15.50 (HTML.applet_pages name (Url.File index_path, name));
15.51 @@ -509,11 +509,11 @@
15.52
15.53 val doc_path = File.tmp_path document_path;
15.54 val result_path = Path.append doc_path Path.parent;
15.55 - val _ = File.mkdir doc_path;
15.56 + val _ = Isabelle_System.mkdirs doc_path;
15.57 val root_path = Path.append doc_path (Path.basic "root.tex");
15.58 val _ = File.copy (Path.explode "~~/lib/texinputs/draft.tex") root_path;
15.59 - val _ = File.isabelle_tool "latex" ("-o sty " ^ File.shell_path root_path);
15.60 - val _ = File.isabelle_tool "latex" ("-o syms " ^ File.shell_path root_path);
15.61 + val _ = Isabelle_System.isabelle_tool "latex" ("-o sty " ^ File.shell_path root_path);
15.62 + val _ = Isabelle_System.isabelle_tool "latex" ("-o syms " ^ File.shell_path root_path);
15.63
15.64 fun known name =
15.65 let val ss = split_lines (File.read (Path.append doc_path (Path.basic name)))
16.1 --- a/src/Pure/Thy/thy_info.ML Sat Nov 27 18:51:15 2010 +0100
16.2 +++ b/src/Pure/Thy/thy_info.ML Sat Nov 27 20:48:06 2010 +0100
16.3 @@ -64,8 +64,8 @@
16.4 (* thy database *)
16.5
16.6 type deps =
16.7 - {master: (Path.T * File.ident), (*master dependencies for thy file*)
16.8 - imports: string list}; (*source specification of imports (partially qualified)*)
16.9 + {master: (Path.T * Thy_Load.file_ident), (*master dependencies for thy file*)
16.10 + imports: string list}; (*source specification of imports (partially qualified)*)
16.11
16.12 fun make_deps master imports : deps = {master = master, imports = imports};
16.13
17.1 --- a/src/Pure/Thy/thy_load.ML Sat Nov 27 18:51:15 2010 +0100
17.2 +++ b/src/Pure/Thy/thy_load.ML Sat Nov 27 20:48:06 2010 +0100
17.3 @@ -17,14 +17,17 @@
17.4 signature THY_LOAD =
17.5 sig
17.6 include BASIC_THY_LOAD
17.7 + eqtype file_ident
17.8 + val pretty_file_ident: file_ident -> Pretty.T
17.9 + val file_ident: Path.T -> file_ident option
17.10 val set_master_path: Path.T -> unit
17.11 val get_master_path: unit -> Path.T
17.12 val master_directory: theory -> Path.T
17.13 - val provide: Path.T * (Path.T * File.ident) -> theory -> theory
17.14 - val check_file: Path.T list -> Path.T -> Path.T * File.ident
17.15 - val check_thy: Path.T -> string -> Path.T * File.ident
17.16 + val provide: Path.T * (Path.T * file_ident) -> theory -> theory
17.17 + val check_file: Path.T list -> Path.T -> Path.T * file_ident
17.18 + val check_thy: Path.T -> string -> Path.T * file_ident
17.19 val deps_thy: Path.T -> string ->
17.20 - {master: Path.T * File.ident, text: string, imports: string list, uses: Path.T list}
17.21 + {master: Path.T * file_ident, text: string, imports: string list, uses: Path.T list}
17.22 val loaded_files: theory -> Path.T list
17.23 val all_current: theory -> bool
17.24 val provide_file: Path.T -> theory -> theory
17.25 @@ -36,12 +39,57 @@
17.26 structure Thy_Load: THY_LOAD =
17.27 struct
17.28
17.29 +(* file identification *)
17.30 +
17.31 +local
17.32 + val file_ident_cache =
17.33 + Synchronized.var "file_ident_cache"
17.34 + (Symtab.empty: {time_stamp: string, id: string} Symtab.table);
17.35 +in
17.36 +
17.37 +fun check_cache (path, time) =
17.38 + (case Symtab.lookup (Synchronized.value file_ident_cache) path of
17.39 + NONE => NONE
17.40 + | SOME {time_stamp, id} => if time_stamp = time then SOME id else NONE);
17.41 +
17.42 +fun update_cache (path, (time, id)) =
17.43 + Synchronized.change file_ident_cache
17.44 + (Symtab.update (path, {time_stamp = time, id = id}));
17.45 +
17.46 +end;
17.47 +
17.48 +datatype file_ident = File_Ident of string;
17.49 +
17.50 +fun pretty_file_ident (File_Ident s) = Pretty.str (quote s);
17.51 +
17.52 +fun file_ident path =
17.53 + let val physical_path = perhaps (try OS.FileSys.fullPath) (File.platform_path path) in
17.54 + (case try (Time.toString o OS.FileSys.modTime) physical_path of
17.55 + NONE => NONE
17.56 + | SOME mod_time => SOME (File_Ident
17.57 + (case getenv "ISABELLE_FILE_IDENT" of
17.58 + "" => physical_path ^ ": " ^ mod_time
17.59 + | cmd =>
17.60 + (case check_cache (physical_path, mod_time) of
17.61 + SOME id => id
17.62 + | NONE =>
17.63 + let
17.64 + val (id, rc) = (*potentially slow*)
17.65 + bash_output
17.66 + ("\"$ISABELLE_HOME/lib/scripts/fileident\" " ^ File.shell_quote physical_path);
17.67 + in
17.68 + if id <> "" andalso rc = 0 then (update_cache (physical_path, (mod_time, id)); id)
17.69 + else error ("Failed to identify file " ^ quote (Path.implode path) ^ " by " ^ cmd)
17.70 + end))))
17.71 + end;
17.72 +
17.73 +
17.74 (* manage source files *)
17.75
17.76 type files =
17.77 - {master_dir: Path.T, (*master directory of theory source*)
17.78 - required: Path.T list, (*source path*)
17.79 - provided: (Path.T * (Path.T * File.ident)) list}; (*source path, physical path, identifier*)
17.80 + {master_dir: Path.T, (*master directory of theory source*)
17.81 + required: Path.T list, (*source path*)
17.82 + provided: (Path.T * (Path.T * file_ident)) list}; (*source path, physical path, identifier*)
17.83
17.84 fun make_files (master_dir, required, provided): files =
17.85 {master_dir = master_dir, required = required, provided = provided};
17.86 @@ -79,26 +127,26 @@
17.87 (* maintain default paths *)
17.88
17.89 local
17.90 - val load_path = Unsynchronized.ref [Path.current];
17.91 + val load_path = Synchronized.var "load_path" [Path.current];
17.92 val master_path = Unsynchronized.ref Path.current;
17.93 in
17.94
17.95 -fun show_path () = map Path.implode (! load_path);
17.96 +fun show_path () = map Path.implode (Synchronized.value load_path);
17.97
17.98 -fun del_path s =
17.99 - CRITICAL (fn () => Unsynchronized.change load_path (remove (op =) (Path.explode s)));
17.100 +fun del_path s = Synchronized.change load_path (remove (op =) (Path.explode s));
17.101
17.102 -fun add_path s =
17.103 - CRITICAL (fn () => (del_path s; Unsynchronized.change load_path (cons (Path.explode s))));
17.104 +fun add_path s = Synchronized.change load_path (update (op =) (Path.explode s));
17.105
17.106 fun path_add s =
17.107 - CRITICAL (fn () =>
17.108 - (del_path s; Unsynchronized.change load_path (fn path => path @ [Path.explode s])));
17.109 + Synchronized.change load_path (fn path =>
17.110 + let val p = Path.explode s
17.111 + in remove (op =) p path @ [p] end);
17.112
17.113 -fun reset_path () = CRITICAL (fn () => load_path := [Path.current]);
17.114 +fun reset_path () = Synchronized.change load_path (K [Path.current]);
17.115
17.116 fun search_path dir path =
17.117 - distinct (op =) (dir :: (if Path.is_basic path then (! load_path) else [Path.current]));
17.118 + distinct (op =)
17.119 + (dir :: (if Path.is_basic path then (Synchronized.value load_path) else [Path.current]));
17.120
17.121 fun set_master_path path = master_path := path;
17.122 fun get_master_path () = ! master_path;
17.123 @@ -115,7 +163,7 @@
17.124 in
17.125 dirs |> get_first (fn dir =>
17.126 let val full_path = File.full_path (Path.append dir path) in
17.127 - (case File.ident full_path of
17.128 + (case file_ident full_path of
17.129 NONE => NONE
17.130 | SOME id => SOME (full_path, id))
17.131 end)
18.1 --- a/src/Pure/pure_setup.ML Sat Nov 27 18:51:15 2010 +0100
18.2 +++ b/src/Pure/pure_setup.ML Sat Nov 27 20:48:06 2010 +0100
18.3 @@ -36,7 +36,7 @@
18.4 toplevel_pp ["Context", "Proof", "context"] "Proof_Display.pp_context";
18.5 toplevel_pp ["Syntax", "ast"] "Syntax.pretty_ast";
18.6 toplevel_pp ["Path", "T"] "Pretty.str o quote o Path.implode";
18.7 -toplevel_pp ["File", "ident"] "Pretty.str o quote o File.rep_ident";
18.8 +toplevel_pp ["Thy_Load", "file_ident"] "Thy_Load.pretty_file_ident";
18.9 toplevel_pp ["Proof", "state"] "(fn _: Proof.state => Pretty.str \"<Proof.state>\")";
18.10 toplevel_pp ["Toplevel", "state"] "Toplevel.pretty_abstract";
18.11
19.1 --- a/src/Tools/Code/code_haskell.ML Sat Nov 27 18:51:15 2010 +0100
19.2 +++ b/src/Tools/Code/code_haskell.ML Sat Nov 27 20:48:06 2010 +0100
19.3 @@ -353,7 +353,7 @@
19.4 val _ = File.check destination;
19.5 val filepath = (Path.append destination o Path.ext "hs" o Path.explode o implode
19.6 o separate "/" o Long_Name.explode) module_name;
19.7 - val _ = File.mkdir_leaf (Path.dir filepath);
19.8 + val _ = Isabelle_System.mkdir (Path.dir filepath);
19.9 in
19.10 (File.write filepath o format [] width o Pretty.chunks2)
19.11 [str "{-# OPTIONS_GHC -fglasgow-exts #-}", content]
20.1 --- a/src/Tools/cache_io.ML Sat Nov 27 18:51:15 2010 +0100
20.2 +++ b/src/Tools/cache_io.ML Sat Nov 27 20:48:06 2010 +0100
20.3 @@ -44,9 +44,9 @@
20.4 fun with_tmp_dir name f =
20.5 let
20.6 val path = File.tmp_path (Path.explode (name ^ serial_string ()))
20.7 - val _ = File.mkdir path
20.8 + val _ = Isabelle_System.mkdirs path
20.9 val x = Exn.capture f path
20.10 - val _ = try File.rm_tree path
20.11 + val _ = try Isabelle_System.rm_tree path
20.12 in Exn.release x end
20.13
20.14 type result = {