Add filenamextns to prover info. Update doc location. Add whitespace element in parseresult
authoraspinall
Mon Sep 27 16:03:16 2004 +0200 (2004-09-27)
changeset 1520809271a87fbf0
parent 15207 a383b0a412b0
child 15209 b62f72ea3bb0
Add filenamextns to prover info. Update doc location. Add whitespace element in parseresult
src/Pure/proof_general.ML
     1.1 --- a/src/Pure/proof_general.ML	Mon Sep 27 16:02:31 2004 +0200
     1.2 +++ b/src/Pure/proof_general.ML	Mon Sep 27 16:03:16 2004 +0200
     1.3 @@ -620,7 +620,7 @@
     1.4  	val proverinfo = 
     1.5  	    XML.element "proverinfo"
     1.6                [("name",Session.name()), ("version", version),
     1.7 -	       ("url", isabelle_www)]
     1.8 +	       ("url", isabelle_www), ("filenameextns", ".thy;")]
     1.9  	    [XML.element "welcomemsg" [] [XML.text (Session.welcome())],
    1.10  	     XML.element "helpdoc" 
    1.11           (* NB: would be nice to generate/display docs from isatool
    1.12 @@ -628,7 +628,7 @@
    1.13            front end should be responsible for launching viewer, etc. *)
    1.14  		      [("name", "Isabelle/HOL Tutorial"),
    1.15  		       ("descr", "A Gentle Introduction to Isabelle/HOL"), 
    1.16 -		       ("url",  "http://isabelle.in.tum.de/dist/Isabelle2003/doc/tutorial.pdf")]
    1.17 +		       ("url",  "http://isabelle.in.tum.de/dist/Isabelle2004/doc/tutorial.pdf")]
    1.18  	      []]
    1.19      in
    1.20  	if exists then
    1.21 @@ -736,6 +736,11 @@
    1.22      fun markup_text_attrs str elt attrs = [XML.element elt attrs [XML.text str]]
    1.23      fun empty elt = [XML.element elt [] []]
    1.24  
    1.25 +    fun whitespace "" = ""
    1.26 +      | whitespace str = XML.element "whitespace" []
    1.27 +				(map (fn c=> "&#"^Int.toString (Char.ord c)^ ";") 
    1.28 +				     (String.explode str))
    1.29 +
    1.30      (* an extra token is needed to terminate the command *)
    1.31      val sync = OuterSyntax.scan "\\<^sync>";
    1.32  
    1.33 @@ -918,7 +923,7 @@
    1.34  	val (prewhs,rest) = take_prefix (OuterLex.is_kind OuterLex.Space) toks
    1.35      in 
    1.36  	if (prewhs <> []) then
    1.37 -	    XML.text (implode (map OuterLex.unparse prewhs))
    1.38 +	    whitespace (implode (map OuterLex.unparse prewhs)) 
    1.39  	    :: (markup_comment_whs rest)
    1.40  	else 
    1.41  	    (markup_text (OuterLex.unparse t) "comment") @