equal
deleted
inserted
replaced
30 |
30 |
31 |
31 |
32 (*Interface for toplevel pretty printers, see also Pure/install_pp.ML*) |
32 (*Interface for toplevel pretty printers, see also Pure/install_pp.ML*) |
33 |
33 |
34 fun make_pp _ pprint (str, blk, brk, en) obj = |
34 fun make_pp _ pprint (str, blk, brk, en) obj = |
35 pprint obj (str, fn ind => blk (ind, false), fn wd => brk (wd, 0), en); |
35 pprint obj (str, fn ind => blk (ind, false), fn wd => brk (wd, 0), |
|
36 fn () => brk (99999, 0), en); |
36 |
37 |
37 |
38 |
38 (*** File information ***) |
39 (*** File information ***) |
39 |
40 |
40 (*Get time of last modification.*) |
41 (*Get time of last modification.*) |