--- a/lib/Tools/mkdir Fri Jul 31 23:31:11 2009 +0200
+++ b/lib/Tools/mkdir Sat Aug 01 00:39:51 2009 +0200
@@ -187,8 +187,8 @@
[ -z "$QUIET" ] && echo "creating $PREFIX/ROOT.ML" >&2
cat >ROOT.ML <<EOF
(*
- no_document use_thy "ThisTheory";
- use_thy "ThatTheory";
+ no_document use_thys ["This_Theory1", "This_Theory2"];
+ use_thys ["That_Theory1", "That_Theory2", "That_Theory3"];
*)
EOF
fi
--- a/src/Pure/Concurrent/future.ML Fri Jul 31 23:31:11 2009 +0200
+++ b/src/Pure/Concurrent/future.ML Sat Aug 01 00:39:51 2009 +0200
@@ -120,11 +120,10 @@
fun SYNCHRONIZED name = SimpleThread.synchronized name lock;
fun wait cond = (*requires SYNCHRONIZED*)
- Multithreading.sync_wait NONE cond lock;
+ Multithreading.sync_wait NONE NONE cond lock;
-fun wait_interruptible timeout cond = (*requires SYNCHRONIZED*)
- interruptible (fn () =>
- ignore (Multithreading.sync_wait (SOME (Time.+ (Time.now (), timeout))) cond lock)) ();
+fun wait_timeout timeout cond = (*requires SYNCHRONIZED*)
+ Multithreading.sync_wait NONE (SOME (Time.+ (Time.now (), timeout))) cond lock;
fun signal cond = (*requires SYNCHRONIZED*)
ConditionVar.signal cond;
@@ -149,11 +148,11 @@
val res =
if ok then
Exn.capture (fn () =>
- (Thread.testInterrupt ();
- Multithreading.with_attributes Multithreading.restricted_interrupts
- (fn _ => fn () => e ())) ()) ()
+ Multithreading.with_attributes Multithreading.private_interrupts (fn _ => e ())) ()
else Exn.Exn Exn.Interrupt;
- val _ = Synchronized.change result (K (SOME res));
+ val _ = Synchronized.change result
+ (fn NONE => SOME res
+ | SOME _ => raise Fail "Duplicate assignment of future value");
in
(case res of
Exn.Exn exn => (Task_Queue.cancel_group group exn; false)
@@ -276,20 +275,23 @@
broadcast_work ());
(*delay loop*)
- val _ = wait_interruptible next_round scheduler_event
- handle Exn.Interrupt =>
- (Multithreading.tracing 1 (fn () => "Interrupt");
- List.app do_cancel (Task_Queue.cancel_all (! queue)));
+ val _ = Exn.release (wait_timeout next_round scheduler_event);
(*shutdown*)
val _ = if Task_Queue.is_empty (! queue) then do_shutdown := true else ();
val continue = not (! do_shutdown andalso null (! workers));
val _ = if continue then () else scheduler := NONE;
val _ = broadcast scheduler_event;
- in continue end;
+ in continue end
+ handle Exn.Interrupt =>
+ (Multithreading.tracing 1 (fn () => "Interrupt");
+ uninterruptible (fn _ => fn () => List.app do_cancel (Task_Queue.cancel_all (! queue))) ();
+ scheduler_next ());
fun scheduler_loop () =
- while SYNCHRONIZED "scheduler" (fn () => scheduler_next ()) do ();
+ Multithreading.with_attributes
+ (Multithreading.sync_interrupts Multithreading.public_interrupts)
+ (fn _ => while SYNCHRONIZED "scheduler" (fn () => scheduler_next ()) do ());
fun scheduler_active () = (*requires SYNCHRONIZED*)
(case ! scheduler of NONE => false | SOME thread => Thread.isActive thread);
@@ -393,12 +395,11 @@
fun interruptible_task f x =
if Multithreading.available then
- (Thread.testInterrupt ();
Multithreading.with_attributes
(if is_worker ()
- then Multithreading.restricted_interrupts
- else Multithreading.regular_interrupts)
- (fn _ => fn x => f x) x)
+ then Multithreading.private_interrupts
+ else Multithreading.public_interrupts)
+ (fn _ => f x)
else interruptible f x;
(*cancel: present and future group members will be interrupted eventually*)
--- a/src/Pure/Concurrent/simple_thread.ML Fri Jul 31 23:31:11 2009 +0200
+++ b/src/Pure/Concurrent/simple_thread.ML Sat Aug 01 00:39:51 2009 +0200
@@ -16,7 +16,7 @@
fun fork interrupts body =
Thread.fork (fn () => exception_trace (fn () => body ()),
- if interrupts then Multithreading.regular_interrupts else Multithreading.no_interrupts);
+ if interrupts then Multithreading.public_interrupts else Multithreading.no_interrupts);
fun interrupt thread = Thread.interrupt thread handle Thread _ => ();
--- a/src/Pure/Concurrent/synchronized.ML Fri Jul 31 23:31:11 2009 +0200
+++ b/src/Pure/Concurrent/synchronized.ML Sat Aug 01 00:39:51 2009 +0200
@@ -48,9 +48,10 @@
(case f x of
SOME (y, x') => (var := x'; SOME y)
| NONE =>
- if Multithreading.sync_wait (time_limit x) cond lock
- then try_change ()
- else NONE)
+ (case Multithreading.sync_wait NONE (time_limit x) cond lock of
+ Exn.Result true => try_change ()
+ | Exn.Result false => NONE
+ | Exn.Exn exn => reraise exn))
end;
val res = try_change ();
val _ = ConditionVar.broadcast cond;
--- a/src/Pure/ML-Systems/multithreading.ML Fri Jul 31 23:31:11 2009 +0200
+++ b/src/Pure/ML-Systems/multithreading.ML Sat Aug 01 00:39:51 2009 +0200
@@ -13,20 +13,21 @@
signature MULTITHREADING =
sig
include BASIC_MULTITHREADING
- val trace: int ref
- val tracing: int -> (unit -> string) -> unit
- val tracing_time: bool -> Time.time -> (unit -> string) -> unit
- val real_time: ('a -> unit) -> 'a -> Time.time
val available: bool
val max_threads: int ref
val max_threads_value: unit -> int
val enabled: unit -> bool
val no_interrupts: Thread.threadAttribute list
- val regular_interrupts: Thread.threadAttribute list
- val restricted_interrupts: Thread.threadAttribute list
- val with_attributes: Thread.threadAttribute list ->
- (Thread.threadAttribute list -> 'a -> 'b) -> 'a -> 'b
- val sync_wait: Time.time option -> ConditionVar.conditionVar -> Mutex.mutex -> bool
+ val public_interrupts: Thread.threadAttribute list
+ val private_interrupts: Thread.threadAttribute list
+ val sync_interrupts: Thread.threadAttribute list -> Thread.threadAttribute list
+ val with_attributes: Thread.threadAttribute list -> (Thread.threadAttribute list -> 'a) -> 'a
+ val sync_wait: Thread.threadAttribute list option -> Time.time option ->
+ ConditionVar.conditionVar -> Mutex.mutex -> bool Exn.result
+ val trace: int ref
+ val tracing: int -> (unit -> string) -> unit
+ val tracing_time: bool -> Time.time -> (unit -> string) -> unit
+ val real_time: ('a -> unit) -> 'a -> Time.time
val self_critical: unit -> bool
val serial: unit -> int
end;
@@ -34,14 +35,6 @@
structure Multithreading: MULTITHREADING =
struct
-(* tracing *)
-
-val trace = ref (0: int);
-fun tracing _ _ = ();
-fun tracing_time _ _ _ = ();
-fun real_time f x = (f x; Time.zeroTime);
-
-
(* options *)
val available = false;
@@ -52,18 +45,22 @@
(* attributes *)
-val no_interrupts =
- [Thread.EnableBroadcastInterrupt false, Thread.InterruptState Thread.InterruptDefer];
+val no_interrupts = [];
+val public_interrupts = [];
+val private_interrupts = [];
+fun sync_interrupts _ = [];
-val regular_interrupts =
- [Thread.EnableBroadcastInterrupt true, Thread.InterruptState Thread.InterruptAsynchOnce];
+fun with_attributes _ e = e [];
-val restricted_interrupts =
- [Thread.EnableBroadcastInterrupt false, Thread.InterruptState Thread.InterruptAsynchOnce];
+fun sync_wait _ _ _ _ = Exn.Result true;
+
+
+(* tracing *)
-fun with_attributes _ f x = f [] x;
-
-fun sync_wait _ _ _ = false;
+val trace = ref (0: int);
+fun tracing _ _ = ();
+fun tracing_time _ _ _ = ();
+fun real_time f x = (f x; Time.zeroTime);
(* critical section *)
--- a/src/Pure/ML-Systems/multithreading_polyml.ML Fri Jul 31 23:31:11 2009 +0200
+++ b/src/Pure/ML-Systems/multithreading_polyml.ML Sat Aug 01 00:39:51 2009 +0200
@@ -27,31 +27,6 @@
structure Multithreading: MULTITHREADING =
struct
-(* tracing *)
-
-val trace = ref 0;
-
-fun tracing level msg =
- if level > ! trace then ()
- else (TextIO.output (TextIO.stdErr, (">>> " ^ msg () ^ "\n")); TextIO.flushOut TextIO.stdErr)
- handle _ (*sic*) => ();
-
-fun tracing_time detailed time =
- tracing
- (if not detailed then 5
- else if Time.>= (time, Time.fromMilliseconds 1000) then 1
- else if Time.>= (time, Time.fromMilliseconds 100) then 2
- else if Time.>= (time, Time.fromMilliseconds 10) then 3
- else if Time.>= (time, Time.fromMilliseconds 1) then 4 else 5);
-
-fun real_time f x =
- let
- val timer = Timer.startRealTimer ();
- val () = f x;
- val time = Timer.checkRealTimer timer;
- in time end;
-
-
(* options *)
val available = true;
@@ -91,57 +66,76 @@
val no_interrupts =
[Thread.EnableBroadcastInterrupt false, Thread.InterruptState Thread.InterruptDefer];
-val regular_interrupts =
+val public_interrupts =
[Thread.EnableBroadcastInterrupt true, Thread.InterruptState Thread.InterruptAsynchOnce];
-val restricted_interrupts =
+val private_interrupts =
[Thread.EnableBroadcastInterrupt false, Thread.InterruptState Thread.InterruptAsynchOnce];
+val sync_interrupts = map
+ (fn x as Thread.InterruptState Thread.InterruptDefer => x
+ | Thread.InterruptState _ => Thread.InterruptState Thread.InterruptSynch
+ | x => x);
+
val safe_interrupts = map
(fn Thread.InterruptState Thread.InterruptAsynch =>
Thread.InterruptState Thread.InterruptAsynchOnce
| x => x);
-fun with_attributes new_atts f x =
+fun with_attributes new_atts e =
let
val orig_atts = safe_interrupts (Thread.getAttributes ());
val result = Exn.capture (fn () =>
- (Thread.setAttributes (safe_interrupts new_atts); f orig_atts x)) ();
+ (Thread.setAttributes (safe_interrupts new_atts); e orig_atts)) ();
val _ = Thread.setAttributes orig_atts;
in Exn.release result end;
-(* regular interruptibility *)
+(* portable wrappers *)
+
+fun interruptible f x = with_attributes public_interrupts (fn _ => f x);
-fun interruptible f x =
- (Thread.testInterrupt (); with_attributes regular_interrupts (fn _ => fn x => f x) x);
-
-fun uninterruptible f =
- with_attributes no_interrupts (fn atts => fn x =>
- f (fn g => with_attributes atts (fn _ => fn y => g y)) x);
+fun uninterruptible f x =
+ with_attributes no_interrupts (fn atts =>
+ f (fn g => fn y => with_attributes atts (fn _ => g y)) x);
(* synchronous wait *)
-fun sync_attributes e =
+fun sync_wait opt_atts time cond lock =
+ with_attributes
+ (sync_interrupts (case opt_atts of SOME atts => atts | NONE => Thread.getAttributes ()))
+ (fn _ =>
+ (case time of
+ SOME t => Exn.Result (ConditionVar.waitUntil (cond, lock, t))
+ | NONE => (ConditionVar.wait (cond, lock); Exn.Result true))
+ handle exn => Exn.Exn exn);
+
+
+(* tracing *)
+
+val trace = ref 0;
+
+fun tracing level msg =
+ if level > ! trace then ()
+ else uninterruptible (fn _ => fn () =>
+ (TextIO.output (TextIO.stdErr, (">>> " ^ msg () ^ "\n")); TextIO.flushOut TextIO.stdErr)
+ handle _ (*sic*) => ()) ();
+
+fun tracing_time detailed time =
+ tracing
+ (if not detailed then 5
+ else if Time.>= (time, Time.fromMilliseconds 1000) then 1
+ else if Time.>= (time, Time.fromMilliseconds 100) then 2
+ else if Time.>= (time, Time.fromMilliseconds 10) then 3
+ else if Time.>= (time, Time.fromMilliseconds 1) then 4 else 5);
+
+fun real_time f x =
let
- val orig_atts = Thread.getAttributes ();
- val broadcast =
- (case List.find (fn Thread.EnableBroadcastInterrupt _ => true | _ => false) orig_atts of
- NONE => Thread.EnableBroadcastInterrupt false
- | SOME att => att);
- val interrupt_state =
- (case List.find (fn Thread.InterruptState _ => true | _ => false) orig_atts of
- NONE => Thread.InterruptState Thread.InterruptDefer
- | SOME (state as Thread.InterruptState Thread.InterruptDefer) => state
- | _ => Thread.InterruptState Thread.InterruptSynch);
- in with_attributes [broadcast, interrupt_state] (fn _ => fn () => e ()) () end;
-
-fun sync_wait time cond lock =
- sync_attributes (fn () =>
- (case time of
- SOME t => ConditionVar.waitUntil (cond, lock, t)
- | NONE => (ConditionVar.wait (cond, lock); true)));
+ val timer = Timer.startRealTimer ();
+ val () = f x;
+ val time = Timer.checkRealTimer timer;
+ in time end;
(* execution with time limit *)
@@ -169,7 +163,7 @@
(* system shell processes, with propagation of interrupts *)
-fun system_out script = uninterruptible (fn restore_attributes => fn () =>
+fun system_out script = with_attributes no_interrupts (fn orig_atts =>
let
val script_name = OS.FileSys.tmpName ();
val _ = write_file script_name script;
@@ -180,13 +174,12 @@
(*result state*)
datatype result = Wait | Signal | Result of int;
val result = ref Wait;
- val result_mutex = Mutex.mutex ();
- val result_cond = ConditionVar.conditionVar ();
+ val lock = Mutex.mutex ();
+ val cond = ConditionVar.conditionVar ();
fun set_result res =
- (Mutex.lock result_mutex; result := res; Mutex.unlock result_mutex;
- ConditionVar.signal result_cond);
+ (Mutex.lock lock; result := res; ConditionVar.signal cond; Mutex.unlock lock);
- val _ = Mutex.lock result_mutex;
+ val _ = Mutex.lock lock;
(*system thread*)
val system_thread = Thread.fork (fn () =>
@@ -216,11 +209,12 @@
handle OS.SysErr _ => () | IO.Io _ =>
(OS.Process.sleep (Time.fromMilliseconds 100); if n > 0 then kill (n - 1) else ());
- val _ = while ! result = Wait do
- restore_attributes (fn () =>
- (ignore (sync_wait (SOME (Time.+ (Time.now (), Time.fromMilliseconds 100)))
- result_cond result_mutex)
- handle Exn.Interrupt => kill 10)) ();
+ val _ =
+ while ! result = Wait do
+ let val res =
+ sync_wait (SOME orig_atts)
+ (SOME (Time.+ (Time.now (), Time.fromMilliseconds 100))) cond lock
+ in case res of Exn.Exn Exn.Interrupt => kill 10 | _ => () end;
(*cleanup*)
val output = read_file output_name handle IO.Io _ => "";
@@ -229,7 +223,7 @@
val _ = OS.FileSys.remove output_name handle OS.SysErr _ => ();
val _ = Thread.interrupt system_thread handle Thread _ => ();
val rc = (case ! result of Signal => raise Exn.Interrupt | Result rc => rc);
- in (output, rc) end) ();
+ in (output, rc) end);
(* critical section -- may be nested within the same thread *)