# HG changeset patch
# User wenzelm
# Date 1084209942 -7200
# Node ID 2ed5b960c6b10bb30adc63a6137ed7cf6e473262
# Parent  021264410f8753e14e4ad05197c31df9146fcd66
ProofGeneral.process_pgip command;

diff -r 021264410f87 -r 2ed5b960c6b1 src/Pure/proof_general.ML
--- a/src/Pure/proof_general.ML	Mon May 10 17:10:41 2004 +0200
+++ b/src/Pure/proof_general.ML	Mon May 10 19:25:42 2004 +0200
@@ -317,12 +317,12 @@
 
 fun issue_pgip pgips = notify (XML.element "pgip" [] pgips);
 
-fun usespgml () = 
+fun usespgml () =
   issue_pgip [XML.element "usespgml" [("version", pgml_version_supported)] []];
 
 (*NB: the default returned here is actually the current value, so
   repeated uses of <askprefs> will not work correctly*)
-fun show_options () = issue_pgip (map 
+fun show_options () = issue_pgip (map
   (fn (name, (descr, (ty, get, _))) => (XML.element "oldhaspref"
     [("type", ty), ("descr", descr), ("default", get ())] [name])) (!options));
 
@@ -332,8 +332,8 @@
 
 fun get_option name = (case assoc (!options, name) of
       None => warning ("Unknown option: " ^ quote name)
-    | Some (_, (_, get, _)) => 
-	issue_pgip [XML.element "prefval" [("name", name)] [get ()]]);
+    | Some (_, (_, get, _)) =>
+        issue_pgip [XML.element "prefval" [("name", name)] [get ()]]);
 
 
 (* processing PGIP commands from the interface *)
@@ -428,9 +428,14 @@
     (P.name >> (Toplevel.no_timing oo
       (fn name => Toplevel.imperative (fn () => inform_file_retracted name))));
 
+val process_pgipP =
+  OuterSyntax.improper_command "ProofGeneral.process_pgip" "(internal)" K.control
+    (P.text >> (Toplevel.no_timing oo
+      (fn txt => Toplevel.imperative (fn () => process_pgip txt))));
+
 fun init_outer_syntax () = OuterSyntax.add_parsers
  [undoP, restartP, kill_proofP, context_thy_onlyP, try_context_thy_onlyP,
-  inform_file_processedP, inform_file_retractedP];
+  inform_file_processedP, inform_file_retractedP, process_pgipP];
 
 end;
 
@@ -493,8 +498,4 @@
 
 end;
 
-
 end;
-
-(*a hack for Proof General 3.2 to avoid problems with escapes in ML commands*)
-infix \\\\ val op \\\\ = op \\;