ML_Compiler.exn_message;
authorwenzelm
Sat, 06 Jun 2009 21:11:23 +0200
changeset 314785e412e4c6546
parent 31477 ae1a00e1a2f6
child 31479 08e2a70d002a
ML_Compiler.exn_message;
src/Pure/ProofGeneral/proof_general_pgip.ML
src/Pure/System/isar.ML
src/Pure/System/session.ML
     1.1 --- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Sat Jun 06 21:11:23 2009 +0200
     1.2 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Sat Jun 06 21:11:23 2009 +0200
     1.3 @@ -1000,7 +1000,7 @@
     1.4        | (Toplevel.UNDEF,SOME src) =>
     1.5          (Output.error_msg "No working context defined"; loop true src)
     1.6        | (e,SOME src) =>
     1.7 -        (Output.error_msg (Toplevel.exn_message e); loop true src)
     1.8 +        (Output.error_msg (ML_Compiler.exn_message e); loop true src)
     1.9        | (PGIP_QUIT,_) => ()
    1.10        | (_,NONE) => ()
    1.11  in
     2.1 --- a/src/Pure/System/isar.ML	Sat Jun 06 21:11:23 2009 +0200
     2.2 +++ b/src/Pure/System/isar.ML	Sat Jun 06 21:11:23 2009 +0200
     2.3 @@ -134,7 +134,7 @@
     2.4        NONE => if secure then quit () else ()
     2.5      | SOME (tr, src') => if op >> tr orelse check_secure () then raw_loop secure src' else ())
     2.6      handle exn =>
     2.7 -      (Output.error_msg (Toplevel.exn_message exn)
     2.8 +      (Output.error_msg (ML_Compiler.exn_message exn)
     2.9          handle crash =>
    2.10            (CRITICAL (fn () => change crashes (cons crash));
    2.11              warning "Recovering from Isar toplevel crash -- see also Isar.crashes");
     3.1 --- a/src/Pure/System/session.ML	Sat Jun 06 21:11:23 2009 +0200
     3.2 +++ b/src/Pure/System/session.ML	Sat Jun 06 21:11:23 2009 +0200
     3.3 @@ -107,6 +107,6 @@
     3.4      |> setmp_noncritical Multithreading.max_threads
     3.5        (if Multithreading.available then max_threads
     3.6         else (if max_threads = 1 then () else warning "Multithreading support unavailable"; 1))) ()
     3.7 -  handle exn => (Output.error_msg (Toplevel.exn_message exn); exit 1);
     3.8 +  handle exn => (Output.error_msg (ML_Compiler.exn_message exn); exit 1);
     3.9  
    3.10  end;