src/Pure/Concurrent/multithreading.ML
changeset 62891 7a11ea5c9626
parent 62826 eb94e570c1a4
child 62892 7485507620b6
     1.1 --- a/src/Pure/Concurrent/multithreading.ML	Wed Apr 06 16:51:52 2016 +0200
     1.2 +++ b/src/Pure/Concurrent/multithreading.ML	Wed Apr 06 17:16:30 2016 +0200
     1.3 @@ -4,21 +4,16 @@
     1.4  Multithreading in Poly/ML (cf. polyml/basis/Thread.sml).
     1.5  *)
     1.6  
     1.7 -signature BASIC_MULTITHREADING =
     1.8 -sig
     1.9 -  val interruptible: ('a -> 'b) -> 'a -> 'b
    1.10 -  val uninterruptible: ((('c -> 'd) -> 'c -> 'd) -> 'a -> 'b) -> 'a -> 'b
    1.11 -end;
    1.12 -
    1.13  signature MULTITHREADING =
    1.14  sig
    1.15 -  include BASIC_MULTITHREADING
    1.16    val no_interrupts: Thread.threadAttribute list
    1.17    val public_interrupts: Thread.threadAttribute list
    1.18    val private_interrupts: Thread.threadAttribute list
    1.19    val sync_interrupts: Thread.threadAttribute list -> Thread.threadAttribute list
    1.20    val interrupted: unit -> unit  (*exception Interrupt*)
    1.21    val with_attributes: Thread.threadAttribute list -> (Thread.threadAttribute list -> 'a) -> 'a
    1.22 +  val interruptible: ('a -> 'b) -> 'a -> 'b
    1.23 +  val uninterruptible: ((('c -> 'd) -> 'c -> 'd) -> 'a -> 'b) -> 'a -> 'b
    1.24    val max_threads_value: unit -> int
    1.25    val max_threads_update: int -> unit
    1.26    val enabled: unit -> bool
    1.27 @@ -75,9 +70,6 @@
    1.28      val _ = Thread.setAttributes orig_atts;
    1.29    in Exn.release result end;
    1.30  
    1.31 -
    1.32 -(* portable wrappers *)
    1.33 -
    1.34  fun interruptible f x = with_attributes public_interrupts (fn _ => f x);
    1.35  
    1.36  fun uninterruptible f x =
    1.37 @@ -179,6 +171,3 @@
    1.38  end;
    1.39  
    1.40  end;
    1.41 -
    1.42 -structure Basic_Multithreading: BASIC_MULTITHREADING = Multithreading;
    1.43 -open Basic_Multithreading;