Output.error_msg;
authorwenzelm
Sat Jan 14 17:14:16 2006 +0100 (2006-01-14)
changeset 18683a8f9c192f6d1
parent 18682 216692feebab
child 18684 38d72231b41d
Output.error_msg;
src/Pure/General/scan.ML
src/Pure/Isar/session.ML
     1.1 --- a/src/Pure/General/scan.ML	Sat Jan 14 17:14:15 2006 +0100
     1.2 +++ b/src/Pure/General/scan.ML	Sat Jan 14 17:14:16 2006 +0100
     1.3 @@ -243,7 +243,7 @@
     1.4  fun force scan xs = scan xs handle MORE _ => raise FAIL NONE;
     1.5  fun prompt str scan xs = scan xs handle MORE NONE => raise MORE (SOME str);
     1.6  fun catch scan xs = scan xs handle ABORT msg => raise FAIL (SOME msg);
     1.7 -fun error scan xs = scan xs handle ABORT msg => Output.error msg;
     1.8 +fun error scan xs = scan xs handle ABORT msg => Library.error msg;
     1.9  
    1.10  
    1.11  (* finite scans *)
    1.12 @@ -284,7 +284,7 @@
    1.13  
    1.14      fun drain_loop recover inp =
    1.15        drain_with (catch scanner) inp handle FAIL msg =>
    1.16 -        (error_msg (if_none msg "Syntax error."); drain_with recover inp);
    1.17 +        (Output.error_msg (if_none msg "Syntax error."); drain_with recover inp);
    1.18  
    1.19      val ((ys, (state', xs')), src') =
    1.20        (case (get def_prmpt src, opt_recover) of
     2.1 --- a/src/Pure/Isar/session.ML	Sat Jan 14 17:14:15 2006 +0100
     2.2 +++ b/src/Pure/Isar/session.ML	Sat Jan 14 17:14:16 2006 +0100
     2.3 @@ -86,7 +86,7 @@
     2.4           (dumping dump) (get_rpath rpath) verbose;
     2.5         ThyInfo.time_use root;
     2.6         finish ()))) ()
     2.7 -  handle exn => (writeln (Toplevel.exn_message exn); exit 1);
     2.8 +  handle exn => (Output.error_msg (Toplevel.exn_message exn); exit 1);
     2.9  
    2.10  
    2.11  end;