# HG changeset patch
# User wenzelm
# Date 1368468906 -7200
# Node ID 7e014c16da7dcfa6d88349ca04d550f2c2adaeaa
# Parent  016cb7d8f297cd6a15be16bd249e24b53e1ec3ff
dummy PGIP id, which appears to be sufficient for PG/Emacs;
removed obsolete init operations;

diff -r 016cb7d8f297 -r 7e014c16da7d src/Pure/ProofGeneral/proof_general_emacs.ML
--- a/src/Pure/ProofGeneral/proof_general_emacs.ML	Mon May 13 19:52:16 2013 +0200
+++ b/src/Pure/ProofGeneral/proof_general_emacs.ML	Mon May 13 20:15:06 2013 +0200
@@ -215,7 +215,6 @@
       Output.default_output Output.default_escape;
      Markup.add_mode ProofGeneralPgip.proof_general_emacsN YXML.output_markup;
      setup_messages ();
-     ProofGeneralPgip.init_pgip_session_id ();
      setup_thy_loader ();
      setup_present_hook ();
      initialized := true);
diff -r 016cb7d8f297 -r 7e014c16da7d src/Pure/ProofGeneral/proof_general_pgip.ML
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Mon May 13 19:52:16 2013 +0200
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Mon May 13 20:15:06 2013 +0200
@@ -10,9 +10,6 @@
   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 *)
-
-  val init_pgip_session_id: unit -> unit
 
   (* More message functions... *)
   val nonfatal_error : string -> unit     (* recoverable (batch) error: carry on scripting *)
@@ -47,7 +44,7 @@
 local
   val pgip_class  = "pg"
   val pgip_tag = "Isabelle/Isar"
-  val pgip_id = Unsynchronized.ref ""
+  val pgip_id = "dummy"
   val pgip_seq = Unsynchronized.ref 0
   fun pgip_serial () = Unsynchronized.inc pgip_seq
 
@@ -55,7 +52,7 @@
     Pgip { tag = SOME pgip_tag,
            class = pgip_class,
            seq = pgip_serial (),
-           id = ! pgip_id,
+           id = pgip_id,
            destid = ! pgip_refid,
            (* destid=refid since Isabelle only communicates back to sender *)
            refid = ! pgip_refid,
@@ -63,11 +60,7 @@
            content = pgips }
 in
 
-fun init_pgip_session_id () =
-    pgip_id := getenv "HOSTNAME" ^ "/" ^ getenv "USER" ^ "/" ^
-               getenv "ISABELLE_PID" ^ "/" ^ Time.toString (Time.now ())
-
-fun matching_pgip_id id = (id = ! pgip_id)
+fun matching_pgip_id id = (id = pgip_id)
 
 val output_xml_fn = Unsynchronized.ref Output.physical_writeln
 fun output_xml s = ! output_xml_fn (XML.string_of s);
@@ -991,29 +984,6 @@
 end
 
 
-(* init *)
-
-val initialized = Unsynchronized.ref false;
-
-fun init_pgip false = panic "No Proof General interface support for Isabelle/classic mode."
-  | init_pgip true =
-      (if ! initialized then ()
-       else
-        (setup_preferences_tweak ();
-         Output.add_mode proof_generalN Output.default_output Output.default_escape;
-         Markup.add_mode proof_generalN YXML.output_markup;
-         setup_messages ();
-         setup_thy_loader ();
-         setup_present_hook ();
-         init_pgip_session_id ();
-         welcome ();
-         initialized := true);
-       sync_thy_loader ();
-       Unsynchronized.change print_mode (update (op =) proof_generalN);
-       pgip_toplevel tty_src);
-
-
-
 (** Out-of-loop PGIP commands (for Emacs hybrid mode) **)
 
 local