# HG changeset patch
# User wenzelm
# Date 1137255256 -3600
# Node ID a8f9c192f6d1d81c825e0e326c6855bdeff62a18
# Parent  216692feebab68c0e6b411737c3f52ec4bfdc76b
Output.error_msg;

diff -r 216692feebab -r a8f9c192f6d1 src/Pure/General/scan.ML
--- a/src/Pure/General/scan.ML	Sat Jan 14 17:14:15 2006 +0100
+++ b/src/Pure/General/scan.ML	Sat Jan 14 17:14:16 2006 +0100
@@ -243,7 +243,7 @@
 fun force scan xs = scan xs handle MORE _ => raise FAIL NONE;
 fun prompt str scan xs = scan xs handle MORE NONE => raise MORE (SOME str);
 fun catch scan xs = scan xs handle ABORT msg => raise FAIL (SOME msg);
-fun error scan xs = scan xs handle ABORT msg => Output.error msg;
+fun error scan xs = scan xs handle ABORT msg => Library.error msg;
 
 
 (* finite scans *)
@@ -284,7 +284,7 @@
 
     fun drain_loop recover inp =
       drain_with (catch scanner) inp handle FAIL msg =>
-        (error_msg (if_none msg "Syntax error."); drain_with recover inp);
+        (Output.error_msg (if_none msg "Syntax error."); drain_with recover inp);
 
     val ((ys, (state', xs')), src') =
       (case (get def_prmpt src, opt_recover) of
diff -r 216692feebab -r a8f9c192f6d1 src/Pure/Isar/session.ML
--- a/src/Pure/Isar/session.ML	Sat Jan 14 17:14:15 2006 +0100
+++ b/src/Pure/Isar/session.ML	Sat Jan 14 17:14:16 2006 +0100
@@ -86,7 +86,7 @@
          (dumping dump) (get_rpath rpath) verbose;
        ThyInfo.time_use root;
        finish ()))) ()
-  handle exn => (writeln (Toplevel.exn_message exn); exit 1);
+  handle exn => (Output.error_msg (Toplevel.exn_message exn); exit 1);
 
 
 end;