src/Pure/Concurrent/par_list_sequential.ML
author wenzelm
Fri, 14 Nov 2014 11:19:14 +0100
changeset 59004 6573e6d64ec8
parent 44269 3ff2fd162aee
permissions -rw-r--r--
proper sequential version (cf. 302104d8366b);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
32816
5db89f8d44f3 more official status of sequential implementations;
wenzelm
parents: 29368
diff changeset
     1
(*  Title:      Pure/Concurrent/par_list_sequential.ML
28546
d57bfb44c9e5 Dummy version of parallel list combinators -- plain sequential evaluation.
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
d57bfb44c9e5 Dummy version of parallel list combinators -- plain sequential evaluation.
wenzelm
parents:
diff changeset
     3
d57bfb44c9e5 Dummy version of parallel list combinators -- plain sequential evaluation.
wenzelm
parents:
diff changeset
     4
Dummy version of parallel list combinators -- plain sequential evaluation.
d57bfb44c9e5 Dummy version of parallel list combinators -- plain sequential evaluation.
wenzelm
parents:
diff changeset
     5
*)
d57bfb44c9e5 Dummy version of parallel list combinators -- plain sequential evaluation.
wenzelm
parents:
diff changeset
     6
29368
503ce3f8f092 renamed structure ParList to Par_List;
wenzelm
parents: 28556
diff changeset
     7
structure Par_List: PAR_LIST =
28546
d57bfb44c9e5 Dummy version of parallel list combinators -- plain sequential evaluation.
wenzelm
parents:
diff changeset
     8
struct
d57bfb44c9e5 Dummy version of parallel list combinators -- plain sequential evaluation.
wenzelm
parents:
diff changeset
     9
44269
3ff2fd162aee updated sequential version (cf. b94951f06e48);
wenzelm
parents: 41711
diff changeset
    10
fun managed_results _ f = map (Exn.capture f);
41711
3422ae5aff3a more tracing information via Par_List.map_name;
wenzelm
parents: 32816
diff changeset
    11
fun map_name _ = map;
28546
d57bfb44c9e5 Dummy version of parallel list combinators -- plain sequential evaluation.
wenzelm
parents:
diff changeset
    12
val map = map;
59004
6573e6d64ec8 proper sequential version (cf. 302104d8366b);
wenzelm
parents: 44269
diff changeset
    13
val map_independent = map;
28546
d57bfb44c9e5 Dummy version of parallel list combinators -- plain sequential evaluation.
wenzelm
parents:
diff changeset
    14
val get_some = get_first;
28556
85d2972fe9e6 fixed spelling;
wenzelm
parents: 28546
diff changeset
    15
val find_some = find_first;
28546
d57bfb44c9e5 Dummy version of parallel list combinators -- plain sequential evaluation.
wenzelm
parents:
diff changeset
    16
val exists = exists;
d57bfb44c9e5 Dummy version of parallel list combinators -- plain sequential evaluation.
wenzelm
parents:
diff changeset
    17
val forall = forall;
d57bfb44c9e5 Dummy version of parallel list combinators -- plain sequential evaluation.
wenzelm
parents:
diff changeset
    18
d57bfb44c9e5 Dummy version of parallel list combinators -- plain sequential evaluation.
wenzelm
parents:
diff changeset
    19
end;