# HG changeset patch
# User aspinall
# Date 1096293796 -7200
# Node ID 09271a87fbf03930a1205d1d01520d7d68917a0b
# Parent  a383b0a412b0cf9cb118967fbcb7c7e66fbe2173
Add filenamextns to prover info.  Update doc location.  Add whitespace element in parseresult

diff -r a383b0a412b0 -r 09271a87fbf0 src/Pure/proof_general.ML
--- a/src/Pure/proof_general.ML	Mon Sep 27 16:02:31 2004 +0200
+++ b/src/Pure/proof_general.ML	Mon Sep 27 16:03:16 2004 +0200
@@ -620,7 +620,7 @@
 	val proverinfo = 
 	    XML.element "proverinfo"
               [("name",Session.name()), ("version", version),
-	       ("url", isabelle_www)]
+	       ("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
@@ -628,7 +628,7 @@
           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/Isabelle2003/doc/tutorial.pdf")]
+		       ("url",  "http://isabelle.in.tum.de/dist/Isabelle2004/doc/tutorial.pdf")]
 	      []]
     in
 	if exists then
@@ -736,6 +736,11 @@
     fun markup_text_attrs str elt attrs = [XML.element elt attrs [XML.text str]]
     fun empty elt = [XML.element elt [] []]
 
+    fun whitespace "" = ""
+      | whitespace str = XML.element "whitespace" []
+				(map (fn c=> "&#"^Int.toString (Char.ord c)^ ";") 
+				     (String.explode str))
+
     (* an extra token is needed to terminate the command *)
     val sync = OuterSyntax.scan "\\<^sync>";
 
@@ -918,7 +923,7 @@
 	val (prewhs,rest) = take_prefix (OuterLex.is_kind OuterLex.Space) toks
     in 
 	if (prewhs <> []) then
-	    XML.text (implode (map OuterLex.unparse prewhs))
+	    whitespace (implode (map OuterLex.unparse prewhs)) 
 	    :: (markup_comment_whs rest)
 	else 
 	    (markup_text (OuterLex.unparse t) "comment") @