# HG changeset patch
# User wenzelm
# Date 1416998631 -3600
# Node ID 61b723761dff913e86e5958de67c00489d207d4e
# Parent  43e07797269b37c08f098698ed7d7aeede6f3cf6
load simple_thread.ML later, such that it benefits from redefined print_exception_trace;

diff -r 43e07797269b -r 61b723761dff src/Pure/Concurrent/future.ML
--- a/src/Pure/Concurrent/future.ML	Tue Nov 25 17:30:05 2014 +0100
+++ b/src/Pure/Concurrent/future.ML	Wed Nov 26 11:43:51 2014 +0100
@@ -114,7 +114,7 @@
   val lock = Mutex.mutex ();
 in
 
-fun SYNCHRONIZED name = Simple_Thread.synchronized name lock;
+fun SYNCHRONIZED name = Multithreading.synchronized name lock;
 
 fun wait cond = (*requires SYNCHRONIZED*)
   Multithreading.sync_wait NONE NONE cond lock;
diff -r 43e07797269b -r 61b723761dff src/Pure/Concurrent/simple_thread.ML
--- a/src/Pure/Concurrent/simple_thread.ML	Tue Nov 25 17:30:05 2014 +0100
+++ b/src/Pure/Concurrent/simple_thread.ML	Wed Nov 26 11:43:51 2014 +0100
@@ -11,7 +11,6 @@
   val fork: bool -> (unit -> unit) -> Thread.thread
   val join: Thread.thread -> unit
   val interrupt_unsynchronized: Thread.thread -> unit
-  val synchronized: string -> Mutex.mutex -> (unit -> 'a) -> 'a
 end;
 
 structure Simple_Thread: SIMPLE_THREAD =
@@ -34,27 +33,4 @@
 
 fun interrupt_unsynchronized thread = Thread.interrupt thread handle Thread _ => ();
 
-
-(* basic synchronization *)
-
-fun synchronized name lock e =
-  if Multithreading.available then
-    Exn.release (uninterruptible (fn restore_attributes => fn () =>
-      let
-        val immediate =
-          if Mutex.trylock lock then true
-          else
-            let
-              val _ = Multithreading.tracing 5 (fn () => name ^ ": locking ...");
-              val time = Multithreading.real_time Mutex.lock lock;
-              val _ = Multithreading.tracing_time true time
-                (fn () => name ^ ": locked after " ^ Time.toString time);
-            in false end;
-        val result = Exn.capture (restore_attributes e) ();
-        val _ =
-          if immediate then () else Multithreading.tracing 5 (fn () => name ^ ": unlocking ...");
-        val _ = Mutex.unlock lock;
-      in result end) ())
-  else e ();
-
 end;
diff -r 43e07797269b -r 61b723761dff src/Pure/Concurrent/single_assignment.ML
--- a/src/Pure/Concurrent/single_assignment.ML	Tue Nov 25 17:30:05 2014 +0100
+++ b/src/Pure/Concurrent/single_assignment.ML	Wed Nov 26 11:43:51 2014 +0100
@@ -32,7 +32,7 @@
 fun peek (Var {var, ...}) = SingleAssignment.savalue var;
 
 fun await (v as Var {name, lock, cond, ...}) =
-  Simple_Thread.synchronized name lock (fn () =>
+  Multithreading.synchronized name lock (fn () =>
     let
       fun wait () =
         (case peek v of
@@ -44,7 +44,7 @@
     in wait () end);
 
 fun assign (v as Var {name, lock, cond, var}) x =
-  Simple_Thread.synchronized name lock (fn () =>
+  Multithreading.synchronized name lock (fn () =>
     (case peek v of
       SOME _ => raise Fail ("Duplicate assignment to " ^ name)
     | NONE =>
diff -r 43e07797269b -r 61b723761dff src/Pure/Concurrent/synchronized.ML
--- a/src/Pure/Concurrent/synchronized.ML	Tue Nov 25 17:30:05 2014 +0100
+++ b/src/Pure/Concurrent/synchronized.ML	Wed Nov 26 11:43:51 2014 +0100
@@ -39,7 +39,7 @@
 (* synchronized access *)
 
 fun timed_access (Var {name, lock, cond, var}) time_limit f =
-  Simple_Thread.synchronized name lock (fn () =>
+  Multithreading.synchronized name lock (fn () =>
     let
       fun try_change () =
         let val x = ! var in
diff -r 43e07797269b -r 61b723761dff src/Pure/ML-Systems/multithreading.ML
--- a/src/Pure/ML-Systems/multithreading.ML	Tue Nov 25 17:30:05 2014 +0100
+++ b/src/Pure/ML-Systems/multithreading.ML	Wed Nov 26 11:43:51 2014 +0100
@@ -31,6 +31,7 @@
   val tracing_time: bool -> Time.time -> (unit -> string) -> unit
   val real_time: ('a -> unit) -> 'a -> Time.time
   val self_critical: unit -> bool
+  val synchronized: string -> Mutex.mutex -> (unit -> 'a) -> 'a
   val serial: unit -> int
 end;
 
@@ -74,6 +75,8 @@
 fun NAMED_CRITICAL _ e = e ();
 fun CRITICAL e = e ();
 
+fun synchronized _ _ e = e ();
+
 
 (* serial numbers *)
 
diff -r 43e07797269b -r 61b723761dff src/Pure/ML-Systems/multithreading_polyml.ML
--- a/src/Pure/ML-Systems/multithreading_polyml.ML	Tue Nov 25 17:30:05 2014 +0100
+++ b/src/Pure/ML-Systems/multithreading_polyml.ML	Wed Nov 26 11:43:51 2014 +0100
@@ -184,6 +184,22 @@
 
 end;
 
+fun synchronized name lock e =
+  Exn.release (uninterruptible (fn restore_attributes => fn () =>
+    let
+      val immediate =
+        if Mutex.trylock lock then true
+        else
+          let
+            val _ = tracing 5 (fn () => name ^ ": locking ...");
+            val time = real_time Mutex.lock lock;
+            val _ = tracing_time true time (fn () => name ^ ": locked after " ^ Time.toString time);
+          in false end;
+      val result = Exn.capture (restore_attributes e) ();
+      val _ = if immediate then () else tracing 5 (fn () => name ^ ": unlocking ...");
+      val _ = Mutex.unlock lock;
+    in result end) ());
+
 
 (* serial numbers *)
 
diff -r 43e07797269b -r 61b723761dff src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Tue Nov 25 17:30:05 2014 +0100
+++ b/src/Pure/ROOT.ML	Wed Nov 26 11:43:51 2014 +0100
@@ -18,8 +18,6 @@
 use "General/alist.ML";
 use "General/table.ML";
 
-use "Concurrent/simple_thread.ML";
-
 use "Concurrent/synchronized.ML";
 if Multithreading.available then ()
 else use "Concurrent/synchronized_sequential.ML";
@@ -51,6 +49,7 @@
 val toplevel_pp = Secure.toplevel_pp;
 
 
+
 (** bootstrap phase 1: towards ML within Isar context *)
 
 (* library of general tools *)
@@ -107,6 +106,8 @@
 then use "ML/ml_statistics_polyml-5.5.0.ML"
 else use "ML/ml_statistics_dummy.ML";
 
+use "Concurrent/simple_thread.ML";
+
 use "Concurrent/single_assignment.ML";
 if Multithreading.available then ()
 else use "Concurrent/single_assignment_sequential.ML";