src/Pure/proof_general.ML
changeset 18678 dd0c569fa43d
parent 18587 d4dcdfd764a0
child 18708 4b3dadb4fe33
     1.1 --- a/src/Pure/proof_general.ML	Fri Jan 13 17:39:41 2006 +0100
     1.2 +++ b/src/Pure/proof_general.ML	Sat Jan 14 17:14:06 2006 +0100
     1.3 @@ -431,7 +431,7 @@
     1.4    let val name = thy_name file in
     1.5      if Toplevel.is_toplevel state andalso ThyInfo.known_thy name then
     1.6       (ThyInfo.touch_child_thys name;
     1.7 -      transform_error ThyInfo.pretend_use_thy_only name handle ERROR_MESSAGE msg =>
     1.8 +      ThyInfo.pretend_use_thy_only name handle ERROR msg =>
     1.9         (warning msg; warning ("Failed to register theory: " ^ quote name);
    1.10          tell_file_retracted (Path.base (Path.unpack file))))
    1.11      else raise Toplevel.UNDEF
    1.12 @@ -639,7 +639,7 @@
    1.13      in
    1.14          if exists then
    1.15              (issue_pgips [proverinfo]; issue_pgips [File.read path])
    1.16 -        else panic ("PGIP configuration file \"" ^ config_file() ^ "\" not found")
    1.17 +        else Output.panic ("PGIP configuration file \"" ^ config_file() ^ "\" not found")
    1.18      end;
    1.19  end
    1.20  
    1.21 @@ -1302,9 +1302,9 @@
    1.22                                else false
    1.23             end)
    1.24          | _ => raise PGIP "Invalid PGIP packet received")
    1.25 -     handle (PGIP msg) =>
    1.26 -            (error (msg ^ "\nPGIP error occured in XML text below:\n" ^
    1.27 -                    (XML.string_of_tree xml))))
    1.28 +     handle PGIP msg =>
    1.29 +            error (msg ^ "\nPGIP error occured in XML text below:\n" ^
    1.30 +                    (XML.string_of_tree xml)))
    1.31  
    1.32  val process_pgip = K () o process_pgip_tree o XML.tree_of_string
    1.33  
    1.34 @@ -1336,9 +1336,8 @@
    1.35  and handler (e,srco) =
    1.36      case (e,srco) of
    1.37          (XML_PARSE,SOME src) =>
    1.38 -        panic "Invalid XML input, aborting" (* NB: loop OK for tty, but want exit on EOF *)
    1.39 +        Output.panic "Invalid XML input, aborting" (* NB: loop OK for tty, but want exit on EOF *)
    1.40        | (PGIP_QUIT,_) => ()
    1.41 -      | (ERROR,SOME src) => loop true src (* message already given *)
    1.42        | (Interrupt,SOME src) => (!error_fn "Interrupt during PGIP processing"; loop true src)
    1.43        | (Toplevel.UNDEF,SOME src) => (error "No working context defined"; loop true src) (* usually *)
    1.44        | (e,SOME src) => (error (Toplevel.exn_message e); loop true src)
    1.45 @@ -1441,7 +1440,7 @@
    1.46   (init_setup isar false;
    1.47    if isar then Isar.sync_main () else isa_restart ());
    1.48  
    1.49 -fun init_pgip false = panic "PGIP not supported for Isabelle/classic mode."
    1.50 +fun init_pgip false = Output.panic "PGIP not supported for Isabelle/classic mode."
    1.51    | init_pgip true = (init_setup true true; pgip_toplevel tty_src);
    1.52  
    1.53