clarified HTML template (see also 04cb7e02ca38): avoid odd patching of sources;
authorwenzelm
Thu, 01 Apr 2021 19:01:19 +0200
changeset 73783 c337c798f64c
parent 73782 c72fd8f1fceb
child 73784 cf1a1e92bf34
clarified HTML template (see also 04cb7e02ca38): avoid odd patching of sources;
lib/html/library_index_content.template
lib/html/library_index_footer.template
lib/html/library_index_header.template
src/Pure/Admin/build_release.scala
src/Pure/PIDE/xml.scala
src/Pure/Thy/presentation.scala
--- a/lib/html/library_index_content.template	Thu Apr 01 07:35:03 2021 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,54 +0,0 @@
-  <ul>
-    <li>Higher-Order Logic</li>
-
-    <li style="list-style: none">
-      <ul>
-        <li><a href="HOL/index.html">HOL (Higher-Order Logic)</a>
-        is a version of classical higher-order logic resembling
-        that of the <a href="http://www.cl.cam.ac.uk/Research/HVG/HOL/">HOL System</a>.
-        </li>
-      </ul>
-    </li>
-  </ul>
-
-  <ul>
-    <li>First-Order Logic</li>
-
-    <li style="list-style: none">
-      <ul>
-        <li><a href="FOL/index.html">FOL (Many-sorted First-Order Logic)</a>
-        provides basic classical and intuitionistic first-order logic. It is
-        polymorphic.
-        </li>
-
-        <li><a href="ZF/index.html">ZF (Set Theory)</a>
-        offers a formulation of Zermelo-Fraenkel set theory on top of FOL.
-        </li>
-
-        <li><a href="CCL/index.html">CCL (Classical Computational Logic)</a></li>
-
-        <li><a href="LCF/index.html">LCF (Logic of Computable Functions)</a></li>
-
-        <li><a href="FOLP/index.html">FOLP (FOL with Proof Terms)</a></li>
-      </ul>
-    </li>
-  </ul>
-
-  <ul>
-    <li>Miscellaneous</li>
-
-    <li style="list-style: none">
-      <ul>
-        <li><a href="Sequents/index.html">Sequents (first-order, modal and linear logics)</a></li>
-
-        <li><a href="CTT/index.html">CTT (Constructive Type Theory)</a>
-        is an extensional version of Martin-L&ouml;f's Type Theory.</li>
-
-        <li><a href="Cube/index.html">Cube (The Lambda Cube)</a></li>
-
-        <li><a href="Pure/index.html">The Pure logical framework</a></li>
-
-        <li><a href="Doc/index.html">Sources of Documentation</a></li>
-      </ul>
-    </li>
-  </ul>
--- a/lib/html/library_index_footer.template	Thu Apr 01 07:35:03 2021 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,2 +0,0 @@
-</body>
-</html>
--- a/lib/html/library_index_header.template	Thu Apr 01 07:35:03 2021 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,27 +0,0 @@
-<?xml version="1.0" encoding="iso-8859-1"?>
-<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN"
-    "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
-
-<html xmlns="http://www.w3.org/1999/xhtml">
-<head>
-  <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1" />
-  <title>The {ISABELLE} Library</title>
-</head>
-
-<body text="#000000" bgcolor="#FFFFFF" link="#0000FF" vlink="#000099" alink="#404040">
-  <center>
-    <table width="100%" border="0" cellspacing="10" cellpadding="0">
-      <tr>
-        <td width="20%" valign="middle" align="center"><a href="http://isabelle.in.tum.de/"><img align="bottom" src="isabelle.gif" width="100" height="86" alt="[Isabelle]" border="0" /></a></td>
-
-        <td width="80%" valign="middle" align="center">
-          <table width="90%" border="0" cellspacing="0" cellpadding="20">
-            <tr>
-              <td valign="middle" align="center" bgcolor="#AACCCC"><font face="Helvetica,Arial" size="+2">The {ISABELLE} Library</font></td>
-            </tr>
-          </table>
-        </td>
-      </tr>
-    </table>
-  </center>
-  <hr />
--- a/src/Pure/Admin/build_release.scala	Thu Apr 01 07:35:03 2021 +0200
+++ b/src/Pure/Admin/build_release.scala	Thu Apr 01 19:01:19 2021 +0200
@@ -59,9 +59,6 @@
   {
     val dir = release.isabelle_dir
 
-    File.change(dir + Path.explode("lib/html/library_index_header.template"),
-      _.replace("{ISABELLE}", release.dist_name))
-
     File.change(dir + Path.explode("README"),
       _.replace("some repository version of Isabelle", release.dist_version))
   }
--- a/src/Pure/PIDE/xml.scala	Thu Apr 01 07:35:03 2021 +0200
+++ b/src/Pure/PIDE/xml.scala	Thu Apr 01 19:01:19 2021 +0200
@@ -190,6 +190,7 @@
 
   def string_of_tree(tree: XML.Tree): String = string_of_body(List(tree))
 
+  def text(s: String): String = string_of_tree(XML.Text(s))
 
 
   /** cache **/
--- a/src/Pure/Thy/presentation.scala	Thu Apr 01 07:35:03 2021 +0200
+++ b/src/Pure/Thy/presentation.scala	Thu Apr 01 19:01:19 2021 +0200
@@ -367,10 +367,92 @@
       Isabelle_System.make_directory(browser_info)
       Isabelle_System.copy_file(Path.explode("~~/lib/logo/isabelle.gif"),
         browser_info + Path.explode("isabelle.gif"))
+      val title = "The " + XML.text(Isabelle_System.isabelle_name()) + " Library"
       File.write(browser_info + Path.explode("index.html"),
-        File.read(Path.explode("~~/lib/html/library_index_header.template")) +
-        File.read(Path.explode("~~/lib/html/library_index_content.template")) +
-        File.read(Path.explode("~~/lib/html/library_index_footer.template")))
+"""<?xml version="1.0" encoding="iso-8859-1"?>
+<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN"
+    "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
+
+<html xmlns="http://www.w3.org/1999/xhtml">
+<head>
+  <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1" />
+  <title>""" + title + """</title>
+</head>
+
+<body text="#000000" bgcolor="#FFFFFF" link="#0000FF" vlink="#000099" alink="#404040">
+  <center>
+    <table width="100%" border="0" cellspacing="10" cellpadding="0">
+      <tr>
+        <td width="20%" valign="middle" align="center"><a href="http://isabelle.in.tum.de/"><img align="bottom" src="isabelle.gif" width="100" height="86" alt="[Isabelle]" border="0" /></a></td>
+
+        <td width="80%" valign="middle" align="center">
+          <table width="90%" border="0" cellspacing="0" cellpadding="20">
+            <tr>
+              <td valign="middle" align="center" bgcolor="#AACCCC"><font face="Helvetica,Arial" size="+2">""" + title + """</font></td>
+            </tr>
+          </table>
+        </td>
+      </tr>
+    </table>
+  </center>
+  <hr />
+  <ul>
+    <li>Higher-Order Logic</li>
+
+    <li style="list-style: none">
+      <ul>
+        <li><a href="HOL/index.html">HOL (Higher-Order Logic)</a>
+        is a version of classical higher-order logic resembling
+        that of the <a href="http://www.cl.cam.ac.uk/Research/HVG/HOL/">HOL System</a>.
+        </li>
+      </ul>
+    </li>
+  </ul>
+
+  <ul>
+    <li>First-Order Logic</li>
+
+    <li style="list-style: none">
+      <ul>
+        <li><a href="FOL/index.html">FOL (Many-sorted First-Order Logic)</a>
+        provides basic classical and intuitionistic first-order logic. It is
+        polymorphic.
+        </li>
+
+        <li><a href="ZF/index.html">ZF (Set Theory)</a>
+        offers a formulation of Zermelo-Fraenkel set theory on top of FOL.
+        </li>
+
+        <li><a href="CCL/index.html">CCL (Classical Computational Logic)</a></li>
+
+        <li><a href="LCF/index.html">LCF (Logic of Computable Functions)</a></li>
+
+        <li><a href="FOLP/index.html">FOLP (FOL with Proof Terms)</a></li>
+      </ul>
+    </li>
+  </ul>
+
+  <ul>
+    <li>Miscellaneous</li>
+
+    <li style="list-style: none">
+      <ul>
+        <li><a href="Sequents/index.html">Sequents (first-order, modal and linear logics)</a></li>
+
+        <li><a href="CTT/index.html">CTT (Constructive Type Theory)</a>
+        is an extensional version of Martin-L&ouml;f's Type Theory.</li>
+
+        <li><a href="Cube/index.html">Cube (The Lambda Cube)</a></li>
+
+        <li><a href="Pure/index.html">The Pure logical framework</a></li>
+
+        <li><a href="Doc/index.html">Sources of Documentation</a></li>
+      </ul>
+    </li>
+  </ul>
+</body>
+</html>
+""")
     }
   }