equal
deleted
inserted
replaced
61 (*override previous toplevel bindings!*) |
61 (*override previous toplevel bindings!*) |
62 val use_text = Secure.use_text; |
62 val use_text = Secure.use_text; |
63 val use_file = Secure.use_file; |
63 val use_file = Secure.use_file; |
64 |
64 |
65 fun use s = |
65 fun use s = |
66 Position.setmp_thread_data (Position.of_properties (Position.file_name s)) |
66 Position.setmp_thread_data (Position.file_only s) |
67 (fn () => |
67 (fn () => |
68 Secure.use_file ML_Parse.global_context true s |
68 Secure.use_file ML_Parse.global_context true s |
69 handle ERROR msg => (writeln msg; error "ML error")) (); |
69 handle ERROR msg => (writeln msg; error "ML error")) (); |
70 |
70 |
71 val toplevel_pp = Secure.toplevel_pp; |
71 val toplevel_pp = Secure.toplevel_pp; |