# HG changeset patch
# User wenzelm
# Date 1185299071 -7200
# Node ID c07ae96cbfc4c4a1cce9af5b4c2d46969d5af7f8
# Parent  c2e81bcee06b25e354db7cd2b05d61108ab82cb6
Compatibility file for ML systems without multithreading.

diff -r c2e81bcee06b -r c07ae96cbfc4 src/Pure/ML-Systems/multithreading_dummy.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML-Systems/multithreading_dummy.ML	Tue Jul 24 19:44:31 2007 +0200
@@ -0,0 +1,25 @@
+(*  Title:      Pure/ML-Systems/multithreading_dummy.ML
+    ID:         $Id$
+    Author:     Makarius
+
+Compatibility file for ML systems without multithreading.
+*)
+
+signature MULTITHREADING =
+sig
+  val number_of_threads: int ref
+  val self_critical: unit -> bool
+  val CRITICAL: (unit -> 'a) -> 'a
+end;
+
+structure Multithreading: MULTITHREADING =
+struct
+
+val number_of_threads = ref 0;
+
+fun self_critical () = false;
+fun CRITICAL e = e ();
+
+end;
+
+val CRITICAL = Multithreading.CRITICAL;