more informative error message from failed goal forks (violating old-style TTY protocol!);
authorwenzelm
Fri Aug 31 15:25:26 2012 +0200 (2012-08-31)
changeset 490419edfd36a0355
parent 49040 e5fc20c93e38
child 49042 01041f7bf9b4
more informative error message from failed goal forks (violating old-style TTY protocol!);
src/Pure/ROOT.ML
src/Pure/goal.ML
     1.1 --- a/src/Pure/ROOT.ML	Fri Aug 31 15:24:26 2012 +0200
     1.2 +++ b/src/Pure/ROOT.ML	Fri Aug 31 15:25:26 2012 +0200
     1.3 @@ -158,11 +158,19 @@
     1.4  use "conjunction.ML";
     1.5  use "assumption.ML";
     1.6  use "display.ML";
     1.7 -use "goal.ML";
     1.8  
     1.9  
    1.10  (* Isar -- Intelligible Semi-Automated Reasoning *)
    1.11  
    1.12 +(*ML support*)
    1.13 +use "ML/ml_syntax.ML";
    1.14 +use "ML/ml_env.ML";
    1.15 +use "Isar/runtime.ML";
    1.16 +use "ML/ml_compiler.ML";
    1.17 +if ML_System.is_polyml then use "ML/ml_compiler_polyml.ML" else ();
    1.18 +
    1.19 +use "goal.ML";
    1.20 +
    1.21  (*proof context*)
    1.22  use "Isar/object_logic.ML";
    1.23  use "Isar/rule_cases.ML";
    1.24 @@ -185,13 +193,6 @@
    1.25  use "Isar/keyword.ML";
    1.26  use "Isar/parse.ML";
    1.27  use "Isar/args.ML";
    1.28 -
    1.29 -(*ML support*)
    1.30 -use "ML/ml_syntax.ML";
    1.31 -use "ML/ml_env.ML";
    1.32 -use "Isar/runtime.ML";
    1.33 -use "ML/ml_compiler.ML";
    1.34 -if ML_System.is_polyml then use "ML/ml_compiler_polyml.ML" else ();
    1.35  use "ML/ml_context.ML";
    1.36  
    1.37  (*theory sources*)
     2.1 --- a/src/Pure/goal.ML	Fri Aug 31 15:24:26 2012 +0200
     2.2 +++ b/src/Pure/goal.ML	Fri Aug 31 15:25:26 2012 +0200
     2.3 @@ -138,10 +138,12 @@
     2.4                val result = Exn.capture (Future.interruptible_task e) ();
     2.5                val _ = status task [Isabelle_Markup.finished, Isabelle_Markup.joined];
     2.6                val _ =
     2.7 -                if is_some (Exn.get_res result) then ()
     2.8 -                else
     2.9 -                  (status task [Isabelle_Markup.failed];
    2.10 -                   Output.report (Markup.markup_only Isabelle_Markup.bad));
    2.11 +                (case result of
    2.12 +                  Exn.Res _ => ()
    2.13 +                | Exn.Exn exn =>
    2.14 +                    (status task [Isabelle_Markup.failed];
    2.15 +                     Output.report (Markup.markup_only Isabelle_Markup.bad);
    2.16 +                     Output.error_msg (ML_Compiler.exn_message exn)));
    2.17              in Exn.release result end);
    2.18        val _ = status (Future.task_of future) [Isabelle_Markup.forked];
    2.19      in future end) ();