equal
deleted
inserted
replaced
87 |
87 |
88 (* init *) |
88 (* init *) |
89 |
89 |
90 fun init out = |
90 fun init out = |
91 (Unsynchronized.change print_mode |
91 (Unsynchronized.change print_mode |
92 (fold (update op =) [isabelle_processN, OuterKeyword.keyword_status_reportN, Pretty.symbolicN]); |
92 (fold (update op =) [isabelle_processN, Keyword.keyword_status_reportN, Pretty.symbolicN]); |
93 setup_channels out |> init_message; |
93 setup_channels out |> init_message; |
94 OuterKeyword.report (); |
94 Keyword.report (); |
95 Output.status (Markup.markup Markup.ready ""); |
95 Output.status (Markup.markup Markup.ready ""); |
96 Isar.toplevel_loop {init = true, welcome = false, sync = true, secure = true}); |
96 Isar.toplevel_loop {init = true, welcome = false, sync = true, secure = true}); |
97 |
97 |
98 end; |
98 end; |