# 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 "<forget> not implemented"
-  | Pgip.Restoregoal _      => error "<restoregoal> not implemented"
+  | Pgip.Forget _           => error "<forget> not implemented by Isabelle"
+  | Pgip.Restoregoal _      => error "<restoregoal> not implemented by Isabelle"
   | Pgip.Abortgoal _        => abortgoal inp
   | Pgip.Askids _           => askids inp
   | Pgip.Askrefs _          => askrefs inp