changeset 29564 | f8b933a62151 |
parent 28268 | ac8431ecd57e |
child 30672 | beaadd5af500 |
29563:4773c5c994dc | 29564:f8b933a62151 |
---|---|
1 (* Title: Pure/ML-Systems/polyml_old_compiler5.ML |
1 (* Title: Pure/ML-Systems/polyml_old_compiler5.ML |
2 ID: $Id$ |
|
3 |
2 |
4 Runtime compilation -- for old PolyML.compilerEx (version 5.0, 5.1). |
3 Runtime compilation -- for old PolyML.compilerEx (version 5.0, 5.1). |
5 *) |
4 *) |
6 |
5 |
7 fun use_text (tune: string -> string) _ _ (line, name) (print, err) verbose txt = |
6 fun use_text (tune: string -> string) _ _ (line, name) (print, err) verbose txt = |