run_thy: removed Output.toplevel_errors;
authorwenzelm
Thu Jan 19 21:22:22 2006 +0100 (2006-01-19)
changeset 187176261fcfaca1d
parent 18716 bb4af2bdd17b
child 18718 d01837224eaf
run_thy: removed Output.toplevel_errors;
src/Pure/Isar/outer_syntax.ML
     1.1 --- a/src/Pure/Isar/outer_syntax.ML	Thu Jan 19 21:22:21 2006 +0100
     1.2 +++ b/src/Pure/Isar/outer_syntax.ML	Thu Jan 19 21:22:22 2006 +0100
     1.3 @@ -272,7 +272,7 @@
     1.4      else Toplevel.excursion [Toplevel.empty |> Toplevel.name tr_name |> tr]
     1.5    end;
     1.6  
     1.7 -fun run_thy name path = Output.toplevel_errors (fn () =>
     1.8 +fun run_thy name path =
     1.9    let
    1.10      val text = Source.of_list (Library.untabify (explode (File.read path)));
    1.11      val _ = Present.init_theory name;
    1.12 @@ -288,7 +288,7 @@
    1.13      IsarOutput.present_thy (#1 (get_lexicons ())) command_tags is_markup trs toks
    1.14      |> Buffer.content
    1.15      |> Present.theory_output name
    1.16 -  end) ();
    1.17 +  end;
    1.18  
    1.19  in
    1.20