1.1 --- a/src/Pure/ProofGeneral/proof_general_emacs.ML	Mon May 13 19:52:16 2013 +0200
     1.2 +++ b/src/Pure/ProofGeneral/proof_general_emacs.ML	Mon May 13 20:15:06 2013 +0200
     1.3 @@ -215,7 +215,6 @@
     1.4        Output.default_output Output.default_escape;
     1.5       Markup.add_mode ProofGeneralPgip.proof_general_emacsN YXML.output_markup;
     1.6       setup_messages ();
     1.7 -     ProofGeneralPgip.init_pgip_session_id ();
     1.8       setup_thy_loader ();
     1.9       setup_present_hook ();
    1.10       initialized := true);

     2.1 --- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Mon May 13 19:52:16 2013 +0200
     2.2 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Mon May 13 20:15:06 2013 +0200
     2.3 @@ -10,9 +10,6 @@
     2.4    val proof_general_emacsN: string
     2.5  
     2.6    val new_thms_deps: theory -> theory -> string list * string list
     2.7 -  val init_pgip: bool -> unit             (* main PGIP loop with true; fail with false *)
     2.8 -
     2.9 -  val init_pgip_session_id: unit -> unit
    2.10  
    2.11    (* More message functions... *)
    2.12    val nonfatal_error : string -> unit     (* recoverable (batch) error: carry on scripting *)
    2.13 @@ -47,7 +44,7 @@
    2.14  local
    2.15    val pgip_class  = "pg"
    2.16    val pgip_tag = "Isabelle/Isar"
    2.17 -  val pgip_id = Unsynchronized.ref ""
    2.18 +  val pgip_id = "dummy"
    2.19    val pgip_seq = Unsynchronized.ref 0
    2.20    fun pgip_serial () = Unsynchronized.inc pgip_seq
    2.21  
    2.22 @@ -55,7 +52,7 @@
    2.23      Pgip { tag = SOME pgip_tag,
    2.24             class = pgip_class,
    2.25             seq = pgip_serial (),
    2.26 -           id = ! pgip_id,
    2.27 +           id = pgip_id,
    2.28             destid = ! pgip_refid,
    2.29             (* destid=refid since Isabelle only communicates back to sender *)
    2.30             refid = ! pgip_refid,
    2.31 @@ -63,11 +60,7 @@
    2.32             content = pgips }
    2.33  in
    2.34  
    2.35 -fun init_pgip_session_id () =
    2.36 -    pgip_id := getenv "HOSTNAME" ^ "/" ^ getenv "USER" ^ "/" ^
    2.37 -               getenv "ISABELLE_PID" ^ "/" ^ Time.toString (Time.now ())
    2.38 -
    2.39 -fun matching_pgip_id id = (id = ! pgip_id)
    2.40 +fun matching_pgip_id id = (id = pgip_id)
    2.41  
    2.42  val output_xml_fn = Unsynchronized.ref Output.physical_writeln
    2.43  fun output_xml s = ! output_xml_fn (XML.string_of s);
    2.44 @@ -991,29 +984,6 @@
    2.45  end
    2.46  
    2.47  
    2.48 -(* init *)
    2.49 -
    2.50 -val initialized = Unsynchronized.ref false;
    2.51 -
    2.52 -fun init_pgip false = panic "No Proof General interface support for Isabelle/classic mode."
    2.53 -  | init_pgip true =
    2.54 -      (if ! initialized then ()
    2.55 -       else
    2.56 -        (setup_preferences_tweak ();
    2.57 -         Output.add_mode proof_generalN Output.default_output Output.default_escape;
    2.58 -         Markup.add_mode proof_generalN YXML.output_markup;
    2.59 -         setup_messages ();
    2.60 -         setup_thy_loader ();
    2.61 -         setup_present_hook ();
    2.62 -         init_pgip_session_id ();
    2.63 -         welcome ();
    2.64 -         initialized := true);
    2.65 -       sync_thy_loader ();
    2.66 -       Unsynchronized.change print_mode (update (op =) proof_generalN);
    2.67 -       pgip_toplevel tty_src);
    2.68 -
    2.69 -
    2.70 -
    2.71  (** Out-of-loop PGIP commands (for Emacs hybrid mode) **)
    2.72  
    2.73  local