# HG changeset patch
# User aspinall
# Date 1128080856 -7200
# Node ID 5b71bef7ad10711cae7576b5160877bd9d25d292
# Parent  c495e6029d00beaca0087f93ee251075e03c2aae
Initialise pgip id also for Emacs mode.  Allow dynamic config file location for PGIP.

diff -r c495e6029d00 -r 5b71bef7ad10 src/Pure/proof_general.ML
--- a/src/Pure/proof_general.ML	Fri Sep 30 11:43:42 2005 +0200
+++ b/src/Pure/proof_general.ML	Fri Sep 30 13:47:36 2005 +0200
@@ -616,20 +616,24 @@
 
 (* Configuration: GUI config, proverinfo messages *)
 
+
+fun orenv v d = case (getenv v) of "" => d  | s => s
+
 local
-    val config_file = "~~/lib/ProofGeneral/pgip_isar.xml"
-    val name_attr = pair "name"
-    val version_attr = pair "version"
-    val isabelle_www = "http://isabelle.in.tum.de/"
+    fun config_file()  = orenv "ISABELLE_PGIPCONFIG" "~~/lib/ProofGeneral/pgip_isar.xml"
+    fun isabelle_www() = orenv "ISABELLE_HOMEPAGE" "http://isabelle.in.tum.de/"
 in
 fun send_pgip_config () =
     let
-        val path = Path.unpack config_file
+        val path = Path.unpack (config_file())
         val exists = File.exists path
         val proverinfo =
             XML.element "proverinfo"
-              [("name",Session.name()), ("version", version),
-               ("url", isabelle_www), ("filenameextns", ".thy;")]
+              [("name",     	 "Isabelle"), 
+	       ("version",  	 version),
+	       ("instance", 	 Session.name()), 
+	       ("url",      	 isabelle_www()),   
+	       ("filenameextns", ".thy;")]
             [XML.element "welcomemsg" [] [XML.text (Session.welcome())],
              XML.element "helpdoc"
          (* NB: would be nice to generate/display docs from isatool
@@ -642,7 +646,7 @@
     in
         if exists then
             (issue_pgips [proverinfo]; issue_pgips [File.read path])
-        else panic ("PGIP configuration file " ^ config_file ^ " not found")
+        else panic ("PGIP configuration file \"" ^ config_file() ^ "\" not found")
     end;
 end
 
@@ -1431,9 +1435,9 @@
     set initialized; ()));
   sync_thy_loader ();
   change print_mode (cons proof_generalN o remove (op =) proof_generalN);
+  init_pgip_session_id();
   if pgip then
-      (init_pgip_session_id();
-       change print_mode (append [pgmlN, pgmlatomsN] o fold (remove (op =)) [pgmlN, pgmlatomsN]))
+      (change print_mode (append [pgmlN, pgmlatomsN] o fold (remove (op =)) [pgmlN, pgmlatomsN]))
   else
     pgip_emacs_compatibility_flag := true;  (* assume this for PG <3.6 compatibility *)
   set quick_and_dirty;