# HG changeset patch # User wenzelm # Date 1137702142 -3600 # Node ID 6261fcfaca1d18dad66debe3708c46ea1f9c5f63 # Parent bb4af2bdd17bd2aa36ae0836d4163ca6fd7be0ee run_thy: removed Output.toplevel_errors; diff -r bb4af2bdd17b -r 6261fcfaca1d src/Pure/Isar/outer_syntax.ML --- a/src/Pure/Isar/outer_syntax.ML Thu Jan 19 21:22:21 2006 +0100 +++ b/src/Pure/Isar/outer_syntax.ML Thu Jan 19 21:22:22 2006 +0100 @@ -272,7 +272,7 @@ else Toplevel.excursion [Toplevel.empty |> Toplevel.name tr_name |> tr] end; -fun run_thy name path = Output.toplevel_errors (fn () => +fun run_thy name path = let val text = Source.of_list (Library.untabify (explode (File.read path))); val _ = Present.init_theory name; @@ -288,7 +288,7 @@ IsarOutput.present_thy (#1 (get_lexicons ())) command_tags is_markup trs toks |> Buffer.content |> Present.theory_output name - end) (); + end; in