doc avec frames

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8469 85f007b7-540e-0410-9357-904b9bb8a0f7
author: mohring <mohring@85f007b7-540e-0410-9357-904b9bb8a0f7> 2004-01-06 16:52:44 +0000
committer: mohring <mohring@85f007b7-540e-0410-9357-904b9bb8a0f7> 2004-01-06 16:52:44 +0000
commit: c1466b54d098e4e410aefacd6317bf8fa40bb63c (patch)
tree: e968766a88726210d0e4a8c2ed365b0366280d39
parent: 3c94d3e2d09f6baa497aadba8f8c64bfd68a9ca9 (diff)
7 files changed, 67 insertions, 16 deletions
diff --git a/doc/Makefile b/doc/Makefile
index f330cdc6a..ede88a11d 100644
--- a/doc/Makefile
+++ b/doc/Makefile
@@ -154,8 +154,8 @@ doc-html.tar.gz: all-html
 	rm -rf coq-docs-html/*
 	cp Tutorial.v.html coq-docs-html/tutorial.html
 	cp Reference-Manual.html coqide-queries.png coqide.png coq-docs-html 
-	(cd coq-docs-html; hacha ./Reference-Manual.html; rm ./Reference-Manual.html)
-	cp cover.html coq-docs-html
+	(cd coq-docs-html; hacha -o toc.html ./Reference-Manual.html; rm ./Reference-Manual.html)
+	cp cover.html main.html main-0.html coq-docs-html
 	tar cf doc-html.tar coq-docs-html
 	gzip -f doc-html.tar
 
@@ -164,9 +164,9 @@ html-www: all-html
 	- $(MKDIR) www
 	rm -rf www/*
 	cp Tutorial.v.html www/tutorial.html
-	cp Reference-Manual.html  coqide-queries.png coqide.png www
-	(cd www; hacha ./Reference-Manual.html; rm ./Reference-Manual.html)
-	cp cover.html www
+	cp coqide-queries.png coqide.png www
+	(cd www; hacha -o toc.html ../Reference-Manual.html)
+	cp cover.html main.html main-0.html www
 
 
 clean-refman:
diff --git a/doc/Reference-Manual.tex b/doc/Reference-Manual.tex
index 2e6c45843..0b9a8cc25 100644
--- a/doc/Reference-Manual.tex
+++ b/doc/Reference-Manual.tex
@@ -10,6 +10,7 @@
 \usepackage{verbatim}
 \usepackage{amsmath}
 \usepackage{amssymb}
+\usepackage{hevea}
 
 % for coqide
 \ifx\pdfoutput\undefined   % si on est pas en pdflatex
@@ -32,13 +33,17 @@
 %END LATEX
 
 \tophtml{}
+%BEGIN LATEX
 \coverpage{Reference Manual}{The Coq Development Team}
+%END LATEX
 
 %\defaultheaders
 \include{RefMan-int}% Introduction
 \include{RefMan-pre}% Credits
 
+%BEGIN LATEX
 \tableofcontents
+%END LATEX
 
 \part{The language}
 \defaultheaders
@@ -85,14 +90,19 @@
 \nocite{*}
 \bibliographystyle{plain}
 \bibliography{biblio}
+\cutname{biblio.html}
 
 \printindex
+\cutname{general-index.html}
 
 \printindex[tactic]
+\cutname{tactic-index.html}
 
 \printindex[command]
+\cutname{command-index.html}
 
 \printindex[error]
+\cutname{error-index.html}
 
 %BEGIN LATEX
 \listoffigures
diff --git a/doc/cover.html b/doc/cover.html
index 56063de89..792f1129b 100644
--- a/doc/cover.html
+++ b/doc/cover.html
@@ -1,17 +1,11 @@
 <HTML>
 
 <HEAD>
-
 <TITLE>Cover Page</TITLE>
-
 </HEAD>
 
 <BODY>
 
-
-
-
-
 <DIV ALIGN=center>
 <FONT SIZE=7>
 </FONT><FONT SIZE=7><B>
@@ -20,7 +14,7 @@ The Coq Proof Assistant<BR><BR>
  Reference Manual<BR></B></FONT><FONT SIZE=7>
 </FONT>
 <BR><BR><FONT SIZE=5><B><BR></B></FONT><FONT SIZE=5><B>Version 8.0</B></FONT><FONT SIZE=5><B>
-</B></FONT><A NAME="text1"></A><A HREF="node.8.html#note1"><SUP><FONT SIZE=2>1</FONT></SUP></A><FONT SIZE=5><B><BR><BR><BR><BR><BR><BR><BR><BR><BR><BR><BR>
+</B></FONT><A NAME="text1"></A><A HREF="#note1"><SUP><FONT SIZE=2>1</FONT></SUP></A><FONT SIZE=5><B><BR><BR><BR><BR><BR><BR><BR><BR><BR><BR><BR>
 </B></FONT><FONT SIZE=5><B>The Coq Development Team</B></FONT><FONT SIZE=5><B><BR></B></FONT><FONT SIZE=5><B>LogiCal Project</B></FONT><FONT SIZE=5><B><BR><BR><BR>
 </B></FONT></DIV><BR>
 <BR><BR><BR><BR><BR><BR><BR><BR><BR><BR>
@@ -30,8 +24,8 @@ The Coq Proof Assistant<BR><BR>
 </FONT><BR><FONT SIZE=4>ŠINRIA 1999-2003</FONT><BR></DIV>
 <BR>
 
-
-
+<HR WIDTH="50%" SIZE=1><DL><DT><A NAME="note1" HREF="toc.html#text1"><FONT SIZE=5>1</FONT></A><DD>This research was partly supported by IST working group ``Types''
+</DL>
 
 </BODY>
 
diff --git a/doc/macros.tex b/doc/macros.tex
index 02dd1baef..e385381cd 100755
--- a/doc/macros.tex
+++ b/doc/macros.tex
@@ -6,6 +6,10 @@
 %\newcommand{\com}[1]{{\it(* #1 *)}}
 %\newcommand{\com}[1]{}
 
+%%OPTIONS for HACHA
+%\renewcommand{\cuttingunit}{section}
+
+
 %BEGIN LATEX
 \newenvironment{centerframe}%
 {\bgroup
diff --git a/doc/main-0.html b/doc/main-0.html
new file mode 100644
index 000000000..db19678f3
--- /dev/null
+++ b/doc/main-0.html
@@ -0,0 +1,29 @@
+<HTML>
+
+<BODY>
+
+<CENTER>
+
+<TABLE BORDER="0" CELLPADDING=10>
+<TR>
+<TD><CENTER><A HREF="cover.html" TARGET="UP"><FONT SIZE=2>Cover page</FONT></A></CENTER></TD>
+<TD><CENTER><A HREF="toc.html" TARGET="UP"><FONT SIZE=2>Table of contents</FONT></A></CENTER></TD>
+<TD><CENTER><A HREF="biblio.html" TARGET="UP"><FONT SIZE=2>
+Bibliography</FONT></A></CENTER></TD>
+<TD><CENTER><A HREF="general-index.html" TARGET="UP"><FONT SIZE=2>
+Global Index
+</FONT></A></CENTER></TD>
+<TD><CENTER><A HREF="tactic-index.html" TARGET="UP"><FONT SIZE=2>
+Tactics Index
+</FONT></A></CENTER></TD>
+<TD><CENTER><A HREF="command-index.html" TARGET="UP"><FONT SIZE=2>
+Vernacular Commands Index
+</FONT></A></CENTER></TD>
+<TD><CENTER><A HREF="error-index.html" TARGET="UP"><FONT SIZE=2>
+Index of Error Messages
+</FONT></A></CENTER></TD>
+</TABLE>
+
+</CENTER>
+
+</BODY></HTML>
+\ No newline at end of file
diff --git a/doc/main.html b/doc/main.html
new file mode 100644
index 000000000..1b5898298
--- /dev/null
+++ b/doc/main.html
@@ -0,0 +1,13 @@
+<HTML>
+
+<HEAD>
+
+<TITLE>The Coq Proof Assistant Reference Manual</TITLE>
+
+</HEAD>
+
+<FRAMESET ROWS=90%,*><FRAME SRC="cover.html" NAME="UP">
+<FRAME SRC="main-0.html">
+</FRAMESET>
+
+</HTML>
+\ No newline at end of file
diff --git a/doc/title.tex b/doc/title.tex
index 53ad9e0f8..d332af057 100755
--- a/doc/title.tex
+++ b/doc/title.tex
@@ -41,16 +41,16 @@ The Coq Proof Assistant\\
 {\Large \bf LogiCal Project}\\
 \vspace{15pt}
 \end{center}
-
 %BEGIN LATEX
 \newpage
 \vspace*{520pt}
 \thispagestyle{empty}
 %END LATEX
-
 \begin{flushleft}
+%BEGIN LATEX
 {\large{V\coqversion,
 \printingdate}}\\[20pt]
+%END LATEX
 {\large{\copyright INRIA 1999-2004}}\\
 \end{flushleft}
 %BEGIN LATEX
@@ -58,6 +58,7 @@ The Coq Proof Assistant\\
 %END LATEX
 }
 
+
 \newcommand{\shorttitle}[1]{
 \begin{center}
 \begin{huge}
author	mohring <mohring@85f007b7-540e-0410-9357-904b9bb8a0f7>	2004-01-06 16:52:44 +0000
committer	mohring <mohring@85f007b7-540e-0410-9357-904b9bb8a0f7>	2004-01-06 16:52:44 +0000
commit	c1466b54d098e4e410aefacd6317bf8fa40bb63c (patch)
tree	e968766a88726210d0e4a8c2ed365b0366280d39
parent	3c94d3e2d09f6baa497aadba8f8c64bfd68a9ca9 (diff)