more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
authorwenzelm
Thu Sep 09 17:20:27 2010 +0200 (2010-09-09 ago)
changeset 3923269c6d3e87660
parent 39231 25c345302a17
child 39233 9a0c67d4517a
more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
src/HOL/Mirabelle/Tools/mirabelle.ML
src/Pure/Concurrent/future.ML
src/Pure/Concurrent/lazy.ML
src/Pure/Concurrent/lazy_sequential.ML
src/Pure/Concurrent/simple_thread.ML
src/Pure/Concurrent/task_queue.ML
src/Pure/General/basics.ML
src/Pure/General/exn.ML
src/Pure/Isar/proof.ML
src/Pure/Isar/runtime.ML
src/Pure/Isar/toplevel.ML
src/Pure/ML-Systems/multithreading_polyml.ML
src/Pure/ML-Systems/smlnj.ML
src/Pure/ML/ml_compiler_polyml-5.3.ML
src/Pure/PIDE/document.ML
src/Pure/ProofGeneral/proof_general_pgip.ML
     1.1 --- a/src/HOL/Mirabelle/Tools/mirabelle.ML	Thu Sep 09 11:05:52 2010 +0200
     1.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle.ML	Thu Sep 09 17:20:27 2010 +0200
     1.3 @@ -73,12 +73,12 @@
     1.4  fun log_exn log tag id e = log (tag id ^ "exception:\n" ^ General.exnMessage e)
     1.5  
     1.6  fun catch tag f id (st as {log, ...}: run_args) = (f id st; ())
     1.7 -  handle (exn as Exn.Interrupt) => reraise exn
     1.8 -       | exn => (log_exn log tag id exn; ())
     1.9 +  handle exn =>
    1.10 +    if Exn.is_interrupt exn then reraise exn else (log_exn log tag id exn; ())
    1.11  
    1.12  fun catch_result tag d f id (st as {log, ...}: run_args) = f id st
    1.13 -  handle (exn as Exn.Interrupt) => reraise exn
    1.14 -       | exn => (log_exn log tag id exn; d)
    1.15 +  handle exn =>
    1.16 +    if Exn.is_interrupt exn then reraise exn else (log_exn log tag id exn; d)
    1.17  
    1.18  fun register (init, run, done) thy =
    1.19    let val id = length (Actions.get thy) + 1
     2.1 --- a/src/Pure/Concurrent/future.ML	Thu Sep 09 11:05:52 2010 +0200
     2.2 +++ b/src/Pure/Concurrent/future.ML	Thu Sep 09 17:20:27 2010 +0200
     2.3 @@ -110,7 +110,7 @@
     2.4      val _ = Single_Assignment.assign result res
     2.5        handle exn as Fail _ =>
     2.6          (case Single_Assignment.peek result of
     2.7 -          SOME (Exn.Exn Exn.Interrupt) => raise Exn.Interrupt
     2.8 +          SOME (Exn.Exn e) => reraise (if Exn.is_interrupt e then e else exn)
     2.9          | _ => reraise exn);
    2.10      val ok =
    2.11        (case the (Single_Assignment.peek result) of
    2.12 @@ -184,7 +184,7 @@
    2.13              Exn.capture (fn () =>
    2.14                Multithreading.with_attributes Multithreading.private_interrupts
    2.15                  (fn _ => Position.setmp_thread_data pos e ())) ()
    2.16 -          else Exn.Exn Exn.Interrupt;
    2.17 +          else Exn.interrupt_exn;
    2.18        in assign_result group result res end;
    2.19    in (result, job) end;
    2.20  
    2.21 @@ -359,10 +359,12 @@
    2.22  
    2.23      val _ = broadcast scheduler_event;
    2.24    in continue end
    2.25 -  handle Exn.Interrupt =>
    2.26 -   (Multithreading.tracing 1 (fn () => "Interrupt");
    2.27 -    List.app cancel_later (Task_Queue.cancel_all (! queue));
    2.28 -    broadcast_work (); true);
    2.29 +  handle exn =>
    2.30 +    if Exn.is_interrupt exn then
    2.31 +     (Multithreading.tracing 1 (fn () => "Interrupt");
    2.32 +      List.app cancel_later (Task_Queue.cancel_all (! queue));
    2.33 +      broadcast_work (); true)
    2.34 +    else reraise exn;
    2.35  
    2.36  fun scheduler_loop () =
    2.37    while
    2.38 @@ -415,11 +417,12 @@
    2.39  fun get_result x =
    2.40    (case peek x of
    2.41      NONE => Exn.Exn (Fail "Unfinished future")
    2.42 -  | SOME (exn as Exn.Exn Exn.Interrupt) =>
    2.43 -      (case Exn.flatten_list (Task_Queue.group_status (group_of x)) of
    2.44 -        [] => exn
    2.45 -      | exns => Exn.Exn (Exn.EXCEPTIONS exns))
    2.46 -  | SOME res => res);
    2.47 +  | SOME res =>
    2.48 +      if Exn.is_interrupt_exn res then
    2.49 +        (case Exn.flatten_list (Task_Queue.group_status (group_of x)) of
    2.50 +          [] => res
    2.51 +        | exns => Exn.Exn (Exn.EXCEPTIONS exns))
    2.52 +      else res);
    2.53  
    2.54  fun join_next deps = (*requires SYNCHRONIZED*)
    2.55    if null deps then NONE
    2.56 @@ -486,7 +489,7 @@
    2.57  fun promise_group group : 'a future =
    2.58    let
    2.59      val result = Single_Assignment.var "promise" : 'a result;
    2.60 -    fun abort () = assign_result group result (Exn.Exn Exn.Interrupt) handle Fail _ => true;
    2.61 +    fun abort () = assign_result group result Exn.interrupt_exn handle Fail _ => true;
    2.62      val task = SYNCHRONIZED "enqueue_passive" (fn () =>
    2.63        Unsynchronized.change_result queue (Task_Queue.enqueue_passive group abort));
    2.64    in Future {promised = true, task = task, group = group, result = result} end;
    2.65 @@ -496,7 +499,7 @@
    2.66  fun fulfill_result (Future {promised, task, group, result}) res =
    2.67    let
    2.68      val _ = promised orelse raise Fail "Not a promised future";
    2.69 -    fun job ok = assign_result group result (if ok then res else Exn.Exn Exn.Interrupt);
    2.70 +    fun job ok = assign_result group result (if ok then res else Exn.interrupt_exn);
    2.71      val _ = execute (task, group, [job]);
    2.72    in () end;
    2.73  
     3.1 --- a/src/Pure/Concurrent/lazy.ML	Thu Sep 09 11:05:52 2010 +0200
     3.2 +++ b/src/Pure/Concurrent/lazy.ML	Thu Sep 09 17:20:27 2010 +0200
     3.3 @@ -60,9 +60,9 @@
     3.4                  (*semantic race: some other threads might see the same
     3.5                    Interrupt, until there is a fresh start*)
     3.6                  val _ =
     3.7 -                  (case res of
     3.8 -                    Exn.Exn Exn.Interrupt => Synchronized.change var (fn _ => Expr e)
     3.9 -                  | _ => ());
    3.10 +                  if Exn.is_interrupt_exn res then
    3.11 +                    Synchronized.change var (fn _ => Expr e)
    3.12 +                  else ();
    3.13                in res end
    3.14            | NONE => restore_interrupts (fn () => Future.join_result x) ())
    3.15          end) ());
     4.1 --- a/src/Pure/Concurrent/lazy_sequential.ML	Thu Sep 09 11:05:52 2010 +0200
     4.2 +++ b/src/Pure/Concurrent/lazy_sequential.ML	Thu Sep 09 17:20:27 2010 +0200
     4.3 @@ -34,10 +34,7 @@
     4.4        (case ! r of
     4.5          Expr e => Exn.capture e ()
     4.6        | Result res => res);
     4.7 -    val _ =
     4.8 -      (case result of
     4.9 -        Exn.Exn Exn.Interrupt => ()
    4.10 -      | _ => r := Result result);
    4.11 +    val _ = if Exn.is_interrupt_exn result then () else r := Result result;
    4.12    in result end;
    4.13  
    4.14  fun force r = Exn.release (force_result r);
     5.1 --- a/src/Pure/Concurrent/simple_thread.ML	Thu Sep 09 11:05:52 2010 +0200
     5.2 +++ b/src/Pure/Concurrent/simple_thread.ML	Thu Sep 09 17:20:27 2010 +0200
     5.3 @@ -19,7 +19,9 @@
     5.4    if interrupts then Multithreading.public_interrupts else Multithreading.no_interrupts;
     5.5  
     5.6  fun fork interrupts body =
     5.7 -  Thread.fork (fn () => exception_trace (fn () => body () handle Exn.Interrupt => ()),
     5.8 +  Thread.fork (fn () =>
     5.9 +    exception_trace (fn () =>
    5.10 +      body () handle exn => if Exn.is_interrupt exn then () else reraise exn),
    5.11      attributes interrupts);
    5.12  
    5.13  fun interrupt thread = Thread.interrupt thread handle Thread _ => ();
     6.1 --- a/src/Pure/Concurrent/task_queue.ML	Thu Sep 09 11:05:52 2010 +0200
     6.2 +++ b/src/Pure/Concurrent/task_queue.ML	Thu Sep 09 17:20:27 2010 +0200
     6.3 @@ -80,9 +80,8 @@
     6.4  fun cancel_group (Group {status, ...}) exn =
     6.5    Synchronized.change status
     6.6      (fn exns =>
     6.7 -      (case exn of
     6.8 -        Exn.Interrupt => if null exns then [exn] else exns
     6.9 -      | _ => exn :: exns));
    6.10 +      if not (Exn.is_interrupt exn) orelse null exns then exn :: exns
    6.11 +      else exns);
    6.12  
    6.13  fun is_canceled (Group {parent, status, ...}) =
    6.14    not (null (Synchronized.value status)) orelse
     7.1 --- a/src/Pure/General/basics.ML	Thu Sep 09 11:05:52 2010 +0200
     7.2 +++ b/src/Pure/General/basics.ML	Thu Sep 09 17:20:27 2010 +0200
     7.3 @@ -94,7 +94,7 @@
     7.4  (* partiality *)
     7.5  
     7.6  fun try f x = SOME (f x)
     7.7 -  handle (exn as Exn.Interrupt) => reraise exn | _ => NONE;
     7.8 +  handle exn => if Exn.is_interrupt exn then reraise exn else NONE;
     7.9  
    7.10  fun can f x = is_some (try f x);
    7.11  
     8.1 --- a/src/Pure/General/exn.ML	Thu Sep 09 11:05:52 2010 +0200
     8.2 +++ b/src/Pure/General/exn.ML	Thu Sep 09 17:20:27 2010 +0200
     8.3 @@ -12,6 +12,10 @@
     8.4    val capture: ('a -> 'b) -> 'a -> 'b result
     8.5    val release: 'a result -> 'a
     8.6    exception Interrupt
     8.7 +  val interrupt: unit -> 'a
     8.8 +  val is_interrupt: exn -> bool
     8.9 +  val interrupt_exn: 'a result
    8.10 +  val is_interrupt_exn: 'a result -> bool
    8.11    exception EXCEPTIONS of exn list
    8.12    val flatten: exn -> exn list
    8.13    val flatten_list: exn list -> exn list
    8.14 @@ -40,14 +44,27 @@
    8.15    | release (Exn e) = reraise e;
    8.16  
    8.17  
    8.18 -(* interrupt and nested exceptions *)
    8.19 +(* interrupts *)
    8.20  
    8.21  exception Interrupt = Interrupt;
    8.22 +
    8.23 +fun interrupt () = raise Interrupt;
    8.24 +
    8.25 +fun is_interrupt Interrupt = true
    8.26 +  | is_interrupt _ = false;
    8.27 +
    8.28 +val interrupt_exn = Exn Interrupt;
    8.29 +
    8.30 +fun is_interrupt_exn (Exn exn) = is_interrupt exn
    8.31 +  | is_interrupt_exn _ = false;
    8.32 +
    8.33 +
    8.34 +(* nested exceptions *)
    8.35 +
    8.36  exception EXCEPTIONS of exn list;
    8.37  
    8.38 -fun flatten Interrupt = []
    8.39 -  | flatten (EXCEPTIONS exns) = flatten_list exns
    8.40 -  | flatten exn = [exn]
    8.41 +fun flatten (EXCEPTIONS exns) = flatten_list exns
    8.42 +  | flatten exn = if is_interrupt exn then [] else [exn]
    8.43  and flatten_list exns = List.concat (map flatten exns);
    8.44  
    8.45  fun release_all results =
     9.1 --- a/src/Pure/Isar/proof.ML	Thu Sep 09 11:05:52 2010 +0200
     9.2 +++ b/src/Pure/Isar/proof.ML	Thu Sep 09 17:20:27 2010 +0200
     9.3 @@ -990,8 +990,9 @@
     9.4        (case test_proof goal_state of
     9.5          Exn.Result (SOME _) => goal_state
     9.6        | Exn.Result NONE => error (fail_msg (context_of goal_state))
     9.7 -      | Exn.Exn Exn.Interrupt => raise Exn.Interrupt
     9.8 -      | Exn.Exn exn => raise Exn.EXCEPTIONS ([exn, ERROR (fail_msg (context_of goal_state))])))
     9.9 +      | Exn.Exn exn =>
    9.10 +          if Exn.is_interrupt exn then reraise exn
    9.11 +          else raise Exn.EXCEPTIONS ([exn, ERROR (fail_msg (context_of goal_state))])))
    9.12    end;
    9.13  
    9.14  in
    10.1 --- a/src/Pure/Isar/runtime.ML	Thu Sep 09 11:05:52 2010 +0200
    10.2 +++ b/src/Pure/Isar/runtime.ML	Thu Sep 09 17:20:27 2010 +0200
    10.3 @@ -54,30 +54,38 @@
    10.4  
    10.5      val detailed = ! Output.debugging;
    10.6  
    10.7 -    fun exn_msgs _ (CONTEXT (ctxt, exn)) = exn_msgs (SOME ctxt) exn
    10.8 -      | exn_msgs ctxt (Exn.EXCEPTIONS exns) = maps (exn_msgs ctxt) exns
    10.9 -      | exn_msgs ctxt (EXCURSION_FAIL (exn, loc)) =
   10.10 -          map (fn msg => msg ^ Markup.markup Markup.location ("\n" ^ loc)) (exn_msgs ctxt exn)
   10.11 -      | exn_msgs _ TERMINATE = ["Exit"]
   10.12 -      | exn_msgs _ Exn.Interrupt = []
   10.13 -      | exn_msgs _ TimeLimit.TimeOut = ["Timeout"]
   10.14 -      | exn_msgs _ TOPLEVEL_ERROR = ["Error"]
   10.15 -      | exn_msgs _ (SYS_ERROR msg) = ["## SYSTEM ERROR ##\n" ^ msg]
   10.16 -      | exn_msgs _ (ERROR msg) = [msg]
   10.17 -      | exn_msgs _ (exn as Fail msg) = [raised exn "Fail" [msg]]
   10.18 -      | exn_msgs _ (exn as THEORY (msg, thys)) =
   10.19 -          [raised exn "THEORY" (msg :: (if detailed then map Context.str_of_thy thys else []))]
   10.20 -      | exn_msgs _ (exn as Syntax.AST (msg, asts)) = [raised exn "AST" (msg ::
   10.21 -            (if detailed then map (Pretty.string_of o Syntax.pretty_ast) asts else []))]
   10.22 -      | exn_msgs ctxt (exn as TYPE (msg, Ts, ts)) = [raised exn "TYPE" (msg ::
   10.23 -            (if detailed then
   10.24 -              if_context ctxt Syntax.string_of_typ Ts @ if_context ctxt Syntax.string_of_term ts
   10.25 -             else []))]
   10.26 -      | exn_msgs ctxt (exn as TERM (msg, ts)) = [raised exn "TERM" (msg ::
   10.27 -            (if detailed then if_context ctxt Syntax.string_of_term ts else []))]
   10.28 -      | exn_msgs ctxt (exn as THM (msg, i, thms)) = [raised exn ("THM " ^ string_of_int i) (msg ::
   10.29 -            (if detailed then if_context ctxt Display.string_of_thm thms else []))]
   10.30 -      | exn_msgs _ exn = [raised exn (General.exnMessage exn) []];
   10.31 +    fun exn_msgs context exn =
   10.32 +      if Exn.is_interrupt exn then []
   10.33 +      else
   10.34 +        (case exn of
   10.35 +          Exn.EXCEPTIONS exns => maps (exn_msgs context) exns
   10.36 +        | CONTEXT (ctxt, exn) => exn_msgs (SOME ctxt) exn
   10.37 +        | EXCURSION_FAIL (exn, loc) =>
   10.38 +            map (fn msg => msg ^ Markup.markup Markup.location ("\n" ^ loc)) (exn_msgs context exn)
   10.39 +        | TERMINATE => ["Exit"]
   10.40 +        | TimeLimit.TimeOut => ["Timeout"]
   10.41 +        | TOPLEVEL_ERROR => ["Error"]
   10.42 +        | SYS_ERROR msg => ["## SYSTEM ERROR ##\n" ^ msg]
   10.43 +        | ERROR msg => [msg]
   10.44 +        | Fail msg => [raised exn "Fail" [msg]]
   10.45 +        | THEORY (msg, thys) =>
   10.46 +            [raised exn "THEORY" (msg :: (if detailed then map Context.str_of_thy thys else []))]
   10.47 +        | Syntax.AST (msg, asts) =>
   10.48 +            [raised exn "AST" (msg ::
   10.49 +              (if detailed then map (Pretty.string_of o Syntax.pretty_ast) asts else []))]
   10.50 +        | TYPE (msg, Ts, ts) =>
   10.51 +            [raised exn "TYPE" (msg ::
   10.52 +              (if detailed then
   10.53 +                if_context context Syntax.string_of_typ Ts @
   10.54 +                if_context context Syntax.string_of_term ts
   10.55 +               else []))]
   10.56 +        | TERM (msg, ts) =>
   10.57 +            [raised exn "TERM" (msg ::
   10.58 +              (if detailed then if_context context Syntax.string_of_term ts else []))]
   10.59 +        | THM (msg, i, thms) =>
   10.60 +            [raised exn ("THM " ^ string_of_int i) (msg ::
   10.61 +              (if detailed then if_context context Display.string_of_thm thms else []))]
   10.62 +        | _ => [raised exn (General.exnMessage exn) []]);
   10.63    in exn_msgs NONE e end;
   10.64  
   10.65  fun exn_message exn_position exn =
    11.1 --- a/src/Pure/Isar/toplevel.ML	Thu Sep 09 11:05:52 2010 +0200
    11.2 +++ b/src/Pure/Isar/toplevel.ML	Thu Sep 09 17:20:27 2010 +0200
    11.3 @@ -231,7 +231,7 @@
    11.4  
    11.5  fun thread interrupts body =
    11.6    Thread.fork
    11.7 -    (((fn () => body () handle Exn.Interrupt => ())
    11.8 +    (((fn () => body () handle exn => if Exn.is_interrupt exn then () else reraise exn)
    11.9          |> Runtime.debugging
   11.10          |> Runtime.toplevel_error
   11.11            (fn exn => priority ("## INTERNAL ERROR ##\n" ^ ML_Compiler.exn_message exn))),
    12.1 --- a/src/Pure/ML-Systems/multithreading_polyml.ML	Thu Sep 09 11:05:52 2010 +0200
    12.2 +++ b/src/Pure/ML-Systems/multithreading_polyml.ML	Thu Sep 09 17:20:27 2010 +0200
    12.3 @@ -148,7 +148,7 @@
    12.4        (OS.Process.sleep time; timeout := true; Thread.interrupt worker), []);
    12.5  
    12.6      val result = Exn.capture (restore_attributes f) x;
    12.7 -    val was_timeout = (case result of Exn.Exn Exn.Interrupt => ! timeout | _ => false);
    12.8 +    val was_timeout = Exn.is_interrupt_exn result andalso ! timeout;
    12.9  
   12.10      val _ = Thread.interrupt watchdog handle Thread _ => ();
   12.11    in if was_timeout then raise TimeOut else Exn.release result end) ();
   12.12 @@ -209,7 +209,7 @@
   12.13          let val res =
   12.14            sync_wait (SOME orig_atts)
   12.15              (SOME (Time.+ (Time.now (), Time.fromMilliseconds 100))) cond lock
   12.16 -        in case res of Exn.Exn Exn.Interrupt => kill 10 | _ => () end;
   12.17 +        in if Exn.is_interrupt_exn res then kill 10 else () end;
   12.18  
   12.19      (*cleanup*)
   12.20      val output = read_file output_name handle IO.Io _ => "";
   12.21 @@ -217,7 +217,7 @@
   12.22      val _ = OS.FileSys.remove pid_name handle OS.SysErr _ => ();
   12.23      val _ = OS.FileSys.remove output_name handle OS.SysErr _ => ();
   12.24      val _ = Thread.interrupt system_thread handle Thread _ => ();
   12.25 -    val rc = (case ! result of Signal => raise Exn.Interrupt | Result rc => rc);
   12.26 +    val rc = (case ! result of Signal => Exn.interrupt () | Result rc => rc);
   12.27    in (output, rc) end);
   12.28  
   12.29  
    13.1 --- a/src/Pure/ML-Systems/smlnj.ML	Thu Sep 09 11:05:52 2010 +0200
    13.2 +++ b/src/Pure/ML-Systems/smlnj.ML	Thu Sep 09 17:20:27 2010 +0200
    13.3 @@ -142,7 +142,7 @@
    13.4  
    13.5  fun interruptible (f: 'a -> 'b) x =
    13.6    let
    13.7 -    val result = ref (Exn.Exn Interrupt: 'b Exn.result);
    13.8 +    val result = ref (Exn.interrupt_exn: 'b Exn.result);
    13.9      val old_handler = Signals.inqHandler Signals.sigINT;
   13.10    in
   13.11      SMLofNJ.Cont.callcc (fn cont =>
   13.12 @@ -165,7 +165,7 @@
   13.13  struct
   13.14    open TextIO;
   13.15    fun inputLine is = TextIO.inputLine is
   13.16 -    handle IO.Io _ => raise Interrupt;
   13.17 +    handle IO.Io _ => Exn.interrupt ();
   13.18  end;
   13.19  
   13.20  
    14.1 --- a/src/Pure/ML/ml_compiler_polyml-5.3.ML	Thu Sep 09 11:05:52 2010 +0200
    14.2 +++ b/src/Pure/ML/ml_compiler_polyml-5.3.ML	Thu Sep 09 17:20:27 2010 +0200
    14.3 @@ -186,17 +186,18 @@
    14.4      val _ =
    14.5        (while not (List.null (! input_buffer)) do
    14.6          PolyML.compiler (get, parameters) ())
    14.7 -      handle exn as Exn.Interrupt => reraise exn
    14.8 -        | exn =>
    14.9 -            let
   14.10 -              val exn_msg =
   14.11 -                (case exn of
   14.12 -                  STATIC_ERRORS () => ""
   14.13 -                | Runtime.TOPLEVEL_ERROR => ""
   14.14 -                | _ => "Exception- " ^ General.exnMessage exn ^ " raised");
   14.15 -              val _ = output_warnings ();
   14.16 -              val _ = output_writeln ();
   14.17 -            in raise_error exn_msg end;
   14.18 +      handle exn =>
   14.19 +        if Exn.is_interrupt exn then reraise exn
   14.20 +        else
   14.21 +          let
   14.22 +            val exn_msg =
   14.23 +              (case exn of
   14.24 +                STATIC_ERRORS () => ""
   14.25 +              | Runtime.TOPLEVEL_ERROR => ""
   14.26 +              | _ => "Exception- " ^ General.exnMessage exn ^ " raised");
   14.27 +            val _ = output_warnings ();
   14.28 +            val _ = output_writeln ();
   14.29 +          in raise_error exn_msg end;
   14.30    in
   14.31      if verbose then (output_warnings (); flush_error (); output_writeln ())
   14.32      else ()
    15.1 --- a/src/Pure/PIDE/document.ML	Thu Sep 09 11:05:52 2010 +0200
    15.2 +++ b/src/Pure/PIDE/document.ML	Thu Sep 09 17:20:27 2010 +0200
    15.3 @@ -225,7 +225,7 @@
    15.4              SOME (st', NONE) => ([], SOME st')
    15.5            | SOME (_, SOME exn_info) =>
    15.6                (case ML_Compiler.exn_messages (Runtime.EXCURSION_FAIL exn_info) of
    15.7 -                [] => raise Exn.Interrupt
    15.8 +                [] => Exn.interrupt ()
    15.9                | errs => (errs, NONE))
   15.10            | NONE => ([ML_Compiler.exn_message Runtime.TERMINATE], NONE));
   15.11          val _ = List.app (Toplevel.error_msg tr) errs;
    16.1 --- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Thu Sep 09 11:05:52 2010 +0200
    16.2 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Thu Sep 09 17:20:27 2010 +0200
    16.3 @@ -983,17 +983,18 @@
    16.4      end handle e => handler (e,SOME src)  (* error in XML parse or Ready issue *)
    16.5  
    16.6  and handler (e,srco) =
    16.7 -    case (e,srco) of
    16.8 -        (XML_PARSE,SOME src) =>
    16.9 -        panic "Invalid XML input, aborting" (* TODO: attempt recovery  *)
   16.10 -      | (Exn.Interrupt,SOME src) =>
   16.11 -        (Output.error_msg "Interrupt during PGIP processing"; loop true src)
   16.12 -      | (Toplevel.UNDEF,SOME src) =>
   16.13 -        (Output.error_msg "No working context defined"; loop true src)
   16.14 -      | (e,SOME src) =>
   16.15 -        (Output.error_msg (ML_Compiler.exn_message e); loop true src)
   16.16 -      | (PGIP_QUIT,_) => ()
   16.17 -      | (_,NONE) => ()
   16.18 +    if Exn.is_interrupt e andalso is_some srco then
   16.19 +        (Output.error_msg "Interrupt during PGIP processing"; loop true (the srco))
   16.20 +    else
   16.21 +        case (e,srco) of
   16.22 +            (XML_PARSE,SOME src) =>
   16.23 +            panic "Invalid XML input, aborting" (* TODO: attempt recovery  *)
   16.24 +          | (Toplevel.UNDEF,SOME src) =>
   16.25 +            (Output.error_msg "No working context defined"; loop true src)
   16.26 +          | (e,SOME src) =>
   16.27 +            (Output.error_msg (ML_Compiler.exn_message e); loop true src)
   16.28 +          | (PGIP_QUIT,_) => ()
   16.29 +          | (_,NONE) => ()
   16.30  in
   16.31    (* TODO: add socket interface *)
   16.32