equal
deleted
inserted
replaced
153 |
153 |
154 in |
154 in |
155 |
155 |
156 fun toplevel_loop in_stream {init = do_init, welcome, sync, secure} = |
156 fun toplevel_loop in_stream {init = do_init, welcome, sync, secure} = |
157 (Context.set_thread_data NONE; |
157 (Context.set_thread_data NONE; |
158 if do_init then (Options.load_default (); init ()) else (); |
158 if do_init then init () else (); |
159 Output.Private_Hooks.protocol_message_fn := protocol_message; |
159 Output.Private_Hooks.protocol_message_fn := protocol_message; |
160 if welcome then writeln (Session.welcome ()) else (); |
160 if welcome then writeln (Session.welcome ()) else (); |
161 uninterruptible (fn _ => fn () => raw_loop secure (Outer_Syntax.isar in_stream sync)) ()); |
161 uninterruptible (fn _ => fn () => raw_loop secure (Outer_Syntax.isar in_stream sync)) ()); |
162 |
162 |
163 end; |
163 end; |