# HG changeset patch
# User wenzelm
# Date 1495884035 -7200
# Node ID de7888573ed789f0c54c5340ac43ac885dfef6f5
# Parent  223fd19ac6b36e2c037621d4d5fb9232204d86ed
clarified build errors;
tuned signature;

diff -r 223fd19ac6b3 -r de7888573ed7 src/Pure/Isar/runtime.ML
--- a/src/Pure/Isar/runtime.ML	Sat May 27 13:07:27 2017 +0200
+++ b/src/Pure/Isar/runtime.ML	Sat May 27 13:20:35 2017 +0200
@@ -13,8 +13,8 @@
   val exn_context: Proof.context option -> exn -> exn
   val thread_context: exn -> exn
   type error = ((serial * string) * string option)
-  val exn_messages_ids: exn -> error list
-  val exn_messages: exn -> (serial * string) list
+  val exn_messages: exn -> error list
+  val exn_message_list: exn -> string list
   val exn_message: exn -> string
   val exn_error_message: exn -> unit
   val exn_system_message: exn -> unit
@@ -91,7 +91,7 @@
 
 in
 
-fun exn_messages_ids e =
+fun exn_messages e =
   let
     fun raised exn name msgs =
       let val pos = Position.here (Exn_Properties.position exn) in
@@ -141,12 +141,12 @@
 
 end;
 
-fun exn_messages exn = map #1 (exn_messages_ids exn);
+fun exn_message_list exn =
+  (case exn_messages exn of
+    [] => ["Interrupt"]
+  | msgs => map (#2 o #1) msgs);
 
-fun exn_message exn =
-  (case exn_messages exn of
-    [] => "Interrupt"
-  | msgs => cat_lines (map snd msgs));
+val exn_message = cat_lines o exn_message_list;
 
 val exn_error_message = Output.error_message o exn_message;
 val exn_system_message = Output.system_message o exn_message;
diff -r 223fd19ac6b3 -r de7888573ed7 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Sat May 27 13:07:27 2017 +0200
+++ b/src/Pure/Isar/toplevel.ML	Sat May 27 13:20:35 2017 +0200
@@ -593,7 +593,7 @@
 fun command_errors int tr st =
   (case transition int tr st of
     (st', NONE) => ([], SOME st')
-  | (_, SOME (exn, _)) => (Runtime.exn_messages_ids exn, NONE));
+  | (_, SOME (exn, _)) => (Runtime.exn_messages exn, NONE));
 
 fun command_exception int tr st =
   (case transition int tr st of
diff -r 223fd19ac6b3 -r de7888573ed7 src/Pure/PIDE/command.ML
--- a/src/Pure/PIDE/command.ML	Sat May 27 13:07:27 2017 +0200
+++ b/src/Pure/PIDE/command.ML	Sat May 27 13:20:35 2017 +0200
@@ -201,7 +201,7 @@
         (Thy_Output.output_text st' {markdown = false} (Token.input_of cmt); [])
           handle exn =>
             if Exn.is_interrupt exn then Exn.reraise exn
-            else Runtime.exn_messages_ids exn)) ();
+            else Runtime.exn_messages exn)) ();
 
 fun report tr m =
   Toplevel.setmp_thread_position tr (fn () => Output.report [Markup.markup_only m]) ();
@@ -293,7 +293,7 @@
   (Toplevel.setmp_thread_position tr o Runtime.controlled_execution opt_context) e ()
     handle exn =>
       if Exn.is_interrupt exn then Exn.reraise exn
-      else List.app (Future.error_message (Toplevel.pos_of tr)) (Runtime.exn_messages_ids exn);
+      else List.app (Future.error_message (Toplevel.pos_of tr)) (Runtime.exn_messages exn);
 
 fun print_finished (Print {print_process, ...}) = Lazy.is_finished print_process;
 
diff -r 223fd19ac6b3 -r de7888573ed7 src/Pure/PIDE/execution.ML
--- a/src/Pure/PIDE/execution.ML	Sat May 27 13:07:27 2017 +0200
+++ b/src/Pure/PIDE/execution.ML	Sat May 27 13:20:35 2017 +0200
@@ -118,7 +118,7 @@
                     status task [Markup.finished];
                     Output.report [Markup.markup_only (Markup.bad ())];
                     if exec_id = 0 then ()
-                    else List.app (Future.error_message pos) (Runtime.exn_messages_ids exn))
+                    else List.app (Future.error_message pos) (Runtime.exn_messages exn))
                 | Exn.Res _ =>
                     status task [Markup.finished])
             in Exn.release result end);
diff -r 223fd19ac6b3 -r de7888573ed7 src/Pure/Tools/build.ML
--- a/src/Pure/Tools/build.ML	Sat May 27 13:07:27 2017 +0200
+++ b/src/Pure/Tools/build.ML	Sat May 27 13:20:35 2017 +0200
@@ -225,7 +225,7 @@
     val _ =
       Unsynchronized.setmp Private_Output.protocol_message_fn protocol_message
         build_session args
-      handle exn => (List.app (error_message o #2) (Runtime.exn_messages exn); Exn.reraise exn);
+      handle exn => (List.app error_message (Runtime.exn_message_list exn); Exn.reraise exn);
     val _ = Options.reset_default ();
   in () end;