1.1 --- a/src/HOL/Tools/Nitpick/kodkod.ML Sat Nov 27 14:09:03 2010 -0800
1.2 +++ b/src/HOL/Tools/Nitpick/kodkod.ML Sat Nov 27 14:34:54 2010 -0800
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 --- a/src/HOL/ex/Eval_Examples.thy Sat Nov 27 14:09:03 2010 -0800
2.2 +++ b/src/HOL/ex/Eval_Examples.thy Sat Nov 27 14:34:54 2010 -0800
2.3 @@ -9,26 +9,26 @@
2.4 text {* evaluation oracle *}
2.5
2.6 lemma "True \<or> False" by eval
2.7 -lemma "\<not> (Suc 0 = Suc 1)" by eval
2.8 -lemma "[] = ([]\<Colon> int list)" by eval
2.9 +lemma "Suc 0 \<noteq> Suc 1" by eval
2.10 +lemma "[] = ([] :: int list)" by eval
2.11 lemma "[()] = [()]" by eval
2.12 -lemma "fst ([]::nat list, Suc 0) = []" by eval
2.13 +lemma "fst ([] :: nat list, Suc 0) = []" by eval
2.14
2.15 text {* SML evaluation oracle *}
2.16
2.17 lemma "True \<or> False" by evaluation
2.18 -lemma "\<not> (Suc 0 = Suc 1)" by evaluation
2.19 -lemma "[] = ([]\<Colon> int list)" by evaluation
2.20 +lemma "Suc 0 \<noteq> Suc 1" by evaluation
2.21 +lemma "[] = ([] :: int list)" by evaluation
2.22 lemma "[()] = [()]" by evaluation
2.23 -lemma "fst ([]::nat list, Suc 0) = []" by evaluation
2.24 +lemma "fst ([] :: nat list, Suc 0) = []" by evaluation
2.25
2.26 text {* normalization *}
2.27
2.28 lemma "True \<or> False" by normalization
2.29 -lemma "\<not> (Suc 0 = Suc 1)" by normalization
2.30 -lemma "[] = ([]\<Colon> int list)" by normalization
2.31 +lemma "Suc 0 \<noteq> Suc 1" by normalization
2.32 +lemma "[] = ([] :: int list)" by normalization
2.33 lemma "[()] = [()]" by normalization
2.34 -lemma "fst ([]::nat list, Suc 0) = []" by normalization
2.35 +lemma "fst ([] :: nat list, Suc 0) = []" by normalization
2.36
2.37 text {* term evaluation *}
2.38
2.39 @@ -47,10 +47,10 @@
2.40 value [SML] "nat 100"
2.41 value [nbe] "nat 100"
2.42
2.43 -value "(10\<Colon>int) \<le> 12"
2.44 -value [code] "(10\<Colon>int) \<le> 12"
2.45 -value [SML] "(10\<Colon>int) \<le> 12"
2.46 -value [nbe] "(10\<Colon>int) \<le> 12"
2.47 +value "(10::int) \<le> 12"
2.48 +value [code] "(10::int) \<le> 12"
2.49 +value [SML] "(10::int) \<le> 12"
2.50 +value [nbe] "(10::int) \<le> 12"
2.51
2.52 value "max (2::int) 4"
2.53 value [code] "max (2::int) 4"
2.54 @@ -62,29 +62,29 @@
2.55 value [SML] "of_int 2 / of_int 4 * (1::rat)"
2.56 value [nbe] "of_int 2 / of_int 4 * (1::rat)"
2.57
2.58 -value "[]::nat list"
2.59 -value [code] "[]::nat list"
2.60 -value [SML] "[]::nat list"
2.61 -value [nbe] "[]::nat list"
2.62 +value "[] :: nat list"
2.63 +value [code] "[] :: nat list"
2.64 +value [SML] "[] :: nat list"
2.65 +value [nbe] "[] :: nat list"
2.66
2.67 value "[(nat 100, ())]"
2.68 value [code] "[(nat 100, ())]"
2.69 value [SML] "[(nat 100, ())]"
2.70 value [nbe] "[(nat 100, ())]"
2.71
2.72 -
2.73 text {* a fancy datatype *}
2.74
2.75 -datatype ('a, 'b) bair =
2.76 - Bair "'a\<Colon>order" 'b
2.77 - | Shift "('a, 'b) cair"
2.78 - | Dummy unit
2.79 -and ('a, 'b) cair =
2.80 - Cair 'a 'b
2.81 +datatype ('a, 'b) foo =
2.82 + Foo "'a\<Colon>order" 'b
2.83 + | Bla "('a, 'b) bar"
2.84 + | Dummy nat
2.85 +and ('a, 'b) bar =
2.86 + Bar 'a 'b
2.87 + | Blubb "('a, 'b) foo"
2.88
2.89 -value "Shift (Cair (4::nat) [Suc 0])"
2.90 -value [code] "Shift (Cair (4::nat) [Suc 0])"
2.91 -value [SML] "Shift (Cair (4::nat) [Suc 0])"
2.92 -value [nbe] "Shift (Cair (4::nat) [Suc 0])"
2.93 +value "Bla (Bar (4::nat) [Suc 0])"
2.94 +value [code] "Bla (Bar (4::nat) [Suc 0])"
2.95 +value [SML] "Bla (Bar (4::nat) [Suc 0])"
2.96 +value [nbe] "Bla (Bar (4::nat) [Suc 0])"
2.97
2.98 end
3.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
3.2 +++ b/src/Pure/Concurrent/bash.ML Sat Nov 27 14:34:54 2010 -0800
3.3 @@ -0,0 +1,83 @@
3.4 +(* Title: Pure/Concurrent/bash.ML
3.5 + Author: Makarius
3.6 +
3.7 +GNU bash processes, with propagation of interrupts.
3.8 +*)
3.9 +
3.10 +val bash_output = uninterruptible (fn restore_attributes => fn script =>
3.11 + let
3.12 + datatype result = Wait | Signal | Result of int;
3.13 + val result = Synchronized.var "bash_result" Wait;
3.14 +
3.15 + val id = serial_string ();
3.16 + val script_path = File.tmp_path (Path.basic ("bash_script" ^ id));
3.17 + val output_path = File.tmp_path (Path.basic ("bash_output" ^ id));
3.18 + val pid_path = File.tmp_path (Path.basic ("bash_pid" ^ id));
3.19 +
3.20 + val system_thread =
3.21 + Simple_Thread.fork false (fn () =>
3.22 + Multithreading.with_attributes Multithreading.private_interrupts (fn _ =>
3.23 + let
3.24 + val _ = File.write script_path script;
3.25 + val status =
3.26 + OS.Process.system
3.27 + ("exec \"$ISABELLE_HOME/lib/scripts/process\" group " ^
3.28 + File.shell_path pid_path ^ " script \"exec bash " ^
3.29 + File.shell_path script_path ^ " > " ^
3.30 + File.shell_path output_path ^ "\"");
3.31 + val res =
3.32 + (case Posix.Process.fromStatus status of
3.33 + Posix.Process.W_EXITED => Result 0
3.34 + | Posix.Process.W_EXITSTATUS 0wx82 => Signal
3.35 + | Posix.Process.W_EXITSTATUS w => Result (Word8.toInt w)
3.36 + | Posix.Process.W_SIGNALED s =>
3.37 + if s = Posix.Signal.int then Signal
3.38 + else Result (256 + LargeWord.toInt (Posix.Signal.toWord s))
3.39 + | Posix.Process.W_STOPPED s =>
3.40 + Result (512 + LargeWord.toInt (Posix.Signal.toWord s)));
3.41 + in Synchronized.change result (K res) end
3.42 + handle _ (*sic*) => Synchronized.change result (fn Wait => Signal | res => res)));
3.43 +
3.44 + fun terminate () =
3.45 + let
3.46 + val sig_test = Posix.Signal.fromWord 0w0;
3.47 +
3.48 + fun kill_group pid s =
3.49 + (Posix.Process.kill
3.50 + (Posix.Process.K_GROUP (Posix.Process.wordToPid (LargeWord.fromInt pid)), s); true)
3.51 + handle OS.SysErr _ => false;
3.52 +
3.53 + fun kill s =
3.54 + (case Int.fromString (File.read pid_path) of
3.55 + NONE => true
3.56 + | SOME pid => (kill_group pid s; kill_group pid sig_test))
3.57 + handle IO.Io _ => true;
3.58 +
3.59 + fun multi_kill count s =
3.60 + count = 0 orelse
3.61 + kill s andalso (OS.Process.sleep (seconds 0.1); multi_kill (count - 1) s);
3.62 + val _ =
3.63 + multi_kill 10 Posix.Signal.int andalso
3.64 + multi_kill 10 Posix.Signal.term andalso
3.65 + multi_kill 10 Posix.Signal.kill;
3.66 + in () end;
3.67 +
3.68 + fun cleanup () =
3.69 + (terminate ();
3.70 + Simple_Thread.interrupt system_thread;
3.71 + try File.rm script_path;
3.72 + try File.rm output_path;
3.73 + try File.rm pid_path);
3.74 + in
3.75 + let
3.76 + val _ =
3.77 + restore_attributes (fn () =>
3.78 + Synchronized.guarded_access result (fn Wait => NONE | x => SOME ((), x))) ();
3.79 +
3.80 + val output = the_default "" (try File.read output_path);
3.81 + val rc = (case Synchronized.value result of Signal => Exn.interrupt () | Result rc => rc);
3.82 + val _ = cleanup ();
3.83 + in (output, rc) end
3.84 + handle exn => (cleanup (); reraise exn)
3.85 + end);
3.86 +
4.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
4.2 +++ b/src/Pure/Concurrent/bash_sequential.ML Sat Nov 27 14:34:54 2010 -0800
4.3 @@ -0,0 +1,34 @@
4.4 +(* Title: Pure/Concurrent/bash_sequential.ML
4.5 + Author: Makarius
4.6 +
4.7 +Generic GNU bash processes (no provisions to propagate interrupts, but
4.8 +could work via the controlling tty).
4.9 +*)
4.10 +
4.11 +fun bash_output script =
4.12 + let
4.13 + val id = serial_string ();
4.14 + val script_path = File.tmp_path (Path.basic ("bash_script" ^ id));
4.15 + val output_path = File.tmp_path (Path.basic ("bash_output" ^ id));
4.16 + fun cleanup () = (try File.rm script_path; try File.rm output_path);
4.17 + in
4.18 + let
4.19 + val _ = File.write script_path script;
4.20 + val status =
4.21 + OS.Process.system
4.22 + ("exec \"$ISABELLE_HOME/lib/scripts/process\" no_group /dev/null" ^
4.23 + " script \"exec bash " ^ File.shell_path script_path ^ " > " ^
4.24 + File.shell_path output_path ^ "\"");
4.25 + val rc =
4.26 + (case Posix.Process.fromStatus status of
4.27 + Posix.Process.W_EXITED => 0
4.28 + | Posix.Process.W_EXITSTATUS w => Word8.toInt w
4.29 + | Posix.Process.W_SIGNALED s => 256 + LargeWord.toInt (Posix.Signal.toWord s)
4.30 + | Posix.Process.W_STOPPED s => 512 + LargeWord.toInt (Posix.Signal.toWord s));
4.31 +
4.32 + val output = the_default "" (try File.read output_path);
4.33 + val _ = cleanup ();
4.34 + in (output, rc) end
4.35 + handle exn => (cleanup (); reraise exn)
4.36 + end;
4.37 +
5.1 --- a/src/Pure/General/file.ML Sat Nov 27 14:09:03 2010 -0800
5.2 +++ b/src/Pure/General/file.ML Sat Nov 27 14:34:54 2010 -0800
5.3 @@ -13,16 +13,9 @@
5.4 val pwd: unit -> Path.T
5.5 val full_path: Path.T -> Path.T
5.6 val tmp_path: Path.T -> Path.T
5.7 - val isabelle_tool: string -> string -> int
5.8 - eqtype ident
5.9 - val rep_ident: ident -> string
5.10 - val ident: Path.T -> ident option
5.11 val exists: Path.T -> bool
5.12 val check: Path.T -> unit
5.13 val rm: Path.T -> unit
5.14 - val rm_tree: Path.T -> unit
5.15 - val mkdir: Path.T -> unit
5.16 - val mkdir_leaf: Path.T -> unit
5.17 val open_input: (TextIO.instream -> 'a) -> Path.T -> 'a
5.18 val open_output: (TextIO.outstream -> 'a) -> Path.T -> 'a
5.19 val open_append: (TextIO.outstream -> 'a) -> Path.T -> 'a
5.20 @@ -35,7 +28,6 @@
5.21 val write_buffer: Path.T -> Buffer.T -> unit
5.22 val eq: Path.T * Path.T -> bool
5.23 val copy: Path.T -> Path.T -> unit
5.24 - val copy_dir: Path.T -> Path.T -> unit
5.25 end;
5.26
5.27 structure File: FILE =
5.28 @@ -45,7 +37,11 @@
5.29
5.30 val platform_path = Path.implode o Path.expand;
5.31
5.32 -val shell_quote = enclose "'" "'";
5.33 +fun shell_quote s =
5.34 + if exists_string (fn c => c = "'") s then
5.35 + error ("Illegal single quote in path specification: " ^ quote s)
5.36 + else enclose "'" "'" s;
5.37 +
5.38 val shell_path = shell_quote o platform_path;
5.39
5.40
5.41 @@ -65,66 +61,6 @@
5.42 Path.append (Path.variable "ISABELLE_TMP") (Path.base path);
5.43
5.44
5.45 -(* system commands *)
5.46 -
5.47 -fun isabelle_tool name args =
5.48 - (case space_explode ":" (getenv "ISABELLE_TOOLS") |> get_first (fn dir =>
5.49 - let val path = dir ^ "/" ^ name in
5.50 - if can OS.FileSys.modTime path andalso
5.51 - not (OS.FileSys.isDir path) andalso
5.52 - OS.FileSys.access (path, [OS.FileSys.A_READ, OS.FileSys.A_EXEC])
5.53 - then SOME path
5.54 - else NONE
5.55 - end handle OS.SysErr _ => NONE) of
5.56 - SOME path => bash (shell_quote path ^ " " ^ args)
5.57 - | NONE => (writeln ("Unknown Isabelle tool: " ^ name); 2));
5.58 -
5.59 -fun system_command cmd =
5.60 - if bash cmd <> 0 then error ("System command failed: " ^ cmd)
5.61 - else ();
5.62 -
5.63 -
5.64 -(* file identification *)
5.65 -
5.66 -local
5.67 - val ident_cache =
5.68 - Unsynchronized.ref (Symtab.empty: {time_stamp: string, id: string} Symtab.table);
5.69 -in
5.70 -
5.71 -fun check_cache (path, time) =
5.72 - (case Symtab.lookup (! ident_cache) path of
5.73 - NONE => NONE
5.74 - | SOME {time_stamp, id} => if time_stamp = time then SOME id else NONE);
5.75 -
5.76 -fun update_cache (path, (time, id)) = CRITICAL (fn () =>
5.77 - Unsynchronized.change ident_cache
5.78 - (Symtab.update (path, {time_stamp = time, id = id})));
5.79 -
5.80 -end;
5.81 -
5.82 -datatype ident = Ident of string;
5.83 -fun rep_ident (Ident s) = s;
5.84 -
5.85 -fun ident path =
5.86 - let val physical_path = perhaps (try OS.FileSys.fullPath) (platform_path path) in
5.87 - (case try (Time.toString o OS.FileSys.modTime) physical_path of
5.88 - NONE => NONE
5.89 - | SOME mod_time => SOME (Ident
5.90 - (case getenv "ISABELLE_FILE_IDENT" of
5.91 - "" => physical_path ^ ": " ^ mod_time
5.92 - | cmd =>
5.93 - (case check_cache (physical_path, mod_time) of
5.94 - SOME id => id
5.95 - | NONE =>
5.96 - let val (id, rc) = (*potentially slow*)
5.97 - bash_output ("\"$ISABELLE_HOME/lib/scripts/fileident\" " ^ shell_quote physical_path)
5.98 - in
5.99 - if id <> "" andalso rc = 0 then (update_cache (physical_path, (mod_time, id)); id)
5.100 - else error ("Failed to identify file " ^ quote (Path.implode path) ^ " by " ^ cmd)
5.101 - end))))
5.102 - end;
5.103 -
5.104 -
5.105 (* directory entries *)
5.106
5.107 val exists = can OS.FileSys.modTime o platform_path;
5.108 @@ -135,15 +71,6 @@
5.109
5.110 val rm = OS.FileSys.remove o platform_path;
5.111
5.112 -fun rm_tree path = system_command ("rm -r " ^ shell_path path);
5.113 -
5.114 -fun mkdir path = system_command ("mkdir -p " ^ shell_path path);
5.115 -
5.116 -fun mkdir_leaf path = (check (Path.dir path); mkdir path);
5.117 -
5.118 -fun is_dir path =
5.119 - the_default false (try OS.FileSys.isDir (platform_path path));
5.120 -
5.121
5.122 (* open files *)
5.123
5.124 @@ -201,14 +128,13 @@
5.125 SOME ids => is_equal (OS.FileSys.compare ids)
5.126 | NONE => false);
5.127
5.128 +fun is_dir path =
5.129 + the_default false (try OS.FileSys.isDir (platform_path path));
5.130 +
5.131 fun copy src dst =
5.132 if eq (src, dst) then ()
5.133 else
5.134 let val target = if is_dir dst then Path.append dst (Path.base src) else dst
5.135 in write target (read src) end;
5.136
5.137 -fun copy_dir src dst =
5.138 - if eq (src, dst) then ()
5.139 - else (system_command ("cp -r -f " ^ shell_path src ^ "/. " ^ shell_path dst); ());
5.140 -
5.141 end;
6.1 --- a/src/Pure/General/secure.ML Sat Nov 27 14:09:03 2010 -0800
6.2 +++ b/src/Pure/General/secure.ML Sat Nov 27 14:34:54 2010 -0800
6.3 @@ -15,8 +15,6 @@
6.4 val toplevel_pp: string list -> string -> unit
6.5 val PG_setup: unit -> unit
6.6 val commit: unit -> unit
6.7 - val bash_output: string -> string * int
6.8 - val bash: string -> int
6.9 end;
6.10
6.11 structure Secure: SECURE =
6.12 @@ -58,20 +56,6 @@
6.13 fun PG_setup () =
6.14 use_global "val change = Unsynchronized.change; structure ThyLoad = ProofGeneral.ThyLoad;";
6.15
6.16 -
6.17 -(* shell commands *)
6.18 -
6.19 -fun secure_shell () = deny_secure "Cannot execute shell commands in secure mode";
6.20 -
6.21 -val orig_bash_output = bash_output;
6.22 -
6.23 -fun bash_output s = (secure_shell (); orig_bash_output s);
6.24 -
6.25 -fun bash s =
6.26 - (case bash_output s of
6.27 - ("", rc) => rc
6.28 - | (out, rc) => (writeln (perhaps (try (unsuffix "\n")) out); rc));
6.29 -
6.30 end;
6.31
6.32 (*override previous toplevel bindings!*)
6.33 @@ -80,5 +64,4 @@
6.34 fun use s = Secure.use_file ML_Parse.global_context true s
6.35 handle ERROR msg => (writeln msg; error "ML error");
6.36 val toplevel_pp = Secure.toplevel_pp;
6.37 -val bash_output = Secure.bash_output;
6.38 -val bash = Secure.bash;
6.39 +
7.1 --- a/src/Pure/IsaMakefile Sat Nov 27 14:09:03 2010 -0800
7.2 +++ b/src/Pure/IsaMakefile Sat Nov 27 14:34:54 2010 -0800
7.3 @@ -22,7 +22,6 @@
7.4 BOOTSTRAP_FILES = \
7.5 General/exn.ML \
7.6 General/timing.ML \
7.7 - ML-Systems/bash.ML \
7.8 ML-Systems/compiler_polyml-5.2.ML \
7.9 ML-Systems/compiler_polyml-5.3.ML \
7.10 ML-Systems/ml_name_space.ML \
7.11 @@ -55,6 +54,8 @@
7.12 Pure: $(OUT)/Pure
7.13
7.14 $(OUT)/Pure: $(BOOTSTRAP_FILES) \
7.15 + Concurrent/bash.ML \
7.16 + Concurrent/bash_sequential.ML \
7.17 Concurrent/cache.ML \
7.18 Concurrent/future.ML \
7.19 Concurrent/lazy.ML \
7.20 @@ -188,6 +189,7 @@
7.21 Syntax/syntax.ML \
7.22 Syntax/type_ext.ML \
7.23 System/isabelle_process.ML \
7.24 + System/isabelle_system.ML \
7.25 System/isar.ML \
7.26 System/session.ML \
7.27 Thy/html.ML \
8.1 --- a/src/Pure/Isar/code.ML Sat Nov 27 14:09:03 2010 -0800
8.2 +++ b/src/Pure/Isar/code.ML Sat Nov 27 14:34:54 2010 -0800
8.3 @@ -316,7 +316,7 @@
8.4 val data = case Datatab.lookup datatab kind
8.5 of SOME data => data
8.6 | NONE => invoke_init kind;
8.7 - val result as (x, data') = f (dest data);
8.8 + val result as (_, data') = f (dest data);
8.9 val _ = Synchronized.change dataref
8.10 ((K o SOME) (Datatab.update (kind, mk data') datatab, thy_ref));
8.11 in result end;
8.12 @@ -358,11 +358,13 @@
8.13 of SOME ty => ty
8.14 | NONE => (Type.strip_sorts o Sign.the_const_type thy) c;
8.15
8.16 +fun args_number thy = length o fst o strip_type o const_typ thy;
8.17 +
8.18 fun subst_signature thy c ty =
8.19 let
8.20 - fun mk_subst (Type (tyco, tys1)) (ty2 as Type (tyco2, tys2)) =
8.21 + fun mk_subst (Type (_, tys1)) (Type (_, tys2)) =
8.22 fold2 mk_subst tys1 tys2
8.23 - | mk_subst ty (TVar (v, sort)) = Vartab.update (v, ([], ty))
8.24 + | mk_subst ty (TVar (v, _)) = Vartab.update (v, ([], ty))
8.25 in case lookup_typ thy c
8.26 of SOME ty' => Envir.subst_type (mk_subst ty (expand_signature thy ty') Vartab.empty) ty'
8.27 | NONE => ty
8.28 @@ -370,7 +372,10 @@
8.29
8.30 fun subst_signatures thy = map_aterms (fn Const (c, ty) => Const (c, subst_signature thy c ty) | t => t);
8.31
8.32 -fun args_number thy = length o fst o strip_type o const_typ thy;
8.33 +fun logical_typscheme thy (c, ty) =
8.34 + (map dest_TFree (Sign.const_typargs thy (c, ty)), Type.strip_sorts ty);
8.35 +
8.36 +fun typscheme thy (c, ty) = logical_typscheme thy (c, subst_signature thy c ty);
8.37
8.38
8.39 (* datatypes *)
8.40 @@ -407,13 +412,14 @@
8.41 val _ = if (tyco' : string) <> tyco
8.42 then error "Different type constructors in constructor set"
8.43 else ();
8.44 - val sorts'' = map2 (curry (Sorts.inter_sort (Sign.classes_of thy))) sorts' sorts
8.45 - in ((tyco, sorts), c :: cs) end;
8.46 + val sorts'' =
8.47 + map2 (curry (Sorts.inter_sort (Sign.classes_of thy))) sorts' sorts
8.48 + in ((tyco, sorts''), c :: cs) end;
8.49 fun inst vs' (c, (vs, ty)) =
8.50 let
8.51 val the_v = the o AList.lookup (op =) (vs ~~ vs');
8.52 val ty' = map_atyps (fn TFree (v, _) => TFree (the_v v)) ty;
8.53 - val vs'' = map dest_TFree (Sign.const_typargs thy (c, ty'));
8.54 + val (vs'', _) = logical_typscheme thy (c, ty');
8.55 in (c, (vs'', (fst o strip_type) ty')) end;
8.56 val c' :: cs' = map (ty_sorts thy) cs;
8.57 val ((tyco, sorts), cs'') = fold add cs' (apsnd single c');
8.58 @@ -439,7 +445,7 @@
8.59
8.60 fun get_type_of_constr_or_abstr thy c =
8.61 case (snd o strip_type o const_typ thy) c
8.62 - of Type (tyco, _) => let val ((vs, cos), abstract) = get_type thy tyco
8.63 + of Type (tyco, _) => let val ((_, cos), abstract) = get_type thy tyco
8.64 in if member (op =) (map fst cos) c then SOME (tyco, abstract) else NONE end
8.65 | _ => NONE;
8.66
8.67 @@ -592,11 +598,6 @@
8.68 fun const_abs_eqn thy = AxClass.unoverload_const thy o dest_Const o fst o strip_comb o snd
8.69 o dest_comb o fst o Logic.dest_equals o Thm.plain_prop_of;
8.70
8.71 -fun logical_typscheme thy (c, ty) =
8.72 - (map dest_TFree (Sign.const_typargs thy (c, ty)), Type.strip_sorts ty);
8.73 -
8.74 -fun typscheme thy (c, ty) = logical_typscheme thy (c, subst_signature thy c ty);
8.75 -
8.76 fun mk_proj tyco vs ty abs rep =
8.77 let
8.78 val ty_abs = Type (tyco, map TFree vs);
8.79 @@ -641,19 +642,19 @@
8.80 else SOME (((v, i), x), mk ((v', 0), x))) (vs ~~ names)
8.81 end;
8.82
8.83 -fun desymbolize_tvars thy thms =
8.84 +fun desymbolize_tvars thms =
8.85 let
8.86 val tvs = fold (Term.add_tvars o Thm.prop_of) thms [];
8.87 val tvar_subst = mk_desymbolization (unprefix "'") (prefix "'") TVar tvs;
8.88 in map (Thm.certify_instantiate (tvar_subst, [])) thms end;
8.89
8.90 -fun desymbolize_vars thy thm =
8.91 +fun desymbolize_vars thm =
8.92 let
8.93 val vs = Term.add_vars (Thm.prop_of thm) [];
8.94 val var_subst = mk_desymbolization I I Var vs;
8.95 in Thm.certify_instantiate ([], var_subst) thm end;
8.96
8.97 -fun canonize_thms thy = desymbolize_tvars thy #> same_arity thy #> map (desymbolize_vars thy);
8.98 +fun canonize_thms thy = desymbolize_tvars #> same_arity thy #> map desymbolize_vars;
8.99
8.100
8.101 (* abstype certificates *)
8.102 @@ -672,13 +673,12 @@
8.103 then error ("Is a class parameter: " ^ string_of_const thy c) else ()) (abs, rep);
8.104 val _ = check_decl_ty thy (abs, raw_ty);
8.105 val _ = check_decl_ty thy (rep, rep_ty);
8.106 - val var = (fst o dest_Var) param
8.107 + val _ = (fst o dest_Var) param
8.108 handle TERM _ => bad "Not an abstype certificate";
8.109 val _ = if param = rhs then () else bad "Not an abstype certificate";
8.110 val ((tyco, sorts), (abs, (vs, ty'))) = ty_sorts thy (abs, Logic.unvarifyT_global raw_ty);
8.111 val ty = domain_type ty';
8.112 - val vs' = map dest_TFree (Sign.const_typargs thy (abs, ty'));
8.113 - val ty_abs = range_type ty';
8.114 + val (vs', _) = logical_typscheme thy (abs, ty');
8.115 in (tyco, (vs ~~ sorts, ((abs, (vs', ty)), (rep, thm)))) end;
8.116
8.117
8.118 @@ -716,7 +716,7 @@
8.119
8.120 fun concretify_abs thy tyco abs_thm =
8.121 let
8.122 - val (vs, ((c, _), (_, cert))) = get_abstype_spec thy tyco;
8.123 + val (_, ((c, _), (_, cert))) = get_abstype_spec thy tyco;
8.124 val lhs = (fst o Logic.dest_equals o Thm.prop_of) abs_thm
8.125 val ty = fastype_of lhs;
8.126 val ty_abs = (fastype_of o snd o dest_comb) lhs;
8.127 @@ -742,13 +742,16 @@
8.128
8.129 fun empty_cert thy c =
8.130 let
8.131 - val raw_ty = const_typ thy c;
8.132 - val tvars = Term.add_tvar_namesT raw_ty [];
8.133 - val tvars' = case AxClass.class_of_param thy c
8.134 - of SOME class => [TFree (Name.aT, [class])]
8.135 - | NONE => Name.invent_list [] Name.aT (length tvars)
8.136 - |> map (fn v => TFree (v, []));
8.137 - val ty = typ_subst_TVars (tvars ~~ tvars') raw_ty;
8.138 + val raw_ty = Logic.unvarifyT_global (const_typ thy c);
8.139 + val (vs, _) = logical_typscheme thy (c, raw_ty);
8.140 + val sortargs = case AxClass.class_of_param thy c
8.141 + of SOME class => [[class]]
8.142 + | NONE => (case get_type_of_constr_or_abstr thy c
8.143 + of SOME (tyco, _) => (map snd o fst o the)
8.144 + (AList.lookup (op =) ((snd o fst o get_type thy) tyco) c)
8.145 + | NONE => replicate (length vs) []);
8.146 + val the_sort = the o AList.lookup (op =) (map fst vs ~~ sortargs);
8.147 + val ty = map_type_tfree (fn (v, _) => TFree (v, the_sort v)) raw_ty
8.148 val chead = build_head thy (c, ty);
8.149 in Equations (Thm.weaken chead Drule.dummy_thm, []) end;
8.150
8.151 @@ -767,19 +770,19 @@
8.152 fold (curry (Sorts.inter_sort (Sign.classes_of thy)) o snd) vs [];
8.153 val sorts = map_transpose inter_sorts vss;
8.154 val vts = Name.names Name.context Name.aT sorts;
8.155 - val thms as thm :: _ =
8.156 + val thms' =
8.157 map2 (fn vs => Thm.certify_instantiate (vs ~~ map TFree vts, [])) vss thms;
8.158 - val head_thm = Thm.symmetric (Thm.assume (build_head thy (head_eqn (hd thms))));
8.159 + val head_thm = Thm.symmetric (Thm.assume (build_head thy (head_eqn (hd thms'))));
8.160 fun head_conv ct = if can Thm.dest_comb ct
8.161 then Conv.fun_conv head_conv ct
8.162 else Conv.rewr_conv head_thm ct;
8.163 val rewrite_head = Conv.fconv_rule (Conv.arg1_conv head_conv);
8.164 - val cert_thm = Conjunction.intr_balanced (map rewrite_head thms);
8.165 + val cert_thm = Conjunction.intr_balanced (map rewrite_head thms');
8.166 in Equations (cert_thm, propers) end;
8.167
8.168 fun cert_of_proj thy c tyco =
8.169 let
8.170 - val (vs, ((abs, (_, ty)), (rep, cert))) = get_abstype_spec thy tyco;
8.171 + val (vs, ((abs, (_, ty)), (rep, _))) = get_abstype_spec thy tyco;
8.172 val _ = if c = rep then () else
8.173 error ("Wrong head of projection,\nexpected constant " ^ string_of_const thy rep);
8.174 in Projection (mk_proj tyco vs ty abs rep, tyco) end;
8.175 @@ -824,7 +827,7 @@
8.176 Thm.prop_of cert_thm
8.177 |> Logic.dest_conjunction_balanced (length propers);
8.178 in (vs, fold (add_rhss_of_eqn thy) equations []) end
8.179 - | typargs_deps_of_cert thy (Projection (t, tyco)) =
8.180 + | typargs_deps_of_cert thy (Projection (t, _)) =
8.181 (fst (typscheme_projection thy t), add_rhss_of_eqn thy t [])
8.182 | typargs_deps_of_cert thy (Abstract (abs_thm, tyco)) =
8.183 let
8.184 @@ -864,7 +867,7 @@
8.185 o snd o equations_of_cert thy) cert
8.186 | pretty_cert thy (Projection (t, _)) =
8.187 [Syntax.pretty_term_global thy (map_types Logic.varifyT_global t)]
8.188 - | pretty_cert thy (Abstract (abs_thm, tyco)) =
8.189 + | pretty_cert thy (Abstract (abs_thm, _)) =
8.190 [(Display.pretty_thm_global thy o AxClass.overload thy o Thm.varifyT_global) abs_thm];
8.191
8.192 fun bare_thms_of_cert thy (cert as Equations _) =
8.193 @@ -1118,7 +1121,7 @@
8.194
8.195 fun del_eqn thm thy = case mk_eqn_liberal thy thm
8.196 of SOME (thm, _) => let
8.197 - fun del_eqn' (Default eqns) = empty_fun_spec
8.198 + fun del_eqn' (Default _) = empty_fun_spec
8.199 | del_eqn' (Eqns eqns) =
8.200 Eqns (filter_out (fn (thm', _) => Thm.eq_thm_prop (thm, thm')) eqns)
8.201 | del_eqn' spec = spec
8.202 @@ -1130,7 +1133,7 @@
8.203
8.204 (* cases *)
8.205
8.206 -fun case_cong thy case_const (num_args, (pos, constrs)) =
8.207 +fun case_cong thy case_const (num_args, (pos, _)) =
8.208 let
8.209 val ([x, y], ctxt) = Name.variants ["A", "A'"] Name.context;
8.210 val (zs, _) = Name.variants (replicate (num_args - 1) "") ctxt;
9.1 --- a/src/Pure/Isar/isar_cmd.ML Sat Nov 27 14:09:03 2010 -0800
9.2 +++ b/src/Pure/Isar/isar_cmd.ML Sat Nov 27 14:34:54 2010 -0800
9.3 @@ -291,11 +291,11 @@
9.4
9.5 fun display_drafts files = Toplevel.imperative (fn () =>
9.6 let val outfile = File.shell_path (Present.drafts (getenv "ISABELLE_DOC_FORMAT") files)
9.7 - in File.isabelle_tool "display" ("-c " ^ outfile ^ " &"); () end);
9.8 + in Isabelle_System.isabelle_tool "display" ("-c " ^ outfile ^ " &"); () end);
9.9
9.10 fun print_drafts files = Toplevel.imperative (fn () =>
9.11 let val outfile = File.shell_path (Present.drafts "ps" files)
9.12 - in File.isabelle_tool "print" ("-c " ^ outfile); () end);
9.13 + in Isabelle_System.isabelle_tool "print" ("-c " ^ outfile); () end);
9.14
9.15
9.16 (* print parts of theory and proof context *)
10.1 --- a/src/Pure/ML-Systems/bash.ML Sat Nov 27 14:09:03 2010 -0800
10.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
10.3 @@ -1,43 +0,0 @@
10.4 -(* Title: Pure/ML-Systems/bash.ML
10.5 - Author: Makarius
10.6 -
10.7 -Generic GNU bash processes (no provisions to propagate interrupts, but
10.8 -could work via the controlling tty).
10.9 -*)
10.10 -
10.11 -local
10.12 -
10.13 -fun read_file name =
10.14 - let val is = TextIO.openIn name
10.15 - in Exn.release (Exn.capture TextIO.inputAll is before TextIO.closeIn is) end;
10.16 -
10.17 -fun write_file name txt =
10.18 - let val os = TextIO.openOut name
10.19 - in Exn.release (Exn.capture TextIO.output (os, txt) before TextIO.closeOut os) end;
10.20 -
10.21 -in
10.22 -
10.23 -fun bash_output script =
10.24 - let
10.25 - val script_name = OS.FileSys.tmpName ();
10.26 - val _ = write_file script_name script;
10.27 -
10.28 - val output_name = OS.FileSys.tmpName ();
10.29 -
10.30 - val status =
10.31 - OS.Process.system ("exec \"$ISABELLE_HOME/lib/scripts/process\" no_group /dev/null" ^
10.32 - " script \"exec bash " ^ script_name ^ " > " ^ output_name ^ "\"");
10.33 - val rc =
10.34 - (case Posix.Process.fromStatus status of
10.35 - Posix.Process.W_EXITED => 0
10.36 - | Posix.Process.W_EXITSTATUS w => Word8.toInt w
10.37 - | Posix.Process.W_SIGNALED s => 256 + LargeWord.toInt (Posix.Signal.toWord s)
10.38 - | Posix.Process.W_STOPPED s => 512 + LargeWord.toInt (Posix.Signal.toWord s));
10.39 -
10.40 - val output = read_file output_name handle IO.Io _ => "";
10.41 - val _ = OS.FileSys.remove script_name handle OS.SysErr _ => ();
10.42 - val _ = OS.FileSys.remove output_name handle OS.SysErr _ => ();
10.43 - in (output, rc) end;
10.44 -
10.45 -end;
10.46 -
11.1 --- a/src/Pure/ML-Systems/multithreading_polyml.ML Sat Nov 27 14:09:03 2010 -0800
11.2 +++ b/src/Pure/ML-Systems/multithreading_polyml.ML Sat Nov 27 14:34:54 2010 -0800
11.3 @@ -8,7 +8,6 @@
11.4 sig
11.5 val interruptible: ('a -> 'b) -> 'a -> 'b
11.6 val uninterruptible: ((('c -> 'd) -> 'c -> 'd) -> 'a -> 'b) -> 'a -> 'b
11.7 - val bash_output: string -> string * int
11.8 structure TimeLimit: TIME_LIMIT
11.9 end;
11.10
11.11 @@ -42,20 +41,6 @@
11.12 fun enabled () = max_threads_value () > 1;
11.13
11.14
11.15 -(* misc utils *)
11.16 -
11.17 -fun show "" = "" | show name = " " ^ name;
11.18 -fun show' "" = "" | show' name = " [" ^ name ^ "]";
11.19 -
11.20 -fun read_file name =
11.21 - let val is = TextIO.openIn name
11.22 - in Exn.release (Exn.capture TextIO.inputAll is before TextIO.closeIn is) end;
11.23 -
11.24 -fun write_file name txt =
11.25 - let val os = TextIO.openOut name
11.26 - in Exn.release (Exn.capture TextIO.output (os, txt) before TextIO.closeOut os) end;
11.27 -
11.28 -
11.29 (* thread attributes *)
11.30
11.31 val no_interrupts =
11.32 @@ -156,71 +141,6 @@
11.33 end;
11.34
11.35
11.36 -(* GNU bash processes, with propagation of interrupts *)
11.37 -
11.38 -fun bash_output script = with_attributes no_interrupts (fn orig_atts =>
11.39 - let
11.40 - val script_name = OS.FileSys.tmpName ();
11.41 - val _ = write_file script_name script;
11.42 -
11.43 - val pid_name = OS.FileSys.tmpName ();
11.44 - val output_name = OS.FileSys.tmpName ();
11.45 -
11.46 - (*result state*)
11.47 - datatype result = Wait | Signal | Result of int;
11.48 - val result = ref Wait;
11.49 - val lock = Mutex.mutex ();
11.50 - val cond = ConditionVar.conditionVar ();
11.51 - fun set_result res =
11.52 - (Mutex.lock lock; result := res; ConditionVar.signal cond; Mutex.unlock lock);
11.53 -
11.54 - val _ = Mutex.lock lock;
11.55 -
11.56 - (*system thread*)
11.57 - val system_thread = Thread.fork (fn () =>
11.58 - let
11.59 - val status =
11.60 - OS.Process.system ("exec \"$ISABELLE_HOME/lib/scripts/process\" group " ^ pid_name ^
11.61 - " script \"exec bash " ^ script_name ^ " > " ^ output_name ^ "\"");
11.62 - val res =
11.63 - (case Posix.Process.fromStatus status of
11.64 - Posix.Process.W_EXITED => Result 0
11.65 - | Posix.Process.W_EXITSTATUS 0wx82 => Signal
11.66 - | Posix.Process.W_EXITSTATUS w => Result (Word8.toInt w)
11.67 - | Posix.Process.W_SIGNALED s =>
11.68 - if s = Posix.Signal.int then Signal
11.69 - else Result (256 + LargeWord.toInt (Posix.Signal.toWord s))
11.70 - | Posix.Process.W_STOPPED s => Result (512 + LargeWord.toInt (Posix.Signal.toWord s)));
11.71 - in set_result res end handle _ (*sic*) => set_result (Result 2), []);
11.72 -
11.73 - (*main thread -- proxy for interrupts*)
11.74 - fun kill n =
11.75 - (case Int.fromString (read_file pid_name) of
11.76 - SOME pid =>
11.77 - Posix.Process.kill
11.78 - (Posix.Process.K_GROUP (Posix.Process.wordToPid (LargeWord.fromInt pid)),
11.79 - Posix.Signal.int)
11.80 - | NONE => ())
11.81 - handle OS.SysErr _ => () | IO.Io _ =>
11.82 - (OS.Process.sleep (seconds 0.1); if n > 0 then kill (n - 1) else ());
11.83 -
11.84 - val _ =
11.85 - while ! result = Wait do
11.86 - let val res =
11.87 - sync_wait (SOME orig_atts)
11.88 - (SOME (Time.+ (Time.now (), seconds 0.1))) cond lock
11.89 - in if Exn.is_interrupt_exn res then kill 10 else () end;
11.90 -
11.91 - (*cleanup*)
11.92 - val output = read_file output_name handle IO.Io _ => "";
11.93 - val _ = OS.FileSys.remove script_name handle OS.SysErr _ => ();
11.94 - val _ = OS.FileSys.remove pid_name handle OS.SysErr _ => ();
11.95 - val _ = OS.FileSys.remove output_name handle OS.SysErr _ => ();
11.96 - val _ = Thread.interrupt system_thread handle Thread _ => ();
11.97 - val rc = (case ! result of Signal => Exn.interrupt () | Result rc => rc);
11.98 - in (output, rc) end);
11.99 -
11.100 -
11.101 (* critical section -- may be nested within the same thread *)
11.102
11.103 local
11.104 @@ -229,6 +149,9 @@
11.105 val critical_thread = ref (NONE: Thread.thread option);
11.106 val critical_name = ref "";
11.107
11.108 +fun show "" = "" | show name = " " ^ name;
11.109 +fun show' "" = "" | show' name = " [" ^ name ^ "]";
11.110 +
11.111 in
11.112
11.113 fun self_critical () =
12.1 --- a/src/Pure/ML-Systems/polyml_common.ML Sat Nov 27 14:09:03 2010 -0800
12.2 +++ b/src/Pure/ML-Systems/polyml_common.ML Sat Nov 27 14:34:54 2010 -0800
12.3 @@ -14,7 +14,6 @@
12.4 use "ML-Systems/multithreading.ML";
12.5 use "ML-Systems/time_limit.ML";
12.6 use "General/timing.ML";
12.7 -use "ML-Systems/bash.ML";
12.8 use "ML-Systems/ml_pretty.ML";
12.9 use "ML-Systems/use_context.ML";
12.10
13.1 --- a/src/Pure/ML-Systems/proper_int.ML Sat Nov 27 14:09:03 2010 -0800
13.2 +++ b/src/Pure/ML-Systems/proper_int.ML Sat Nov 27 14:34:54 2010 -0800
13.3 @@ -165,6 +165,15 @@
13.4 val fromInt = Word.fromInt o dest_int;
13.5 end;
13.6
13.7 +structure Word8 =
13.8 +struct
13.9 + open Word8;
13.10 + val wordSize = mk_int Word8.wordSize;
13.11 + val toInt = mk_int o Word8.toInt;
13.12 + val toIntX = mk_int o Word8.toIntX;
13.13 + val fromInt = Word8.fromInt o dest_int;
13.14 +end;
13.15 +
13.16 structure Word32 =
13.17 struct
13.18 open Word32;
13.19 @@ -174,6 +183,15 @@
13.20 val fromInt = Word32.fromInt o dest_int;
13.21 end;
13.22
13.23 +structure LargeWord =
13.24 +struct
13.25 + open LargeWord;
13.26 + val wordSize = mk_int LargeWord.wordSize;
13.27 + val toInt = mk_int o LargeWord.toInt;
13.28 + val toIntX = mk_int o LargeWord.toIntX;
13.29 + val fromInt = LargeWord.fromInt o dest_int;
13.30 +end;
13.31 +
13.32
13.33 (* Real *)
13.34
14.1 --- a/src/Pure/ML-Systems/smlnj.ML Sat Nov 27 14:09:03 2010 -0800
14.2 +++ b/src/Pure/ML-Systems/smlnj.ML Sat Nov 27 14:34:54 2010 -0800
14.3 @@ -14,7 +14,6 @@
14.4 use "ML-Systems/thread_dummy.ML";
14.5 use "ML-Systems/multithreading.ML";
14.6 use "General/timing.ML";
14.7 -use "ML-Systems/bash.ML";
14.8 use "ML-Systems/ml_name_space.ML";
14.9 use "ML-Systems/ml_pretty.ML";
14.10 structure PolyML = struct end;
14.11 @@ -170,11 +169,6 @@
14.12 val pwd = OS.FileSys.getDir;
14.13
14.14
14.15 -(* system command execution *)
14.16 -
14.17 -val bash_output = (fn (output, rc) => (output, mk_int rc)) o bash_output;
14.18 -
14.19 -
14.20 (* getenv *)
14.21
14.22 fun getenv var =
15.1 --- a/src/Pure/ROOT.ML Sat Nov 27 14:09:03 2010 -0800
15.2 +++ b/src/Pure/ROOT.ML Sat Nov 27 14:34:54 2010 -0800
15.3 @@ -72,6 +72,15 @@
15.4 if Multithreading.available then ()
15.5 else use "Concurrent/synchronized_sequential.ML";
15.6
15.7 +if Multithreading.available
15.8 +then use "Concurrent/bash.ML"
15.9 +else use "Concurrent/bash_sequential.ML";
15.10 +
15.11 +fun bash s =
15.12 + (case bash_output s of
15.13 + ("", rc) => rc
15.14 + | (out, rc) => (writeln (perhaps (try (unsuffix "\n")) out); rc));
15.15 +
15.16 use "Concurrent/mailbox.ML";
15.17 use "Concurrent/task_queue.ML";
15.18 use "Concurrent/future.ML";
15.19 @@ -233,6 +242,7 @@
15.20 use "Isar/toplevel.ML";
15.21
15.22 (*theory documents*)
15.23 +use "System/isabelle_system.ML";
15.24 use "Thy/present.ML";
15.25 use "Thy/term_style.ML";
15.26 use "Thy/thy_output.ML";
16.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
16.2 +++ b/src/Pure/System/isabelle_system.ML Sat Nov 27 14:34:54 2010 -0800
16.3 @@ -0,0 +1,51 @@
16.4 +(* Title: Pure/System/isabelle_system.ML
16.5 + Author: Makarius
16.6 +
16.7 +Isabelle system support.
16.8 +*)
16.9 +
16.10 +signature ISABELLE_SYSTEM =
16.11 +sig
16.12 + val isabelle_tool: string -> string -> int
16.13 + val rm_tree: Path.T -> unit
16.14 + val mkdirs: Path.T -> unit
16.15 + val mkdir: Path.T -> unit
16.16 + val copy_dir: Path.T -> Path.T -> unit
16.17 +end;
16.18 +
16.19 +structure Isabelle_System: ISABELLE_SYSTEM =
16.20 +struct
16.21 +
16.22 +(* system commands *)
16.23 +
16.24 +fun isabelle_tool name args =
16.25 + (case space_explode ":" (getenv "ISABELLE_TOOLS") |> get_first (fn dir =>
16.26 + let val path = dir ^ "/" ^ name in
16.27 + if can OS.FileSys.modTime path andalso
16.28 + not (OS.FileSys.isDir path) andalso
16.29 + OS.FileSys.access (path, [OS.FileSys.A_READ, OS.FileSys.A_EXEC])
16.30 + then SOME path
16.31 + else NONE
16.32 + end handle OS.SysErr _ => NONE) of
16.33 + SOME path => bash (File.shell_quote path ^ " " ^ args)
16.34 + | NONE => (writeln ("Unknown Isabelle tool: " ^ name); 2));
16.35 +
16.36 +fun system_command cmd =
16.37 + if bash cmd <> 0 then error ("System command failed: " ^ cmd)
16.38 + else ();
16.39 +
16.40 +
16.41 +(* directory operations *)
16.42 +
16.43 +fun rm_tree path = system_command ("rm -r " ^ File.shell_path path);
16.44 +
16.45 +fun mkdirs path = system_command ("mkdir -p " ^ File.shell_path path);
16.46 +
16.47 +val mkdir = OS.FileSys.mkDir o File.platform_path;
16.48 +
16.49 +fun copy_dir src dst =
16.50 + if File.eq (src, dst) then ()
16.51 + else (system_command ("cp -r -f " ^ File.shell_path src ^ "/. " ^ File.shell_path dst); ());
16.52 +
16.53 +end;
16.54 +
17.1 --- a/src/Pure/Thy/present.ML Sat Nov 27 14:09:03 2010 -0800
17.2 +++ b/src/Pure/Thy/present.ML Sat Nov 27 14:34:54 2010 -0800
17.3 @@ -94,7 +94,7 @@
17.4 val _ = writeln "Displaying graph ...";
17.5 val path = File.tmp_path (Path.explode "tmp.graph");
17.6 val _ = write_graph gr path;
17.7 - val _ = File.isabelle_tool "browser" ("-c " ^ File.shell_path path ^ " &");
17.8 + val _ = Isabelle_System.isabelle_tool "browser" ("-c " ^ File.shell_path path ^ " &");
17.9 in () end;
17.10
17.11
17.12 @@ -344,7 +344,7 @@
17.13 val args = "-o " ^ File.shell_path pdf_path ^ " " ^ File.shell_path gr_path;
17.14 in
17.15 write_graph graph gr_path;
17.16 - if File.isabelle_tool "browser" args <> 0 orelse
17.17 + if Isabelle_System.isabelle_tool "browser" args <> 0 orelse
17.18 not (File.exists eps_path) orelse not (File.exists pdf_path)
17.19 then error "Failed to prepare dependency graph"
17.20 else
17.21 @@ -384,9 +384,9 @@
17.22 else NONE;
17.23
17.24 fun prepare_sources cp path =
17.25 - (File.mkdir path;
17.26 - if cp then File.copy_dir document_path path else ();
17.27 - File.isabelle_tool "latex"
17.28 + (Isabelle_System.mkdirs path;
17.29 + if cp then Isabelle_System.copy_dir document_path path else ();
17.30 + Isabelle_System.isabelle_tool "latex"
17.31 ("-o sty " ^ File.shell_path (Path.append path (Path.basic "root.tex")));
17.32 (case opt_graphs of NONE => () | SOME (pdf, eps) =>
17.33 (File.write (Path.append path graph_pdf_path) pdf;
17.34 @@ -395,14 +395,14 @@
17.35 List.app (finish_tex path) thys);
17.36 in
17.37 if info then
17.38 - (File.mkdir (Path.append html_prefix session_path);
17.39 + (Isabelle_System.mkdirs (Path.append html_prefix session_path);
17.40 File.write_buffer (Path.append html_prefix pre_index_path) (index_buffer html_index);
17.41 File.write (Path.append html_prefix session_entries_path) "";
17.42 create_index html_prefix;
17.43 if length path > 1 then update_index parent_html_prefix name else ();
17.44 (case readme of NONE => () | SOME path => File.copy path html_prefix);
17.45 write_graph sorted_graph (Path.append html_prefix graph_path);
17.46 - File.isabelle_tool "browser" "-b";
17.47 + Isabelle_System.isabelle_tool "browser" "-b";
17.48 File.copy (Path.explode "~~/lib/browser/GraphBrowser.jar") html_prefix;
17.49 List.app (fn (a, txt) => File.write (Path.append html_prefix (Path.basic a)) txt)
17.50 (HTML.applet_pages name (Url.File index_path, name));
17.51 @@ -509,11 +509,11 @@
17.52
17.53 val doc_path = File.tmp_path document_path;
17.54 val result_path = Path.append doc_path Path.parent;
17.55 - val _ = File.mkdir doc_path;
17.56 + val _ = Isabelle_System.mkdirs doc_path;
17.57 val root_path = Path.append doc_path (Path.basic "root.tex");
17.58 val _ = File.copy (Path.explode "~~/lib/texinputs/draft.tex") root_path;
17.59 - val _ = File.isabelle_tool "latex" ("-o sty " ^ File.shell_path root_path);
17.60 - val _ = File.isabelle_tool "latex" ("-o syms " ^ File.shell_path root_path);
17.61 + val _ = Isabelle_System.isabelle_tool "latex" ("-o sty " ^ File.shell_path root_path);
17.62 + val _ = Isabelle_System.isabelle_tool "latex" ("-o syms " ^ File.shell_path root_path);
17.63
17.64 fun known name =
17.65 let val ss = split_lines (File.read (Path.append doc_path (Path.basic name)))
18.1 --- a/src/Pure/Thy/thy_info.ML Sat Nov 27 14:09:03 2010 -0800
18.2 +++ b/src/Pure/Thy/thy_info.ML Sat Nov 27 14:34:54 2010 -0800
18.3 @@ -64,8 +64,8 @@
18.4 (* thy database *)
18.5
18.6 type deps =
18.7 - {master: (Path.T * File.ident), (*master dependencies for thy file*)
18.8 - imports: string list}; (*source specification of imports (partially qualified)*)
18.9 + {master: (Path.T * Thy_Load.file_ident), (*master dependencies for thy file*)
18.10 + imports: string list}; (*source specification of imports (partially qualified)*)
18.11
18.12 fun make_deps master imports : deps = {master = master, imports = imports};
18.13
19.1 --- a/src/Pure/Thy/thy_load.ML Sat Nov 27 14:09:03 2010 -0800
19.2 +++ b/src/Pure/Thy/thy_load.ML Sat Nov 27 14:34:54 2010 -0800
19.3 @@ -17,14 +17,17 @@
19.4 signature THY_LOAD =
19.5 sig
19.6 include BASIC_THY_LOAD
19.7 + eqtype file_ident
19.8 + val pretty_file_ident: file_ident -> Pretty.T
19.9 + val file_ident: Path.T -> file_ident option
19.10 val set_master_path: Path.T -> unit
19.11 val get_master_path: unit -> Path.T
19.12 val master_directory: theory -> Path.T
19.13 - val provide: Path.T * (Path.T * File.ident) -> theory -> theory
19.14 - val check_file: Path.T list -> Path.T -> Path.T * File.ident
19.15 - val check_thy: Path.T -> string -> Path.T * File.ident
19.16 + val provide: Path.T * (Path.T * file_ident) -> theory -> theory
19.17 + val check_file: Path.T list -> Path.T -> Path.T * file_ident
19.18 + val check_thy: Path.T -> string -> Path.T * file_ident
19.19 val deps_thy: Path.T -> string ->
19.20 - {master: Path.T * File.ident, text: string, imports: string list, uses: Path.T list}
19.21 + {master: Path.T * file_ident, text: string, imports: string list, uses: Path.T list}
19.22 val loaded_files: theory -> Path.T list
19.23 val all_current: theory -> bool
19.24 val provide_file: Path.T -> theory -> theory
19.25 @@ -36,12 +39,57 @@
19.26 structure Thy_Load: THY_LOAD =
19.27 struct
19.28
19.29 +(* file identification *)
19.30 +
19.31 +local
19.32 + val file_ident_cache =
19.33 + Synchronized.var "file_ident_cache"
19.34 + (Symtab.empty: {time_stamp: string, id: string} Symtab.table);
19.35 +in
19.36 +
19.37 +fun check_cache (path, time) =
19.38 + (case Symtab.lookup (Synchronized.value file_ident_cache) path of
19.39 + NONE => NONE
19.40 + | SOME {time_stamp, id} => if time_stamp = time then SOME id else NONE);
19.41 +
19.42 +fun update_cache (path, (time, id)) =
19.43 + Synchronized.change file_ident_cache
19.44 + (Symtab.update (path, {time_stamp = time, id = id}));
19.45 +
19.46 +end;
19.47 +
19.48 +datatype file_ident = File_Ident of string;
19.49 +
19.50 +fun pretty_file_ident (File_Ident s) = Pretty.str (quote s);
19.51 +
19.52 +fun file_ident path =
19.53 + let val physical_path = perhaps (try OS.FileSys.fullPath) (File.platform_path path) in
19.54 + (case try (Time.toString o OS.FileSys.modTime) physical_path of
19.55 + NONE => NONE
19.56 + | SOME mod_time => SOME (File_Ident
19.57 + (case getenv "ISABELLE_FILE_IDENT" of
19.58 + "" => physical_path ^ ": " ^ mod_time
19.59 + | cmd =>
19.60 + (case check_cache (physical_path, mod_time) of
19.61 + SOME id => id
19.62 + | NONE =>
19.63 + let
19.64 + val (id, rc) = (*potentially slow*)
19.65 + bash_output
19.66 + ("\"$ISABELLE_HOME/lib/scripts/fileident\" " ^ File.shell_quote physical_path);
19.67 + in
19.68 + if id <> "" andalso rc = 0 then (update_cache (physical_path, (mod_time, id)); id)
19.69 + else error ("Failed to identify file " ^ quote (Path.implode path) ^ " by " ^ cmd)
19.70 + end))))
19.71 + end;
19.72 +
19.73 +
19.74 (* manage source files *)
19.75
19.76 type files =
19.77 - {master_dir: Path.T, (*master directory of theory source*)
19.78 - required: Path.T list, (*source path*)
19.79 - provided: (Path.T * (Path.T * File.ident)) list}; (*source path, physical path, identifier*)
19.80 + {master_dir: Path.T, (*master directory of theory source*)
19.81 + required: Path.T list, (*source path*)
19.82 + provided: (Path.T * (Path.T * file_ident)) list}; (*source path, physical path, identifier*)
19.83
19.84 fun make_files (master_dir, required, provided): files =
19.85 {master_dir = master_dir, required = required, provided = provided};
19.86 @@ -79,26 +127,26 @@
19.87 (* maintain default paths *)
19.88
19.89 local
19.90 - val load_path = Unsynchronized.ref [Path.current];
19.91 + val load_path = Synchronized.var "load_path" [Path.current];
19.92 val master_path = Unsynchronized.ref Path.current;
19.93 in
19.94
19.95 -fun show_path () = map Path.implode (! load_path);
19.96 +fun show_path () = map Path.implode (Synchronized.value load_path);
19.97
19.98 -fun del_path s =
19.99 - CRITICAL (fn () => Unsynchronized.change load_path (remove (op =) (Path.explode s)));
19.100 +fun del_path s = Synchronized.change load_path (remove (op =) (Path.explode s));
19.101
19.102 -fun add_path s =
19.103 - CRITICAL (fn () => (del_path s; Unsynchronized.change load_path (cons (Path.explode s))));
19.104 +fun add_path s = Synchronized.change load_path (update (op =) (Path.explode s));
19.105
19.106 fun path_add s =
19.107 - CRITICAL (fn () =>
19.108 - (del_path s; Unsynchronized.change load_path (fn path => path @ [Path.explode s])));
19.109 + Synchronized.change load_path (fn path =>
19.110 + let val p = Path.explode s
19.111 + in remove (op =) p path @ [p] end);
19.112
19.113 -fun reset_path () = CRITICAL (fn () => load_path := [Path.current]);
19.114 +fun reset_path () = Synchronized.change load_path (K [Path.current]);
19.115
19.116 fun search_path dir path =
19.117 - distinct (op =) (dir :: (if Path.is_basic path then (! load_path) else [Path.current]));
19.118 + distinct (op =)
19.119 + (dir :: (if Path.is_basic path then (Synchronized.value load_path) else [Path.current]));
19.120
19.121 fun set_master_path path = master_path := path;
19.122 fun get_master_path () = ! master_path;
19.123 @@ -115,7 +163,7 @@
19.124 in
19.125 dirs |> get_first (fn dir =>
19.126 let val full_path = File.full_path (Path.append dir path) in
19.127 - (case File.ident full_path of
19.128 + (case file_ident full_path of
19.129 NONE => NONE
19.130 | SOME id => SOME (full_path, id))
19.131 end)
20.1 --- a/src/Pure/pure_setup.ML Sat Nov 27 14:09:03 2010 -0800
20.2 +++ b/src/Pure/pure_setup.ML Sat Nov 27 14:34:54 2010 -0800
20.3 @@ -36,7 +36,7 @@
20.4 toplevel_pp ["Context", "Proof", "context"] "Proof_Display.pp_context";
20.5 toplevel_pp ["Syntax", "ast"] "Syntax.pretty_ast";
20.6 toplevel_pp ["Path", "T"] "Pretty.str o quote o Path.implode";
20.7 -toplevel_pp ["File", "ident"] "Pretty.str o quote o File.rep_ident";
20.8 +toplevel_pp ["Thy_Load", "file_ident"] "Thy_Load.pretty_file_ident";
20.9 toplevel_pp ["Proof", "state"] "(fn _: Proof.state => Pretty.str \"<Proof.state>\")";
20.10 toplevel_pp ["Toplevel", "state"] "Toplevel.pretty_abstract";
20.11
21.1 --- a/src/Tools/Code/code_haskell.ML Sat Nov 27 14:09:03 2010 -0800
21.2 +++ b/src/Tools/Code/code_haskell.ML Sat Nov 27 14:34:54 2010 -0800
21.3 @@ -353,7 +353,7 @@
21.4 val _ = File.check destination;
21.5 val filepath = (Path.append destination o Path.ext "hs" o Path.explode o implode
21.6 o separate "/" o Long_Name.explode) module_name;
21.7 - val _ = File.mkdir_leaf (Path.dir filepath);
21.8 + val _ = Isabelle_System.mkdir (Path.dir filepath);
21.9 in
21.10 (File.write filepath o format [] width o Pretty.chunks2)
21.11 [str "{-# OPTIONS_GHC -fglasgow-exts #-}", content]
22.1 --- a/src/Tools/cache_io.ML Sat Nov 27 14:09:03 2010 -0800
22.2 +++ b/src/Tools/cache_io.ML Sat Nov 27 14:34:54 2010 -0800
22.3 @@ -44,9 +44,9 @@
22.4 fun with_tmp_dir name f =
22.5 let
22.6 val path = File.tmp_path (Path.explode (name ^ serial_string ()))
22.7 - val _ = File.mkdir path
22.8 + val _ = Isabelle_System.mkdirs path
22.9 val x = Exn.capture f path
22.10 - val _ = try File.rm_tree path
22.11 + val _ = try Isabelle_System.rm_tree path
22.12 in Exn.release x end
22.13
22.14 type result = {