discontinued separate Pure-ProofGeneral keywords session -- protocol commands are already defined in Pure;

--- a/Admin/update-keywords	Fri Aug 27 21:23:31 2010 +0200
+++ b/Admin/update-keywords	Fri Aug 27 22:09:51 2010 +0200
@@ -11,9 +11,9 @@
 cd "$ISABELLE_HOME/etc"
 
 isabelle keywords \
-  "$LOG/Pure.gz" "$LOG/Pure-ProofGeneral.gz" "$LOG/HOL.gz" "$LOG/HOLCF.gz" \
-  "$LOG/HOL-Boogie.gz" "$LOG/HOL-Nominal.gz" "$LOG/HOL-Statespace.gz"
+  "$LOG/Pure.gz" "$LOG/HOL.gz" "$LOG/HOLCF.gz" "$LOG/HOL-Boogie.gz" \
+  "$LOG/HOL-Nominal.gz" "$LOG/HOL-Statespace.gz"
 
 isabelle keywords -k ZF \
-  "$LOG/Pure.gz" "$LOG/Pure-ProofGeneral.gz" "$LOG/FOL.gz" "$LOG/ZF.gz"
+  "$LOG/Pure.gz" "$LOG/FOL.gz" "$LOG/ZF.gz"
 

--- a/etc/isar-keywords-ZF.el	Fri Aug 27 21:23:31 2010 +0200
+++ b/etc/isar-keywords-ZF.el	Fri Aug 27 22:09:51 2010 +0200
@@ -1,6 +1,6 @@
 ;;
 ;; Keyword classification tables for Isabelle/Isar.
-;; Generated from Pure + Pure-ProofGeneral + FOL + ZF.
+;; Generated from Pure + FOL + ZF.
 ;; *** DO NOT EDIT *** DO NOT EDIT *** DO NOT EDIT ***
 ;;
 

--- a/etc/isar-keywords.el	Fri Aug 27 21:23:31 2010 +0200
+++ b/etc/isar-keywords.el	Fri Aug 27 22:09:51 2010 +0200
@@ -1,6 +1,6 @@
 ;;
 ;; Keyword classification tables for Isabelle/Isar.
-;; Generated from Pure + Pure-ProofGeneral + HOL + HOLCF + HOL-Boogie + HOL-Nominal + HOL-Statespace.
+;; Generated from Pure + HOL + HOLCF + HOL-Boogie + HOL-Nominal + HOL-Statespace.
 ;; *** DO NOT EDIT *** DO NOT EDIT *** DO NOT EDIT ***
 ;;
 

--- a/src/Pure/IsaMakefile	Fri Aug 27 21:23:31 2010 +0200
+++ b/src/Pure/IsaMakefile	Fri Aug 27 22:09:51 2010 +0200
@@ -6,7 +6,7 @@
 
 default: Pure
 images: Pure
-test: RAW Pure-ProofGeneral
+test: RAW
 all: images test
 
 
@@ -256,15 +256,7 @@
 	@./mk
 
 
-## Proof General keywords
-
-Pure-ProofGeneral: Pure $(LOG)/Pure-ProofGeneral.gz
-
-$(LOG)/Pure-ProofGeneral.gz: $(OUT)/Pure ProofGeneral/proof_general_keywords.ML
-	@$(ISABELLE_TOOL) usedir -f proof_general_keywords.ML $(OUT)/Pure ProofGeneral
-
-
 ## clean
 
 clean:
-	@rm -f $(OUT)/Pure $(LOG)/Pure.gz $(OUT)/RAW $(LOG)/RAW.gz $(LOG)/Pure-ProofGeneral.gz
+	@rm -f $(OUT)/Pure $(LOG)/Pure.gz $(OUT)/RAW $(LOG)/RAW.gz

--- a/src/Pure/ProofGeneral/proof_general_emacs.ML	Fri Aug 27 21:23:31 2010 +0200
+++ b/src/Pure/ProofGeneral/proof_general_emacs.ML	Fri Aug 27 22:09:51 2010 +0200
@@ -10,7 +10,6 @@
   val test_markupN: string
   val sendback: string -> Pretty.T list -> unit
   val init: bool -> unit
-  val init_outer_syntax: unit -> unit
   structure ThyLoad: sig val add_path: string -> unit end
 end;
 
@@ -20,7 +19,6 @@
 
 (* print modes *)
 
-val proof_generalN = "ProofGeneralEmacs";  (*token markup (colouring vars, etc.)*)
 val thm_depsN = "thm_deps";                (*meta-information about theorem deps*)
 val test_markupN = "test_markup";          (*XML markup for everything*)
 
@@ -187,44 +185,35 @@
 
 (* additional outer syntax for Isar *)
 
-fun prP () =
+val _ =
   Outer_Syntax.improper_command "ProofGeneral.pr" "print state (internal)" Keyword.diag
     (Scan.succeed (Toplevel.no_timing o Toplevel.keep (fn state =>
       if Toplevel.is_toplevel state orelse Toplevel.is_theory state then tell_clear_goals ()
       else (Toplevel.quiet := false; Toplevel.print_state true state))));
 
-fun undoP () = (*undo without output -- historical*)
+val _ = (*undo without output -- historical*)
   Outer_Syntax.improper_command "ProofGeneral.undo" "(internal)" Keyword.control
     (Scan.succeed (Toplevel.no_timing o Toplevel.imperative (fn () => Isar.undo 1)));
 
-fun restartP () =
+val _ =
   Outer_Syntax.improper_command "ProofGeneral.restart" "(internal)" Keyword.control
     (Parse.opt_unit >> (Toplevel.no_timing oo K (Toplevel.imperative restart)));
 
-fun kill_proofP () =
+val _ =
   Outer_Syntax.improper_command "ProofGeneral.kill_proof" "(internal)" Keyword.control
     (Scan.succeed (Toplevel.no_timing o
       Toplevel.imperative (fn () => (Isar.kill_proof (); tell_clear_goals ()))));
 
-fun inform_file_processedP () =
+val _ =
   Outer_Syntax.improper_command "ProofGeneral.inform_file_processed" "(internal)" Keyword.control
     (Parse.name >> (fn file =>
       Toplevel.no_timing o Toplevel.imperative (fn () => inform_file_processed file)));
 
-fun inform_file_retractedP () =
+val _ =
   Outer_Syntax.improper_command "ProofGeneral.inform_file_retracted" "(internal)" Keyword.control
     (Parse.name >> (Toplevel.no_timing oo
       (fn file => Toplevel.imperative (fn () => inform_file_retracted file))));
 
-fun process_pgipP () =
-  Outer_Syntax.improper_command "ProofGeneral.process_pgip" "(internal)" Keyword.control
-    (Parse.text >> (Toplevel.no_timing oo
-      (fn txt => Toplevel.imperative (fn () => ProofGeneralPgip.process_pgip txt))));
-
-fun init_outer_syntax () = List.app (fn f => f ())
-  [prP, undoP, restartP, kill_proofP, inform_file_processedP,
-    inform_file_retractedP, process_pgipP];
-
 
 (* init *)
 
@@ -234,17 +223,17 @@
   | init true =
       (if ! initialized then ()
        else
-        (init_outer_syntax ();
-         Output.add_mode Symbol.xsymbolsN Symbol.output Output.default_escape;
-         Output.add_mode proof_generalN Output.default_output Output.default_escape;
-         Markup.add_mode proof_generalN YXML.output_markup;
+        (Output.add_mode Symbol.xsymbolsN Symbol.output Output.default_escape;
+         Output.add_mode ProofGeneralPgip.proof_general_emacsN
+          Output.default_output Output.default_escape;
+         Markup.add_mode ProofGeneralPgip.proof_general_emacsN YXML.output_markup;
          setup_messages ();
-         ProofGeneralPgip.init_pgip_channel (! Output.priority_fn);
+         ProofGeneralPgip.pgip_channel_emacs (! Output.priority_fn);
          setup_thy_loader ();
          setup_present_hook ();
          initialized := true);
        sync_thy_loader ();
-       Unsynchronized.change print_mode (update (op =) proof_generalN);
+       Unsynchronized.change print_mode (update (op =) ProofGeneralPgip.proof_general_emacsN);
        Secure.PG_setup ();
        Isar.toplevel_loop TextIO.stdIn
         {init = true, welcome = true, sync = true, secure = Secure.is_secure ()});

--- a/src/Pure/ProofGeneral/proof_general_keywords.ML	Fri Aug 27 21:23:31 2010 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,8 +0,0 @@
-(*  Title:      Pure/ProofGeneral/proof_general_keywords.ML
-    Author:     Makarius
-
-Dummy session with outer syntax keyword initialization.
-*)
-
-ProofGeneral.init_outer_syntax ();
-

--- 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;