--- a/src/Pure/Isar/toplevel.ML Thu Jul 22 10:41:12 2010 +0200
+++ b/src/Pure/Isar/toplevel.ML Thu Jul 22 14:01:43 2010 +0200
@@ -578,7 +578,9 @@
(* post-transition hooks *)
-local val hooks = Unsynchronized.ref ([]: (transition -> state -> state -> unit) list) in
+local
+ val hooks = Unsynchronized.ref ([]: (transition -> state -> state -> unit) list);
+in
fun add_hook f = CRITICAL (fn () => Unsynchronized.change hooks (cons f));
fun get_hooks () = ! hooks;
@@ -597,9 +599,10 @@
fun do_profiling f x = profile (! profiling) f x;
val (result, status) =
- state |> (apply_trans int trans
- |> (if ! profiling > 0 andalso not no_timing then do_profiling else I)
- |> (if ! profiling > 0 orelse ! timing andalso not no_timing then do_timing else I));
+ state |>
+ (apply_trans int trans
+ |> (! profiling > 0 andalso not no_timing) ? do_profiling
+ |> (! profiling > 0 orelse ! timing andalso not no_timing) ? do_timing);
val _ = if int andalso not (! quiet) andalso print then print_state false result else ();
in (result, Option.map (fn UNDEF => type_error tr state | exn => exn) status) end);
--- a/src/Pure/Thy/thy_info.ML Thu Jul 22 10:41:12 2010 +0200
+++ b/src/Pure/Thy/thy_info.ML Thu Jul 22 14:01:43 2010 +0200
@@ -105,10 +105,8 @@
fun base_name s = Path.implode (Path.base (Path.explode s));
-type thy = deps option * theory option;
-
local
- val database = Unsynchronized.ref (Graph.empty: thy Graph.T);
+ val database = Unsynchronized.ref (Graph.empty: (deps option * theory option) Graph.T);
in
fun get_thys () = ! database;
fun change_thys f = CRITICAL (fn () => Unsynchronized.change database f);
@@ -421,9 +419,11 @@
fun check_ml master (src_path, info) =
let val info' =
- (case info of NONE => NONE
+ (case info of
+ NONE => NONE
| SOME (_, id) =>
- (case Thy_Load.check_ml (master_dir master) src_path of NONE => NONE
+ (case Thy_Load.check_ml (master_dir master) src_path of
+ NONE => NONE
| SOME (path', id') => if id <> id' then NONE else SOME (path', id')))
in (src_path, info') end;