src/Pure/Concurrent/multithreading.ML
changeset 62891 7a11ea5c9626
parent 62826 eb94e570c1a4
child 62892 7485507620b6
--- a/src/Pure/Concurrent/multithreading.ML	Wed Apr 06 16:51:52 2016 +0200
+++ b/src/Pure/Concurrent/multithreading.ML	Wed Apr 06 17:16:30 2016 +0200
@@ -4,21 +4,16 @@
 Multithreading in Poly/ML (cf. polyml/basis/Thread.sml).
 *)
 
-signature BASIC_MULTITHREADING =
-sig
-  val interruptible: ('a -> 'b) -> 'a -> 'b
-  val uninterruptible: ((('c -> 'd) -> 'c -> 'd) -> 'a -> 'b) -> 'a -> 'b
-end;
-
 signature MULTITHREADING =
 sig
-  include BASIC_MULTITHREADING
   val no_interrupts: Thread.threadAttribute list
   val public_interrupts: Thread.threadAttribute list
   val private_interrupts: Thread.threadAttribute list
   val sync_interrupts: Thread.threadAttribute list -> Thread.threadAttribute list
   val interrupted: unit -> unit  (*exception Interrupt*)
   val with_attributes: Thread.threadAttribute list -> (Thread.threadAttribute list -> 'a) -> 'a
+  val interruptible: ('a -> 'b) -> 'a -> 'b
+  val uninterruptible: ((('c -> 'd) -> 'c -> 'd) -> 'a -> 'b) -> 'a -> 'b
   val max_threads_value: unit -> int
   val max_threads_update: int -> unit
   val enabled: unit -> bool
@@ -75,9 +70,6 @@
     val _ = Thread.setAttributes orig_atts;
   in Exn.release result end;
 
-
-(* portable wrappers *)
-
 fun interruptible f x = with_attributes public_interrupts (fn _ => f x);
 
 fun uninterruptible f x =
@@ -179,6 +171,3 @@
 end;
 
 end;
-
-structure Basic_Multithreading: BASIC_MULTITHREADING = Multithreading;
-open Basic_Multithreading;