# HG changeset patch # User aspinall # Date 1182345002 -7200 # Node ID 061f288540171d3c2379562486596ecb2ad41438 # Parent b2e7d4c29614de8d28aaa2415254b9b91f467302 Remove dedicated flag setting elements in favour of setproverflag. Restore displayconfig response in askpgip. diff -r b2e7d4c29614 -r 061f28854017 src/Pure/ProofGeneral/proof_general_pgip.ML --- a/src/Pure/ProofGeneral/proof_general_pgip.ML Wed Jun 20 15:07:42 2007 +0200 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML Wed Jun 20 15:10:02 2007 +0200 @@ -14,8 +14,8 @@ val init_pgip_channel: (string -> unit) -> unit val process_pgip: string -> unit - (* Yet more message functions... *) - val nonfatal_error : string -> unit (* recoverable error *) + (* More message functions... *) + val nonfatal_error : string -> unit (* recoverable (batch) error: carry on scripting *) val log_msg : string -> unit (* for internal log messages *) val error_with_pos : PgipTypes.fatality -> Position.T -> string -> unit @@ -466,9 +466,10 @@ These are programmed uniformly for extensibility. *) fun askpgip (Askpgip vs) = - issue_pgip - (Usespgip { version = PgipIsabelle.isabelle_pgip_version_supported, - pgipelems = PgipIsabelle.accepted_inputs }) + (issue_pgip + (Usespgip { version = PgipIsabelle.isabelle_pgip_version_supported, + pgipelems = PgipIsabelle.accepted_inputs }); + send_pgip_config()) fun askpgml (Askpgml vs) = issue_pgip @@ -531,11 +532,6 @@ (show_theorem_dependencies := b; proofs := (if b then 1 else 2)) -fun startquiet vs = set_proverflag_quiet true; (* TO BE REMOVED *) -fun stopquiet vs = set_proverflag_quiet false; (* TO BE REMOVED *) -fun pgmlsymbolson vs = set_proverflag_pgmlsymbols true; (* TO BE REMOVED *) -fun pgmlsymbolsoff vs = set_proverflag_pgmlsymbols false; (* TO BE REMOVED *) - fun setproverflag (Setproverflag vs) = let val flagname = #flagname vs @@ -545,7 +541,8 @@ "quiet" => set_proverflag_quiet value | "pgmlsymbols" => set_proverflag_pgmlsymbols value | "metainfo:thmdeps" => set_proverflag_thmdeps value - | _ => log_msg ("Unrecognised prover control flag: " ^ (quote flagname) ^ " ignored.")) + | _ => log_msg ("Unrecognised prover control flag: " ^ + (quote flagname) ^ " ignored.")) end @@ -950,16 +947,12 @@ | Pgip.Setpref _ => setpref inp | Pgip.Proverinit _ => proverinit inp | Pgip.Proverexit _ => proverexit inp - | Pgip.Startquiet _ => startquiet inp - | Pgip.Stopquiet _ => stopquiet inp - | Pgip.Pgmlsymbolson _ => pgmlsymbolson inp - | Pgip.Pgmlsymbolsoff _ => pgmlsymbolsoff inp | Pgip.Setproverflag _ => setproverflag inp | Pgip.Dostep _ => dostep inp | Pgip.Undostep _ => undostep inp | Pgip.Redostep _ => redostep inp - | Pgip.Forget _ => error " not implemented" - | Pgip.Restoregoal _ => error " not implemented" + | Pgip.Forget _ => error " not implemented by Isabelle" + | Pgip.Restoregoal _ => error " not implemented by Isabelle" | Pgip.Abortgoal _ => abortgoal inp | Pgip.Askids _ => askids inp | Pgip.Askrefs _ => askrefs inp