Initialise pgip id also for Emacs mode. Allow dynamic config file location for PGIP.
authoraspinall
Fri Sep 30 13:47:36 2005 +0200 (2005-09-30)
changeset 177325b71bef7ad10
parent 17731 c495e6029d00
child 17733 25ffdae37db1
Initialise pgip id also for Emacs mode. Allow dynamic config file location for PGIP.
src/Pure/proof_general.ML
     1.1 --- a/src/Pure/proof_general.ML	Fri Sep 30 11:43:42 2005 +0200
     1.2 +++ b/src/Pure/proof_general.ML	Fri Sep 30 13:47:36 2005 +0200
     1.3 @@ -616,20 +616,24 @@
     1.4  
     1.5  (* Configuration: GUI config, proverinfo messages *)
     1.6  
     1.7 +
     1.8 +fun orenv v d = case (getenv v) of "" => d  | s => s
     1.9 +
    1.10  local
    1.11 -    val config_file = "~~/lib/ProofGeneral/pgip_isar.xml"
    1.12 -    val name_attr = pair "name"
    1.13 -    val version_attr = pair "version"
    1.14 -    val isabelle_www = "http://isabelle.in.tum.de/"
    1.15 +    fun config_file()  = orenv "ISABELLE_PGIPCONFIG" "~~/lib/ProofGeneral/pgip_isar.xml"
    1.16 +    fun isabelle_www() = orenv "ISABELLE_HOMEPAGE" "http://isabelle.in.tum.de/"
    1.17  in
    1.18  fun send_pgip_config () =
    1.19      let
    1.20 -        val path = Path.unpack config_file
    1.21 +        val path = Path.unpack (config_file())
    1.22          val exists = File.exists path
    1.23          val proverinfo =
    1.24              XML.element "proverinfo"
    1.25 -              [("name",Session.name()), ("version", version),
    1.26 -               ("url", isabelle_www), ("filenameextns", ".thy;")]
    1.27 +              [("name",     	 "Isabelle"), 
    1.28 +	       ("version",  	 version),
    1.29 +	       ("instance", 	 Session.name()), 
    1.30 +	       ("url",      	 isabelle_www()),   
    1.31 +	       ("filenameextns", ".thy;")]
    1.32              [XML.element "welcomemsg" [] [XML.text (Session.welcome())],
    1.33               XML.element "helpdoc"
    1.34           (* NB: would be nice to generate/display docs from isatool
    1.35 @@ -642,7 +646,7 @@
    1.36      in
    1.37          if exists then
    1.38              (issue_pgips [proverinfo]; issue_pgips [File.read path])
    1.39 -        else panic ("PGIP configuration file " ^ config_file ^ " not found")
    1.40 +        else panic ("PGIP configuration file \"" ^ config_file() ^ "\" not found")
    1.41      end;
    1.42  end
    1.43  
    1.44 @@ -1431,9 +1435,9 @@
    1.45      set initialized; ()));
    1.46    sync_thy_loader ();
    1.47    change print_mode (cons proof_generalN o remove (op =) proof_generalN);
    1.48 +  init_pgip_session_id();
    1.49    if pgip then
    1.50 -      (init_pgip_session_id();
    1.51 -       change print_mode (append [pgmlN, pgmlatomsN] o fold (remove (op =)) [pgmlN, pgmlatomsN]))
    1.52 +      (change print_mode (append [pgmlN, pgmlatomsN] o fold (remove (op =)) [pgmlN, pgmlatomsN]))
    1.53    else
    1.54      pgip_emacs_compatibility_flag := true;  (* assume this for PG <3.6 compatibility *)
    1.55    set quick_and_dirty;