--- a/Admin/makedist Tue Oct 30 10:51:35 2007 +0100
+++ b/Admin/makedist Tue Oct 30 10:51:35 2007 +0100
@@ -190,7 +190,7 @@
} >ANNOUNCE
fi
-perl -pi -e "s/{ISABELLE}/$DISTNAME/g;" lib/html/index.html
+perl -pi -e "s/{ISABELLE}/$DISTNAME/g;" lib/html/library_index_header.html
perl -pi -e "s/Isabelle repository version/$DISTVERSION/" src/Pure/ROOT.ML lib/Tools/version
perl -pi -e "s/the internal repository version of Isabelle/$DISTVERSION/" README
--- a/lib/Tools/usedir Tue Oct 30 10:51:35 2007 +0100
+++ b/lib/Tools/usedir Tue Oct 30 10:51:35 2007 +0100
@@ -183,7 +183,7 @@
# prepare browser info dir
-if [ "$INFO" = "true" -a ! -f "$ISABELLE_BROWSER_INFO/library_index_header.html" ]; then
+if [ "$INFO" = "true" -a ! -f "$ISABELLE_BROWSER_INFO/index.html" ]; then
mkdir -p "$ISABELLE_BROWSER_INFO"
cp "$ISABELLE_HOME/lib/logo/isabelle.gif" "$ISABELLE_BROWSER_INFO/isabelle.gif"
cat "$ISABELLE_HOME/lib/html/library_index_header.template" \
--- a/lib/html/index.html Tue Oct 30 10:51:35 2007 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,76 +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">
-<!-- $Id$ -->
-
-<html xmlns="http://www.w3.org/1999/xhtml">
-<head>
- <meta name="generator" content="HTML Tidy for Linux/x86 (vers 31 October 2006), see www.w3.org" />
- <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 />
-
- <ul>
- <li>Higher-Order Logic</li>
-
- <li style="list-style: none">
- <ul>
- <li><a href="HOL/index.html">HOL (Higher-Order Logic)</a></li>
-
- <li><a href="HOLCF/index.html">HOLCF (Higher-Order Logic of Computable Functions)</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></li>
-
- <li><a href="ZF/index.html">ZF (Set Theory)</a></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></li>
-
- <li><a href="Cube/index.html">Cube (The Lambda Cube)</a></li>
- </ul>
- </li>
- </ul>
-</body>
-</html>
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/html/library_index_content.template Tue Oct 30 10:51:35 2007 +0100
@@ -0,0 +1,44 @@
+ <ul>
+ <li>Higher-Order Logic</li>
+
+ <li style="list-style: none">
+ <ul>
+ <li><a href="HOL/index.html">HOL (Higher-Order Logic)</a></li>
+
+ <li><a href="HOLCF/index.html">HOLCF (Higher-Order Logic of Computable Functions)</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></li>
+
+ <li><a href="ZF/index.html">ZF (Set Theory)</a></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></li>
+
+ <li><a href="Cube/index.html">Cube (The Lambda Cube)</a></li>
+ </ul>
+ </li>
+ </ul>
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/html/library_index_footer.template Tue Oct 30 10:51:35 2007 +0100
@@ -0,0 +1,2 @@
+</body>
+</html>
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/html/library_index_header.template Tue Oct 30 10:51:35 2007 +0100
@@ -0,0 +1,28 @@
+<?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">
+<!-- $Id$ -->
+
+<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 />