| changeset 4977 | 6cec2c0ffdbf |
| parent 4506 | f21ec26b2265 |
| child 5038 | 301c37df931d |
| 4976:19f48dafe5d3 | 4977:6cec2c0ffdbf |
|---|---|
54 " both "^ string_of_time both ^ " secs\n" |
54 " both "^ string_of_time both ^ " secs\n" |
55 end |
55 end |
56 end; |
56 end; |
57 |
57 |
58 |
58 |
59 (* prompts *) |
|
60 |
|
61 fun ml_prompts p1 p2 = (); |
|
59 |
62 |
60 |
63 |
61 (* toplevel pretty printing (see also Pure/install_pp.ML) *) |
64 (* toplevel pretty printing (see also Pure/install_pp.ML) *) |
62 |
65 |
63 fun make_pp path pprint = |
66 fun make_pp path pprint = |