src/Pure/ML-Systems/multithreading_dummy.ML
author wenzelm
Tue, 24 Jul 2007 19:44:33 +0200
changeset 23962 e0358fac0541
parent 23960 c07ae96cbfc4
child 23973 b6ce6de5b700
permissions -rw-r--r--
Runtime exceptions as values (from library.ML);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
23960
c07ae96cbfc4 Compatibility file for ML systems without multithreading.
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/ML-Systems/multithreading_dummy.ML
c07ae96cbfc4 Compatibility file for ML systems without multithreading.
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
c07ae96cbfc4 Compatibility file for ML systems without multithreading.
wenzelm
parents:
diff changeset
     3
    Author:     Makarius
c07ae96cbfc4 Compatibility file for ML systems without multithreading.
wenzelm
parents:
diff changeset
     4
c07ae96cbfc4 Compatibility file for ML systems without multithreading.
wenzelm
parents:
diff changeset
     5
Compatibility file for ML systems without multithreading.
c07ae96cbfc4 Compatibility file for ML systems without multithreading.
wenzelm
parents:
diff changeset
     6
*)
c07ae96cbfc4 Compatibility file for ML systems without multithreading.
wenzelm
parents:
diff changeset
     7
c07ae96cbfc4 Compatibility file for ML systems without multithreading.
wenzelm
parents:
diff changeset
     8
signature MULTITHREADING =
c07ae96cbfc4 Compatibility file for ML systems without multithreading.
wenzelm
parents:
diff changeset
     9
sig
c07ae96cbfc4 Compatibility file for ML systems without multithreading.
wenzelm
parents:
diff changeset
    10
  val number_of_threads: int ref
c07ae96cbfc4 Compatibility file for ML systems without multithreading.
wenzelm
parents:
diff changeset
    11
  val self_critical: unit -> bool
c07ae96cbfc4 Compatibility file for ML systems without multithreading.
wenzelm
parents:
diff changeset
    12
  val CRITICAL: (unit -> 'a) -> 'a
c07ae96cbfc4 Compatibility file for ML systems without multithreading.
wenzelm
parents:
diff changeset
    13
end;
c07ae96cbfc4 Compatibility file for ML systems without multithreading.
wenzelm
parents:
diff changeset
    14
c07ae96cbfc4 Compatibility file for ML systems without multithreading.
wenzelm
parents:
diff changeset
    15
structure Multithreading: MULTITHREADING =
c07ae96cbfc4 Compatibility file for ML systems without multithreading.
wenzelm
parents:
diff changeset
    16
struct
c07ae96cbfc4 Compatibility file for ML systems without multithreading.
wenzelm
parents:
diff changeset
    17
c07ae96cbfc4 Compatibility file for ML systems without multithreading.
wenzelm
parents:
diff changeset
    18
val number_of_threads = ref 0;
c07ae96cbfc4 Compatibility file for ML systems without multithreading.
wenzelm
parents:
diff changeset
    19
c07ae96cbfc4 Compatibility file for ML systems without multithreading.
wenzelm
parents:
diff changeset
    20
fun self_critical () = false;
c07ae96cbfc4 Compatibility file for ML systems without multithreading.
wenzelm
parents:
diff changeset
    21
fun CRITICAL e = e ();
c07ae96cbfc4 Compatibility file for ML systems without multithreading.
wenzelm
parents:
diff changeset
    22
c07ae96cbfc4 Compatibility file for ML systems without multithreading.
wenzelm
parents:
diff changeset
    23
end;
c07ae96cbfc4 Compatibility file for ML systems without multithreading.
wenzelm
parents:
diff changeset
    24
c07ae96cbfc4 Compatibility file for ML systems without multithreading.
wenzelm
parents:
diff changeset
    25
val CRITICAL = Multithreading.CRITICAL;