--- a/src/HOL/Tools/Nitpick/kodkod.ML Sat Nov 27 14:09:03 2010 -0800
+++ b/src/HOL/Tools/Nitpick/kodkod.ML Sat Nov 27 14:34:54 2010 -0800
@@ -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
--- a/src/HOL/ex/Eval_Examples.thy Sat Nov 27 14:09:03 2010 -0800
+++ b/src/HOL/ex/Eval_Examples.thy Sat Nov 27 14:34:54 2010 -0800
@@ -9,26 +9,26 @@
text {* evaluation oracle *}
lemma "True \<or> False" by eval
-lemma "\<not> (Suc 0 = Suc 1)" by eval
-lemma "[] = ([]\<Colon> int list)" by eval
+lemma "Suc 0 \<noteq> Suc 1" by eval
+lemma "[] = ([] :: int list)" by eval
lemma "[()] = [()]" by eval
-lemma "fst ([]::nat list, Suc 0) = []" by eval
+lemma "fst ([] :: nat list, Suc 0) = []" by eval
text {* SML evaluation oracle *}
lemma "True \<or> False" by evaluation
-lemma "\<not> (Suc 0 = Suc 1)" by evaluation
-lemma "[] = ([]\<Colon> int list)" by evaluation
+lemma "Suc 0 \<noteq> Suc 1" by evaluation
+lemma "[] = ([] :: int list)" by evaluation
lemma "[()] = [()]" by evaluation
-lemma "fst ([]::nat list, Suc 0) = []" by evaluation
+lemma "fst ([] :: nat list, Suc 0) = []" by evaluation
text {* normalization *}
lemma "True \<or> False" by normalization
-lemma "\<not> (Suc 0 = Suc 1)" by normalization
-lemma "[] = ([]\<Colon> int list)" by normalization
+lemma "Suc 0 \<noteq> Suc 1" by normalization
+lemma "[] = ([] :: int list)" by normalization
lemma "[()] = [()]" by normalization
-lemma "fst ([]::nat list, Suc 0) = []" by normalization
+lemma "fst ([] :: nat list, Suc 0) = []" by normalization
text {* term evaluation *}
@@ -47,10 +47,10 @@
value [SML] "nat 100"
value [nbe] "nat 100"
-value "(10\<Colon>int) \<le> 12"
-value [code] "(10\<Colon>int) \<le> 12"
-value [SML] "(10\<Colon>int) \<le> 12"
-value [nbe] "(10\<Colon>int) \<le> 12"
+value "(10::int) \<le> 12"
+value [code] "(10::int) \<le> 12"
+value [SML] "(10::int) \<le> 12"
+value [nbe] "(10::int) \<le> 12"
value "max (2::int) 4"
value [code] "max (2::int) 4"
@@ -62,29 +62,29 @@
value [SML] "of_int 2 / of_int 4 * (1::rat)"
value [nbe] "of_int 2 / of_int 4 * (1::rat)"
-value "[]::nat list"
-value [code] "[]::nat list"
-value [SML] "[]::nat list"
-value [nbe] "[]::nat list"
+value "[] :: nat list"
+value [code] "[] :: nat list"
+value [SML] "[] :: nat list"
+value [nbe] "[] :: nat list"
value "[(nat 100, ())]"
value [code] "[(nat 100, ())]"
value [SML] "[(nat 100, ())]"
value [nbe] "[(nat 100, ())]"
-
text {* a fancy datatype *}
-datatype ('a, 'b) bair =
- Bair "'a\<Colon>order" 'b
- | Shift "('a, 'b) cair"
- | Dummy unit
-and ('a, 'b) cair =
- Cair 'a 'b
+datatype ('a, 'b) foo =
+ Foo "'a\<Colon>order" 'b
+ | Bla "('a, 'b) bar"
+ | Dummy nat
+and ('a, 'b) bar =
+ Bar 'a 'b
+ | Blubb "('a, 'b) foo"
-value "Shift (Cair (4::nat) [Suc 0])"
-value [code] "Shift (Cair (4::nat) [Suc 0])"
-value [SML] "Shift (Cair (4::nat) [Suc 0])"
-value [nbe] "Shift (Cair (4::nat) [Suc 0])"
+value "Bla (Bar (4::nat) [Suc 0])"
+value [code] "Bla (Bar (4::nat) [Suc 0])"
+value [SML] "Bla (Bar (4::nat) [Suc 0])"
+value [nbe] "Bla (Bar (4::nat) [Suc 0])"
end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Concurrent/bash.ML Sat Nov 27 14:34:54 2010 -0800
@@ -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 14:34:54 2010 -0800
@@ -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 14:09:03 2010 -0800
+++ b/src/Pure/General/file.ML Sat Nov 27 14:34:54 2010 -0800
@@ -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 14:09:03 2010 -0800
+++ b/src/Pure/General/secure.ML Sat Nov 27 14:34:54 2010 -0800
@@ -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 14:09:03 2010 -0800
+++ b/src/Pure/IsaMakefile Sat Nov 27 14:34:54 2010 -0800
@@ -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/code.ML Sat Nov 27 14:09:03 2010 -0800
+++ b/src/Pure/Isar/code.ML Sat Nov 27 14:34:54 2010 -0800
@@ -316,7 +316,7 @@
val data = case Datatab.lookup datatab kind
of SOME data => data
| NONE => invoke_init kind;
- val result as (x, data') = f (dest data);
+ val result as (_, data') = f (dest data);
val _ = Synchronized.change dataref
((K o SOME) (Datatab.update (kind, mk data') datatab, thy_ref));
in result end;
@@ -358,11 +358,13 @@
of SOME ty => ty
| NONE => (Type.strip_sorts o Sign.the_const_type thy) c;
+fun args_number thy = length o fst o strip_type o const_typ thy;
+
fun subst_signature thy c ty =
let
- fun mk_subst (Type (tyco, tys1)) (ty2 as Type (tyco2, tys2)) =
+ fun mk_subst (Type (_, tys1)) (Type (_, tys2)) =
fold2 mk_subst tys1 tys2
- | mk_subst ty (TVar (v, sort)) = Vartab.update (v, ([], ty))
+ | mk_subst ty (TVar (v, _)) = Vartab.update (v, ([], ty))
in case lookup_typ thy c
of SOME ty' => Envir.subst_type (mk_subst ty (expand_signature thy ty') Vartab.empty) ty'
| NONE => ty
@@ -370,7 +372,10 @@
fun subst_signatures thy = map_aterms (fn Const (c, ty) => Const (c, subst_signature thy c ty) | t => t);
-fun args_number thy = length o fst o strip_type o const_typ thy;
+fun logical_typscheme thy (c, ty) =
+ (map dest_TFree (Sign.const_typargs thy (c, ty)), Type.strip_sorts ty);
+
+fun typscheme thy (c, ty) = logical_typscheme thy (c, subst_signature thy c ty);
(* datatypes *)
@@ -407,13 +412,14 @@
val _ = if (tyco' : string) <> tyco
then error "Different type constructors in constructor set"
else ();
- val sorts'' = map2 (curry (Sorts.inter_sort (Sign.classes_of thy))) sorts' sorts
- in ((tyco, sorts), c :: cs) end;
+ val sorts'' =
+ map2 (curry (Sorts.inter_sort (Sign.classes_of thy))) sorts' sorts
+ in ((tyco, sorts''), c :: cs) end;
fun inst vs' (c, (vs, ty)) =
let
val the_v = the o AList.lookup (op =) (vs ~~ vs');
val ty' = map_atyps (fn TFree (v, _) => TFree (the_v v)) ty;
- val vs'' = map dest_TFree (Sign.const_typargs thy (c, ty'));
+ val (vs'', _) = logical_typscheme thy (c, ty');
in (c, (vs'', (fst o strip_type) ty')) end;
val c' :: cs' = map (ty_sorts thy) cs;
val ((tyco, sorts), cs'') = fold add cs' (apsnd single c');
@@ -439,7 +445,7 @@
fun get_type_of_constr_or_abstr thy c =
case (snd o strip_type o const_typ thy) c
- of Type (tyco, _) => let val ((vs, cos), abstract) = get_type thy tyco
+ of Type (tyco, _) => let val ((_, cos), abstract) = get_type thy tyco
in if member (op =) (map fst cos) c then SOME (tyco, abstract) else NONE end
| _ => NONE;
@@ -592,11 +598,6 @@
fun const_abs_eqn thy = AxClass.unoverload_const thy o dest_Const o fst o strip_comb o snd
o dest_comb o fst o Logic.dest_equals o Thm.plain_prop_of;
-fun logical_typscheme thy (c, ty) =
- (map dest_TFree (Sign.const_typargs thy (c, ty)), Type.strip_sorts ty);
-
-fun typscheme thy (c, ty) = logical_typscheme thy (c, subst_signature thy c ty);
-
fun mk_proj tyco vs ty abs rep =
let
val ty_abs = Type (tyco, map TFree vs);
@@ -641,19 +642,19 @@
else SOME (((v, i), x), mk ((v', 0), x))) (vs ~~ names)
end;
-fun desymbolize_tvars thy thms =
+fun desymbolize_tvars thms =
let
val tvs = fold (Term.add_tvars o Thm.prop_of) thms [];
val tvar_subst = mk_desymbolization (unprefix "'") (prefix "'") TVar tvs;
in map (Thm.certify_instantiate (tvar_subst, [])) thms end;
-fun desymbolize_vars thy thm =
+fun desymbolize_vars thm =
let
val vs = Term.add_vars (Thm.prop_of thm) [];
val var_subst = mk_desymbolization I I Var vs;
in Thm.certify_instantiate ([], var_subst) thm end;
-fun canonize_thms thy = desymbolize_tvars thy #> same_arity thy #> map (desymbolize_vars thy);
+fun canonize_thms thy = desymbolize_tvars #> same_arity thy #> map desymbolize_vars;
(* abstype certificates *)
@@ -672,13 +673,12 @@
then error ("Is a class parameter: " ^ string_of_const thy c) else ()) (abs, rep);
val _ = check_decl_ty thy (abs, raw_ty);
val _ = check_decl_ty thy (rep, rep_ty);
- val var = (fst o dest_Var) param
+ val _ = (fst o dest_Var) param
handle TERM _ => bad "Not an abstype certificate";
val _ = if param = rhs then () else bad "Not an abstype certificate";
val ((tyco, sorts), (abs, (vs, ty'))) = ty_sorts thy (abs, Logic.unvarifyT_global raw_ty);
val ty = domain_type ty';
- val vs' = map dest_TFree (Sign.const_typargs thy (abs, ty'));
- val ty_abs = range_type ty';
+ val (vs', _) = logical_typscheme thy (abs, ty');
in (tyco, (vs ~~ sorts, ((abs, (vs', ty)), (rep, thm)))) end;
@@ -716,7 +716,7 @@
fun concretify_abs thy tyco abs_thm =
let
- val (vs, ((c, _), (_, cert))) = get_abstype_spec thy tyco;
+ val (_, ((c, _), (_, cert))) = get_abstype_spec thy tyco;
val lhs = (fst o Logic.dest_equals o Thm.prop_of) abs_thm
val ty = fastype_of lhs;
val ty_abs = (fastype_of o snd o dest_comb) lhs;
@@ -742,13 +742,16 @@
fun empty_cert thy c =
let
- val raw_ty = const_typ thy c;
- val tvars = Term.add_tvar_namesT raw_ty [];
- val tvars' = case AxClass.class_of_param thy c
- of SOME class => [TFree (Name.aT, [class])]
- | NONE => Name.invent_list [] Name.aT (length tvars)
- |> map (fn v => TFree (v, []));
- val ty = typ_subst_TVars (tvars ~~ tvars') raw_ty;
+ val raw_ty = Logic.unvarifyT_global (const_typ thy c);
+ val (vs, _) = logical_typscheme thy (c, raw_ty);
+ val sortargs = case AxClass.class_of_param thy c
+ of SOME class => [[class]]
+ | NONE => (case get_type_of_constr_or_abstr thy c
+ of SOME (tyco, _) => (map snd o fst o the)
+ (AList.lookup (op =) ((snd o fst o get_type thy) tyco) c)
+ | NONE => replicate (length vs) []);
+ val the_sort = the o AList.lookup (op =) (map fst vs ~~ sortargs);
+ val ty = map_type_tfree (fn (v, _) => TFree (v, the_sort v)) raw_ty
val chead = build_head thy (c, ty);
in Equations (Thm.weaken chead Drule.dummy_thm, []) end;
@@ -767,19 +770,19 @@
fold (curry (Sorts.inter_sort (Sign.classes_of thy)) o snd) vs [];
val sorts = map_transpose inter_sorts vss;
val vts = Name.names Name.context Name.aT sorts;
- val thms as thm :: _ =
+ val thms' =
map2 (fn vs => Thm.certify_instantiate (vs ~~ map TFree vts, [])) vss thms;
- val head_thm = Thm.symmetric (Thm.assume (build_head thy (head_eqn (hd thms))));
+ val head_thm = Thm.symmetric (Thm.assume (build_head thy (head_eqn (hd thms'))));
fun head_conv ct = if can Thm.dest_comb ct
then Conv.fun_conv head_conv ct
else Conv.rewr_conv head_thm ct;
val rewrite_head = Conv.fconv_rule (Conv.arg1_conv head_conv);
- val cert_thm = Conjunction.intr_balanced (map rewrite_head thms);
+ val cert_thm = Conjunction.intr_balanced (map rewrite_head thms');
in Equations (cert_thm, propers) end;
fun cert_of_proj thy c tyco =
let
- val (vs, ((abs, (_, ty)), (rep, cert))) = get_abstype_spec thy tyco;
+ val (vs, ((abs, (_, ty)), (rep, _))) = get_abstype_spec thy tyco;
val _ = if c = rep then () else
error ("Wrong head of projection,\nexpected constant " ^ string_of_const thy rep);
in Projection (mk_proj tyco vs ty abs rep, tyco) end;
@@ -824,7 +827,7 @@
Thm.prop_of cert_thm
|> Logic.dest_conjunction_balanced (length propers);
in (vs, fold (add_rhss_of_eqn thy) equations []) end
- | typargs_deps_of_cert thy (Projection (t, tyco)) =
+ | typargs_deps_of_cert thy (Projection (t, _)) =
(fst (typscheme_projection thy t), add_rhss_of_eqn thy t [])
| typargs_deps_of_cert thy (Abstract (abs_thm, tyco)) =
let
@@ -864,7 +867,7 @@
o snd o equations_of_cert thy) cert
| pretty_cert thy (Projection (t, _)) =
[Syntax.pretty_term_global thy (map_types Logic.varifyT_global t)]
- | pretty_cert thy (Abstract (abs_thm, tyco)) =
+ | pretty_cert thy (Abstract (abs_thm, _)) =
[(Display.pretty_thm_global thy o AxClass.overload thy o Thm.varifyT_global) abs_thm];
fun bare_thms_of_cert thy (cert as Equations _) =
@@ -1118,7 +1121,7 @@
fun del_eqn thm thy = case mk_eqn_liberal thy thm
of SOME (thm, _) => let
- fun del_eqn' (Default eqns) = empty_fun_spec
+ fun del_eqn' (Default _) = empty_fun_spec
| del_eqn' (Eqns eqns) =
Eqns (filter_out (fn (thm', _) => Thm.eq_thm_prop (thm, thm')) eqns)
| del_eqn' spec = spec
@@ -1130,7 +1133,7 @@
(* cases *)
-fun case_cong thy case_const (num_args, (pos, constrs)) =
+fun case_cong thy case_const (num_args, (pos, _)) =
let
val ([x, y], ctxt) = Name.variants ["A", "A'"] Name.context;
val (zs, _) = Name.variants (replicate (num_args - 1) "") ctxt;
--- a/src/Pure/Isar/isar_cmd.ML Sat Nov 27 14:09:03 2010 -0800
+++ b/src/Pure/Isar/isar_cmd.ML Sat Nov 27 14:34:54 2010 -0800
@@ -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 14:09:03 2010 -0800
+++ /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 14:09:03 2010 -0800
+++ b/src/Pure/ML-Systems/multithreading_polyml.ML Sat Nov 27 14:34:54 2010 -0800
@@ -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 14:09:03 2010 -0800
+++ b/src/Pure/ML-Systems/polyml_common.ML Sat Nov 27 14:34:54 2010 -0800
@@ -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 14:09:03 2010 -0800
+++ b/src/Pure/ML-Systems/proper_int.ML Sat Nov 27 14:34:54 2010 -0800
@@ -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 14:09:03 2010 -0800
+++ b/src/Pure/ML-Systems/smlnj.ML Sat Nov 27 14:34:54 2010 -0800
@@ -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 14:09:03 2010 -0800
+++ b/src/Pure/ROOT.ML Sat Nov 27 14:34:54 2010 -0800
@@ -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 14:34:54 2010 -0800
@@ -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 14:09:03 2010 -0800
+++ b/src/Pure/Thy/present.ML Sat Nov 27 14:34:54 2010 -0800
@@ -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 14:09:03 2010 -0800
+++ b/src/Pure/Thy/thy_info.ML Sat Nov 27 14:34:54 2010 -0800
@@ -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 14:09:03 2010 -0800
+++ b/src/Pure/Thy/thy_load.ML Sat Nov 27 14:34:54 2010 -0800
@@ -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 14:09:03 2010 -0800
+++ b/src/Pure/pure_setup.ML Sat Nov 27 14:34:54 2010 -0800
@@ -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 14:09:03 2010 -0800
+++ b/src/Tools/Code/code_haskell.ML Sat Nov 27 14:34:54 2010 -0800
@@ -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 14:09:03 2010 -0800
+++ b/src/Tools/cache_io.ML Sat Nov 27 14:34:54 2010 -0800
@@ -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 = {