equal
deleted
inserted
replaced
4 ML toplevel pretty-printing for logical entities. |
4 ML toplevel pretty-printing for logical entities. |
5 *) |
5 *) |
6 |
6 |
7 structure ML_PP: sig end = |
7 structure ML_PP: sig end = |
8 struct |
8 struct |
|
9 |
|
10 val _ = |
|
11 ML_system_pp (fn _ => fn _ => fn t => |
|
12 PolyML.PrettyString ("<thread " ^ quote (Isabelle_Thread.print t) ^ |
|
13 (if Isabelle_Thread.is_active t then "" else " (inactive)") ^ ">")); |
9 |
14 |
10 val _ = |
15 val _ = |
11 ML_system_pp (fn _ => fn _ => Pretty.to_polyml o Proof_Display.pp_context); |
16 ML_system_pp (fn _ => fn _ => Pretty.to_polyml o Proof_Display.pp_context); |
12 |
17 |
13 val _ = |
18 val _ = |