1.1 --- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Thu Jan 04 18:09:30 2007 +0100
     1.2 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Thu Jan 04 18:09:58 2007 +0100
     1.3 @@ -179,14 +179,6 @@
     1.4              queue_or_issue pgip
     1.5          end
     1.6  
     1.7 -    (* Note: PGIP specifies that any fatal Errorresponse which occurs before <ready/>
     1.8 -       indicates that the previously sent command has failed. To be 100% accurate we 
     1.9 -       adjust the Isar top level rather than just using Output.error_msg,
    1.10 -       otherwise degenerate examples like ML_setup {* Output.error_msg "fake"; *}
    1.11 -       (and perhaps other examples involving user tactics which print errors) 
    1.12 -       are wrongly considered to have failed. 
    1.13 -     *)
    1.14 -
    1.15      fun errormsg fatality s =
    1.16          let
    1.17                val content = XML.Elem("pgmltext",[],[XML.Rawtext s])
    1.18 @@ -213,9 +205,9 @@
    1.19    tracing_fn := (fn s => normalmsg  Message Tracing false s);
    1.20    info_fn := (fn s => normalmsg Message Information false s);
    1.21    debug_fn := (fn s => normalmsg Message Internal false s);
    1.22 -  warning_fn := (fn s => errormsg Nonfatal s);
    1.23 +  warning_fn := (fn s => errormsg Warning s);
    1.24    panic_fn := (fn s => errormsg Panic s);
    1.25 -  error_fn := (fn s => errormsg Nonfatal s); (* was (fn s => errormsg Fatal s); *)
    1.26 +  error_fn := (fn s => errormsg Nonfatal s);
    1.27    Toplevel.print_exn_fn := (K () o Option.map (errormsg Fatal) o Toplevel.print_exn_str);
    1.28    ())
    1.29