src/Pure/ProofGeneral/proof_general_pgip.ML
changeset 39232 69c6d3e87660
parent 39139 8235606e2b23
child 39513 fce2202892c4
     1.1 --- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Thu Sep 09 11:05:52 2010 +0200
     1.2 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Thu Sep 09 17:20:27 2010 +0200
     1.3 @@ -983,17 +983,18 @@
     1.4      end handle e => handler (e,SOME src)  (* error in XML parse or Ready issue *)
     1.5  
     1.6  and handler (e,srco) =
     1.7 -    case (e,srco) of
     1.8 -        (XML_PARSE,SOME src) =>
     1.9 -        panic "Invalid XML input, aborting" (* TODO: attempt recovery  *)
    1.10 -      | (Exn.Interrupt,SOME src) =>
    1.11 -        (Output.error_msg "Interrupt during PGIP processing"; loop true src)
    1.12 -      | (Toplevel.UNDEF,SOME src) =>
    1.13 -        (Output.error_msg "No working context defined"; loop true src)
    1.14 -      | (e,SOME src) =>
    1.15 -        (Output.error_msg (ML_Compiler.exn_message e); loop true src)
    1.16 -      | (PGIP_QUIT,_) => ()
    1.17 -      | (_,NONE) => ()
    1.18 +    if Exn.is_interrupt e andalso is_some srco then
    1.19 +        (Output.error_msg "Interrupt during PGIP processing"; loop true (the srco))
    1.20 +    else
    1.21 +        case (e,srco) of
    1.22 +            (XML_PARSE,SOME src) =>
    1.23 +            panic "Invalid XML input, aborting" (* TODO: attempt recovery  *)
    1.24 +          | (Toplevel.UNDEF,SOME src) =>
    1.25 +            (Output.error_msg "No working context defined"; loop true src)
    1.26 +          | (e,SOME src) =>
    1.27 +            (Output.error_msg (ML_Compiler.exn_message e); loop true src)
    1.28 +          | (PGIP_QUIT,_) => ()
    1.29 +          | (_,NONE) => ()
    1.30  in
    1.31    (* TODO: add socket interface *)
    1.32