Move welcomemsg and helpdoc to pgip_isar.xml
authoraspinall
Fri Sep 30 17:54:04 2005 +0200 (2005-09-30)
changeset 17739eddebb044a62
parent 17738 9c7fc0d5cf84
child 17740 fc385ce6187d
Move welcomemsg and helpdoc to pgip_isar.xml
src/Pure/proof_general.ML
     1.1 --- a/src/Pure/proof_general.ML	Fri Sep 30 17:52:18 2005 +0200
     1.2 +++ b/src/Pure/proof_general.ML	Fri Sep 30 17:54:04 2005 +0200
     1.3 @@ -632,17 +632,10 @@
     1.4                [("name",     	 "Isabelle"), 
     1.5  	       ("version",  	 version),
     1.6  	       ("instance", 	 Session.name()), 
     1.7 +	       ("descr",	 "The Isabelle/Isar theorem prover"),
     1.8  	       ("url",      	 isabelle_www()),   
     1.9  	       ("filenameextns", ".thy;")]
    1.10 -            [XML.element "welcomemsg" [] [XML.text (Session.welcome())],
    1.11 -             XML.element "helpdoc"
    1.12 -         (* NB: would be nice to generate/display docs from isatool
    1.13 -          doc, but that program may not be running on same machine;
    1.14 -          front end should be responsible for launching viewer, etc. *)
    1.15 -                      [("name", "Isabelle/HOL Tutorial"),
    1.16 -                       ("descr", "A Gentle Introduction to Isabelle/HOL"),
    1.17 -                       ("url",  "http://isabelle.in.tum.de/dist/Isabelle2004/doc/tutorial.pdf")]
    1.18 -              []]
    1.19 +            []
    1.20      in
    1.21          if exists then
    1.22              (issue_pgips [proverinfo]; issue_pgips [File.read path])