src/Pure/ProofGeneral/proof_general_pgip.ML
changeset 36148 4ddcc2b07891
parent 33389 bb3a5fa94a91
child 36689 379f5b1e7f91
equal deleted inserted replaced
36147:b43b22f63665 36148:4ddcc2b07891
   953                   (* no response to ignored messages. *)
   953                   (* no response to ignored messages. *)
   954                   false
   954                   false
   955            end)
   955            end)
   956         | _ => raise PGIP "Invalid PGIP packet received")
   956         | _ => raise PGIP "Invalid PGIP packet received")
   957      handle PGIP msg =>
   957      handle PGIP msg =>
   958             (Output.error_msg ((msg ^ "\nPGIP error occured in XML text below:\n") ^
   958             (Output.error_msg ((msg ^ "\nPGIP error occurred in XML text below:\n") ^
   959                                (XML.string_of xml));
   959                                (XML.string_of xml));
   960              true))
   960              true))
   961 
   961 
   962 (* External input *)
   962 (* External input *)
   963 
   963