# HG changeset patch
# User wenzelm
# Date 1346419526 -7200
# Node ID 9edfd36a035521f25d2f095712403a403da6b264
# Parent  e5fc20c93e38722883762b82c52c88ed6fdbc957
more informative error message from failed goal forks (violating old-style TTY protocol!);

diff -r e5fc20c93e38 -r 9edfd36a0355 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Fri Aug 31 15:24:26 2012 +0200
+++ b/src/Pure/ROOT.ML	Fri Aug 31 15:25:26 2012 +0200
@@ -158,11 +158,19 @@
 use "conjunction.ML";
 use "assumption.ML";
 use "display.ML";
-use "goal.ML";
 
 
 (* Isar -- Intelligible Semi-Automated Reasoning *)
 
+(*ML support*)
+use "ML/ml_syntax.ML";
+use "ML/ml_env.ML";
+use "Isar/runtime.ML";
+use "ML/ml_compiler.ML";
+if ML_System.is_polyml then use "ML/ml_compiler_polyml.ML" else ();
+
+use "goal.ML";
+
 (*proof context*)
 use "Isar/object_logic.ML";
 use "Isar/rule_cases.ML";
@@ -185,13 +193,6 @@
 use "Isar/keyword.ML";
 use "Isar/parse.ML";
 use "Isar/args.ML";
-
-(*ML support*)
-use "ML/ml_syntax.ML";
-use "ML/ml_env.ML";
-use "Isar/runtime.ML";
-use "ML/ml_compiler.ML";
-if ML_System.is_polyml then use "ML/ml_compiler_polyml.ML" else ();
 use "ML/ml_context.ML";
 
 (*theory sources*)
diff -r e5fc20c93e38 -r 9edfd36a0355 src/Pure/goal.ML
--- a/src/Pure/goal.ML	Fri Aug 31 15:24:26 2012 +0200
+++ b/src/Pure/goal.ML	Fri Aug 31 15:25:26 2012 +0200
@@ -138,10 +138,12 @@
               val result = Exn.capture (Future.interruptible_task e) ();
               val _ = status task [Isabelle_Markup.finished, Isabelle_Markup.joined];
               val _ =
-                if is_some (Exn.get_res result) then ()
-                else
-                  (status task [Isabelle_Markup.failed];
-                   Output.report (Markup.markup_only Isabelle_Markup.bad));
+                (case result of
+                  Exn.Res _ => ()
+                | Exn.Exn exn =>
+                    (status task [Isabelle_Markup.failed];
+                     Output.report (Markup.markup_only Isabelle_Markup.bad);
+                     Output.error_msg (ML_Compiler.exn_message exn)));
             in Exn.release result end);
       val _ = status (Future.task_of future) [Isabelle_Markup.forked];
     in future end) ();