# HG changeset patch
# User aspinall
# Date 1128095644 -7200
# Node ID eddebb044a620c953fe280ff02cb2f345b271f74
# Parent  9c7fc0d5cf84399d5273430984387d1fda0adb6b
Move welcomemsg and helpdoc to pgip_isar.xml

diff -r 9c7fc0d5cf84 -r eddebb044a62 src/Pure/proof_general.ML
--- a/src/Pure/proof_general.ML	Fri Sep 30 17:52:18 2005 +0200
+++ b/src/Pure/proof_general.ML	Fri Sep 30 17:54:04 2005 +0200
@@ -632,17 +632,10 @@
               [("name",     	 "Isabelle"), 
 	       ("version",  	 version),
 	       ("instance", 	 Session.name()), 
+	       ("descr",	 "The Isabelle/Isar theorem prover"),
 	       ("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
-          doc, but that program may not be running on same machine;
-          front end should be responsible for launching viewer, etc. *)
-                      [("name", "Isabelle/HOL Tutorial"),
-                       ("descr", "A Gentle Introduction to Isabelle/HOL"),
-                       ("url",  "http://isabelle.in.tum.de/dist/Isabelle2004/doc/tutorial.pdf")]
-              []]
+            []
     in
         if exists then
             (issue_pgips [proverinfo]; issue_pgips [File.read path])