src/Pure/ProofGeneral/proof_general_pgip.ML

--- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Fri Aug 27 21:23:31 2010 +0200
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Fri Aug 27 22:09:51 2010 +0200
@@ -7,12 +7,12 @@
 
 signature PROOF_GENERAL_PGIP =
 sig
+  val proof_general_emacsN: string
+
   val new_thms_deps: theory -> theory -> string list * string list
   val init_pgip: bool -> unit             (* main PGIP loop with true; fail with false *)
 
-  (* These two are just to support the semi-PGIP Emacs mode *)
-  val init_pgip_channel: (string -> unit) -> unit
-  val process_pgip: string -> unit
+  val pgip_channel_emacs: (string -> unit) -> unit
 
   (* More message functions... *)
   val nonfatal_error : string -> unit     (* recoverable (batch) error: carry on scripting *)
@@ -31,6 +31,7 @@
 
 (** print mode **)
 
+val proof_general_emacsN = "ProofGeneralEmacs";
 val proof_generalN = "ProofGeneral";
 val pgmlsymbols_flag = Unsynchronized.ref true;
 
@@ -315,8 +316,6 @@
         fun keyword_elt kind keyword =
             XML.Elem (("keyword", [("word", keyword), ("category", kind)]), [])
         in
-            (* Also, note we don't call init_outer_syntax here to add interface commands,
-            but they should never appear in scripts anyway so it shouldn't matter *)
             Lexicalstructure
               {content = map (keyword_elt "minor") keywords @ map (keyword_elt "major") commands}
         end
@@ -1007,14 +1006,6 @@
 end
 
 
-(* Extra command for embedding prover-control inside document (obscure/debug usage). *)
-
-fun init_outer_syntax () =
-  Outer_Syntax.improper_command "ProofGeneral.process_pgip" "(internal)" Keyword.control
-    (Parse.text >> (Toplevel.no_timing oo
-      (fn txt => Toplevel.imperative (fn () => process_pgip_plain txt))));
-
-
 (* init *)
 
 val initialized = Unsynchronized.ref false;
@@ -1027,7 +1018,6 @@
          Output.add_mode proof_generalN Output.default_output Output.default_escape;
          Markup.add_mode proof_generalN YXML.output_markup;
          setup_messages ();
-         init_outer_syntax ();
          setup_thy_loader ();
          setup_present_hook ();
          init_pgip_session_id ();
@@ -1046,16 +1036,27 @@
 in
 
 (* Set recipient for PGIP results *)
-fun init_pgip_channel writefn =
+fun pgip_channel_emacs writefn =
     (init_pgip_session_id();
      pgip_output_channel := writefn)
 
 (* Process a PGIP command.
    This works for preferences but not generally guaranteed
    because we haven't done full setup here (e.g., no pgml mode)  *)
-fun process_pgip str =
+fun process_pgip_emacs str =
      setmp_CRITICAL output_xml_fn (!pgip_output_channel) process_pgip_plain str
 
 end
 
+
+(* Extra command for embedding prover-control inside document (obscure/debug usage). *)
+
+val _ =
+  Outer_Syntax.improper_command "ProofGeneral.process_pgip" "(internal)" Keyword.control
+    (Parse.text >> (Toplevel.no_timing oo
+      (fn txt => Toplevel.imperative (fn () =>
+        if print_mode_active proof_general_emacsN
+        then process_pgip_emacs txt
+        else process_pgip_plain txt))));
+
 end;