src/Pure/ML-Systems/multithreading_dummy.ML

sort indexes according to symbolic update_time (multithreading-safe);

(*  Title:      Pure/ML-Systems/multithreading_dummy.ML
    ID:         $Id$
    Author:     Makarius

Compatibility file for ML systems without multithreading.
*)

structure Task =
struct
  datatype task = Task of (unit -> unit) | Running | Finished;
  fun is_running Running = true | is_running _ = false;
  fun is_finished Finished = true | is_finished _ = false;
end;

signature MULTITHREADING =
sig
  val trace: int ref
  val tracing: int -> (unit -> string) -> unit
  val available: bool
  val max_threads: int ref
  val self_critical: unit -> bool
  val NAMED_CRITICAL: string -> (unit -> 'a) -> 'a
  val CRITICAL: (unit -> 'a) -> 'a
  val schedule: int -> ('a -> (Task.task * ('a -> 'a)) * 'a) -> 'a -> exn list
end;

structure Multithreading: MULTITHREADING =
struct

val trace = ref 0;
fun tracing _ _ = ();

val available = false;
val max_threads = ref 1;

fun self_critical () = false;
fun NAMED_CRITICAL _ e = e ();
fun CRITICAL e = e ();

fun schedule _ _ _ = raise Fail "No multithreading support";

end;

val NAMED_CRITICAL = Multithreading.NAMED_CRITICAL;
val CRITICAL = Multithreading.CRITICAL;