| author | blanchet | 
| Fri, 28 Sep 2012 09:12:49 +0200 | |
| changeset 49631 | 9ce0c2cbadb8 | 
| parent 44269 | 3ff2fd162aee | 
| child 59004 | 6573e6d64ec8 | 
| permissions | -rw-r--r-- | 
| 32816 
5db89f8d44f3
more official status of sequential implementations;
 wenzelm parents: 
29368diff
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 | 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 | 10 | fun managed_results _ f = map (Exn.capture f); | 
| 41711 | 11 | fun map_name _ = map; | 
| 28546 
d57bfb44c9e5
Dummy version of parallel list combinators -- plain sequential evaluation.
 wenzelm parents: diff
changeset | 12 | val map = map; | 
| 
d57bfb44c9e5
Dummy version of parallel list combinators -- plain sequential evaluation.
 wenzelm parents: diff
changeset | 13 | val get_some = get_first; | 
| 28556 | 14 | val find_some = find_first; | 
| 28546 
d57bfb44c9e5
Dummy version of parallel list combinators -- plain sequential evaluation.
 wenzelm parents: diff
changeset | 15 | val exists = exists; | 
| 
d57bfb44c9e5
Dummy version of parallel list combinators -- plain sequential evaluation.
 wenzelm parents: diff
changeset | 16 | val forall = forall; | 
| 
d57bfb44c9e5
Dummy version of parallel list combinators -- plain sequential evaluation.
 wenzelm parents: diff
changeset | 17 | |
| 
d57bfb44c9e5
Dummy version of parallel list combinators -- plain sequential evaluation.
 wenzelm parents: diff
changeset | 18 | end; |