Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
produce XHTML 1.0 Transitional;
authorwenzelm
Mon, 11 Aug 2008 18:37:51 +0200
changeset 27829 c073006e0137
parent 27828 edafacb690a3
child 27830 68de2a2780b3
produce XHTML 1.0 Transitional; tuned charset name; renamed Markup.class to Markup.tclass, to avoid potential conflicts with spacial meaning in markup languages (e.g. HTML);
src/Pure/Thy/html.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/Thy/html.ML	Mon Aug 11 18:37:49 2008 +0200
+++ b/src/Pure/Thy/html.ML	Mon Aug 11 18:37:51 2008 +0200
@@ -241,8 +241,7 @@
 
 fun span s = ("<span class=" ^ Library.quote (XML.text s) ^ ">", "</span>");
 
-val _ = Markup.add_mode htmlN (fn (name, props) =>
-  if name = Markup.classN then span "tclass" else span name);
+val _ = Markup.add_mode htmlN (fn (name, _) => span name);
 
 
 
@@ -270,29 +269,31 @@
   | href_opt_path (SOME p) txt = href_path p txt;
 
 fun para txt = "\n<p>" ^ txt ^ "</p>\n";
-fun preform txt = "<pre>" ^ txt ^ "</pre>";
+fun preform txt = "<pre xml:space=\"preserve\">" ^ txt ^ "</pre>";
 val verbatim = preform o output;
 
 
 (* document *)
 
-val charset = ref "iso-8859-1";
+val charset = ref "ISO-8859-1";
 fun with_charset s = setmp_noncritical charset s;
 
 fun begin_document title =
-  "<!DOCTYPE HTML PUBLIC \"-//W3C//DTD HTML 4.01 Transitional//EN\" \
-  \\"http://www.w3.org/TR/html4/loose.dtd\">\n\
-  \\n\
-  \<html>\n\
-  \<head>\n\
-  \<meta http-equiv=\"Content-Type\" content=\"text/html; charset=" ^ ! charset ^ "\">\n\
-  \<title>" ^ plain (title ^ " (" ^ Distribution.version ^ ")") ^ "</title>\n\
-  \<link rel=\"stylesheet\" type=\"text/css\" href=\"isabelle.css\">\n\
-  \</head>\n\
-  \\n\
-  \<body>\n\
-  \<div class=\"head\">\
-  \<h1>" ^ plain title ^ "</h1>\n"
+  let val cs = ! charset in
+    "<?xml version=\"1.0\" encoding=\"" ^ cs ^ "\" ?>\n\
+    \<!DOCTYPE HTML PUBLIC \"-//W3C//DTD XHTML 1.0 Transitional//EN\" \
+    \\"http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd\">\n\
+    \<html xmlns=\"http://www.w3.org/1999/xhtml\">\n\
+    \<head>\n\
+    \<meta http-equiv=\"Content-Type\" content=\"text/html; charset=" ^ cs ^ "\"/>\n\
+    \<title>" ^ plain (title ^ " (" ^ Distribution.version ^ ")") ^ "</title>\n\
+    \<link media=\"all\" rel=\"stylesheet\" type=\"text/css\" href=\"isabelle.css\"/>\n\
+    \</head>\n\
+    \\n\
+    \<body>\n\
+    \<div class=\"head\">\
+    \<h1>" ^ plain title ^ "</h1>\n"
+  end;
 
 val end_document = "\n</div>\n</body>\n</html>\n";
 
@@ -306,8 +307,8 @@
 fun begin_index up (index_path, session) docs graph =
   begin_document ("Index of " ^ session) ^ up_link up ^
   para ("View " ^ href_path graph "theory dependencies" ^
-    implode (map (fn (p, name) => "<br>\nView " ^ href_path p name) docs)) ^
-  "\n</div>\n<hr>\n<div class=\"theories\">\n<h2>Theories</h2>\n<ul>\n";
+    implode (map (fn (p, name) => "<br/>\nView " ^ href_path p name) docs)) ^
+  "\n</div>\n<hr/>\n<div class=\"theories\">\n<h2>Theories</h2>\n<ul>\n";
 
 val end_index = end_document;
 
@@ -329,32 +330,32 @@
         (name, begin_document ("Theory dependencies of " ^ session) ^
           back_link back ^
           para browser_size ^
-          "\n</div>\n<hr>\n<div class=\"graphbrowser\">\n\
+          "\n</div>\n<hr/>\n<div class=\"graphbrowser\">\n\
           \<applet code=\"GraphBrowser/GraphBrowser.class\" \
           \archive=\"GraphBrowser.jar\" \
           \width=" ^ width ^ " height=" ^ height ^ ">\n\
           \<param name=\"graphfile\" value=\"" ^ "session.graph" ^ "\">\n\
-          \</applet>\n<hr>" ^ end_document)
+          \</applet>\n<hr/>" ^ end_document)
       end;
   in map applet_page sizes end;
 
 
-fun entry (p, s) = "<li>" ^ href_path p (plain s) ^ "\n";
+fun entry (p, s) = "<li>" ^ href_path p (plain s) ^ "</li>\n";
 
 val theory_entry = entry;
 
 fun session_entries [] = "</ul>"
   | session_entries es =
-      "</ul>\n</div>\n<hr>\n<div class=\"sessions\">\n\
+      "</ul>\n</div>\n<hr/>\n<div class=\"sessions\">\n\
       \<h2>Sessions</h2>\n<ul>\n" ^ implode (map entry es) ^ "</ul>";
 
 
 (* theory *)
 
 fun verbatim_source ss =
-  "\n</div>\n<hr>\n<div class=\"source\">\n<pre>" ^
+  "\n</div>\n<hr/>\n<div class=\"source\">\n<pre xml:space=\"preserve\">" ^
   implode (output_symbols ss) ^
-  "</pre>\n</div>\n<hr>\n<div class=\"theorems\">\n";
+  "</pre>\n</div>\n<hr/>\n<div class=\"theorems\">\n";
 
 
 local
@@ -368,14 +369,14 @@
   fun imports Bs =
     keyword "imports" ^ " " ^ space_implode " " (map (uncurry href_opt_path o apsnd name) Bs);
 
-  fun uses Ps = keyword "uses" ^ " " ^ space_implode " " (map file Ps) ^ "<br>\n";
+  fun uses Ps = keyword "uses" ^ " " ^ space_implode " " (map file Ps) ^ "<br/>\n";
 in
 
 fun begin_theory up A Bs Ps body =
-  theory up A ^ "<br>\n" ^
-  imports Bs ^ "<br>\n" ^
+  theory up A ^ "<br/>\n" ^
+  imports Bs ^ "<br/>\n" ^
   (if null Ps then "" else uses Ps) ^
-  keyword "begin" ^ "<br>\n" ^
+  keyword "begin" ^ "<br/>\n" ^
   body;
 
 end;
@@ -387,9 +388,9 @@
 
 fun ml_file path str =
   begin_document ("File " ^ Url.implode path) ^
-  "\n</div>\n<hr><div class=\"mlsource\">\n" ^
+  "\n</div>\n<hr/><div class=\"mlsource\">\n" ^
   verbatim str ^
-  "\n</div>\n<hr>\n<div class=\"mlfooter\">\n" ^
+  "\n</div>\n<hr/>\n<div class=\"mlfooter\">\n" ^
   end_document;
isabelle