equal
deleted
inserted
replaced
56 fun PG_setup () = |
56 fun PG_setup () = |
57 use_global "val change = Unsynchronized.change; structure ThyLoad = ProofGeneral.ThyLoad;"; |
57 use_global "val change = Unsynchronized.change; structure ThyLoad = ProofGeneral.ThyLoad;"; |
58 |
58 |
59 end; |
59 end; |
60 |
60 |
61 (*override previous toplevel bindings!*) |
|
62 val use_text = Secure.use_text; |
|
63 val use_file = Secure.use_file; |
|
64 |
|
65 fun use s = |
|
66 Position.setmp_thread_data (Position.file_only s) |
|
67 (fn () => |
|
68 Secure.use_file ML_Parse.global_context true s |
|
69 handle ERROR msg => (writeln msg; error "ML error")) (); |
|
70 |
|
71 val toplevel_pp = Secure.toplevel_pp; |
|
72 |
|