equal
deleted
inserted
replaced
23 (*Finish timing and return string*) |
23 (*Finish timing and return string*) |
24 fun endTiming before = |
24 fun endTiming before = |
25 "User + GC: " ^ |
25 "User + GC: " ^ |
26 makestring (real (System.processtime () - before) / 10.0) ^ |
26 makestring (real (System.processtime () - before) / 10.0) ^ |
27 " secs"; |
27 " secs"; |
|
28 |
|
29 |
|
30 (* prompts *) |
|
31 |
|
32 fun ml_prompts p1 p2 = (PolyML.Compiler.prompt1 := p1; PolyML.Compiler.prompt1 := p2); |
28 |
33 |
29 |
34 |
30 (* toplevel pretty printing (see also Pure/install_pp.ML) *) |
35 (* toplevel pretty printing (see also Pure/install_pp.ML) *) |
31 |
36 |
32 fun make_pp _ pprint (str, blk, brk, en) obj = |
37 fun make_pp _ pprint (str, blk, brk, en) obj = |