# HG changeset patch # User wenzelm # Date 1358369396 -3600 # Node ID 9459f59cff0941bda98790ff3ca9afae392dc07b # Parent fd902b616b4869824c11f6cd7b825f2c590a2593 tuned signature; diff -r fd902b616b48 -r 9459f59cff09 src/Pure/Isar/toplevel.ML --- a/src/Pure/Isar/toplevel.ML Wed Jan 16 21:39:43 2013 +0100 +++ b/src/Pure/Isar/toplevel.ML Wed Jan 16 21:49:56 2013 +0100 @@ -88,7 +88,6 @@ val unknown_context: transition -> transition val setmp_thread_position: transition -> ('a -> 'b) -> 'a -> 'b val status: transition -> Markup.T -> unit - val error_msg: transition -> serial * string -> unit val add_hook: (transition -> state -> state -> unit) -> unit val transition: bool -> transition -> state -> (state * (exn * string) option) option val command: transition -> state -> state @@ -596,9 +595,6 @@ fun status tr m = setmp_thread_position tr (fn () => Output.status (Markup.markup_only m)) (); -fun error_msg tr msg = - setmp_thread_position tr (fn () => Output.error_msg' msg) (); - (* post-transition hooks *) diff -r fd902b616b48 -r 9459f59cff09 src/Pure/System/isar.ML --- a/src/Pure/System/isar.ML Wed Jan 16 21:39:43 2013 +0100 +++ b/src/Pure/System/isar.ML Wed Jan 16 21:49:56 2013 +0100 @@ -96,7 +96,8 @@ NONE => false | SOME (_, SOME exn_info) => (set_exn (SOME exn_info); - Toplevel.error_msg tr (serial (), ML_Compiler.exn_message (Runtime.EXCURSION_FAIL exn_info)); + Toplevel.setmp_thread_position tr + Output.error_msg' (serial (), ML_Compiler.exn_message (Runtime.EXCURSION_FAIL exn_info)); true) | SOME (st', NONE) => let