tuned signature;
authorwenzelm
Wed Jan 16 21:49:56 2013 +0100 (2013-01-16 ago)
changeset 509179459f59cff09
parent 50916 fd902b616b48
child 50918 3b6417e9f73e
tuned signature;
src/Pure/Isar/toplevel.ML
src/Pure/System/isar.ML
     1.1 --- a/src/Pure/Isar/toplevel.ML	Wed Jan 16 21:39:43 2013 +0100
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Wed Jan 16 21:49:56 2013 +0100
     1.3 @@ -88,7 +88,6 @@
     1.4    val unknown_context: transition -> transition
     1.5    val setmp_thread_position: transition -> ('a -> 'b) -> 'a -> 'b
     1.6    val status: transition -> Markup.T -> unit
     1.7 -  val error_msg: transition -> serial * string -> unit
     1.8    val add_hook: (transition -> state -> state -> unit) -> unit
     1.9    val transition: bool -> transition -> state -> (state * (exn * string) option) option
    1.10    val command: transition -> state -> state
    1.11 @@ -596,9 +595,6 @@
    1.12  fun status tr m =
    1.13    setmp_thread_position tr (fn () => Output.status (Markup.markup_only m)) ();
    1.14  
    1.15 -fun error_msg tr msg =
    1.16 -  setmp_thread_position tr (fn () => Output.error_msg' msg) ();
    1.17 -
    1.18  
    1.19  (* post-transition hooks *)
    1.20  
     2.1 --- a/src/Pure/System/isar.ML	Wed Jan 16 21:39:43 2013 +0100
     2.2 +++ b/src/Pure/System/isar.ML	Wed Jan 16 21:49:56 2013 +0100
     2.3 @@ -96,7 +96,8 @@
     2.4      NONE => false
     2.5    | SOME (_, SOME exn_info) =>
     2.6       (set_exn (SOME exn_info);
     2.7 -      Toplevel.error_msg tr (serial (), ML_Compiler.exn_message (Runtime.EXCURSION_FAIL exn_info));
     2.8 +      Toplevel.setmp_thread_position tr
     2.9 +        Output.error_msg' (serial (), ML_Compiler.exn_message (Runtime.EXCURSION_FAIL exn_info));
    2.10        true)
    2.11    | SOME (st', NONE) =>
    2.12        let