removed unused sync_interrupts;
authorwenzelm
Mon Sep 08 20:33:29 2008 +0200 (2008-09-08)
changeset 28169356fc8734741
parent 28168 ba410235ff04
child 28170 a18cf8a0e656
removed unused sync_interrupts;
src/Pure/ML-Systems/multithreading.ML
src/Pure/ML-Systems/multithreading_polyml.ML
     1.1 --- a/src/Pure/ML-Systems/multithreading.ML	Mon Sep 08 20:33:27 2008 +0200
     1.2 +++ b/src/Pure/ML-Systems/multithreading.ML	Mon Sep 08 20:33:29 2008 +0200
     1.3 @@ -20,7 +20,6 @@
     1.4    val max_threads: int ref
     1.5    val max_threads_value: unit -> int
     1.6    val no_interrupts: Thread.threadAttribute list
     1.7 -  val sync_interrupts: Thread.threadAttribute list
     1.8    val regular_interrupts: Thread.threadAttribute list
     1.9    val with_attributes: Thread.threadAttribute list ->
    1.10      (Thread.threadAttribute list -> 'a -> 'b) -> 'a -> 'b
    1.11 @@ -41,7 +40,6 @@
    1.12  fun max_threads_value () = Int.max (! max_threads, 1);
    1.13  
    1.14  val no_interrupts = [];
    1.15 -val sync_interrupts = [];
    1.16  val regular_interrupts = [];
    1.17  
    1.18  fun with_attributes _ f x = f [] x;
     2.1 --- a/src/Pure/ML-Systems/multithreading_polyml.ML	Mon Sep 08 20:33:27 2008 +0200
     2.2 +++ b/src/Pure/ML-Systems/multithreading_polyml.ML	Mon Sep 08 20:33:29 2008 +0200
     2.3 @@ -65,9 +65,6 @@
     2.4  val no_interrupts =
     2.5    [Thread.EnableBroadcastInterrupt false, Thread.InterruptState Thread.InterruptDefer];
     2.6  
     2.7 -val sync_interrupts =
     2.8 -  [Thread.EnableBroadcastInterrupt false, Thread.InterruptState Thread.InterruptSynch];
     2.9 -
    2.10  val regular_interrupts =
    2.11    [Thread.EnableBroadcastInterrupt true, Thread.InterruptState Thread.InterruptAsynchOnce];
    2.12