isabelle: src/Pure/Concurrent/ROOT.ML@479806475f3c (annotated)

28308 d4396a28fb29 fixed headers haftmann parents: 28240 diff changeset	1	(* Title: Pure/Concurrent/ROOT.ML
29118 8f2481aa363d removed old scheduler; wenzelm parents: 29071 diff changeset	2	Author: Makarius
28200 5ef2c4bde4e5 separate Concurrent/ROOT.ML; wenzelm parents: diff changeset	3
5ef2c4bde4e5 separate Concurrent/ROOT.ML; wenzelm parents: diff changeset	4	Concurrency within the ML runtime.
5ef2c4bde4e5 separate Concurrent/ROOT.ML; wenzelm parents: diff changeset	5	*)
5ef2c4bde4e5 separate Concurrent/ROOT.ML; wenzelm parents: diff changeset	6
28240 444d1e8ae496 added Concurrent/simple_thread.ML; wenzelm parents: 28200 diff changeset	7	use "simple_thread.ML";
28574 e73db43298a6 added Concurrent/synchronized.ML; wenzelm parents: 28547 diff changeset	8	use "synchronized.ML";
28200 5ef2c4bde4e5 separate Concurrent/ROOT.ML; wenzelm parents: diff changeset	9	use "mailbox.ML";
5ef2c4bde4e5 separate Concurrent/ROOT.ML; wenzelm parents: diff changeset	10	use "task_queue.ML";
5ef2c4bde4e5 separate Concurrent/ROOT.ML; wenzelm parents: diff changeset	11	use "future.ML";
5ef2c4bde4e5 separate Concurrent/ROOT.ML; wenzelm parents: diff changeset	12	use "par_list.ML";
28547 c81f6344bfb7 added future_scheduler flag (tmp!), from skip_proofs.ML; wenzelm parents: 28308 diff changeset	13	if Multithreading.available then () else use "par_list_dummy.ML";
c81f6344bfb7 added future_scheduler flag (tmp!), from skip_proofs.ML; wenzelm parents: 28308 diff changeset	14