doc-src/System/present.tex
author wenzelm
Thu, 17 Jul 1997 15:03:38 +0200
changeset 3524 c02cb15830de
parent 3217 d30d62128fe5
child 3753 5fd734bed0d4
permissions -rw-r--r--
fixed EqI meta rule;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
3188
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
     1
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
     2
\chapter{Presenting theories}
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
     3
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
     4
\section{Generating HTML documents} \label{sec:html}
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
     5
\index{HTML|bold} 
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
     6
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
     7
Isabelle is able to make HTML documents that show a theory's
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
     8
definition, the theorems proved in its ML file and the relationship
3217
d30d62128fe5 still under construction!
wenzelm
parents: 3188
diff changeset
     9
with its ancestors and descendants. HTML is the hypertext markup
d30d62128fe5 still under construction!
wenzelm
parents: 3188
diff changeset
    10
language used on the World Wide Web to represent text containing
d30d62128fe5 still under construction!
wenzelm
parents: 3188
diff changeset
    11
images and links to other documents.  These documents may be viewed
d30d62128fe5 still under construction!
wenzelm
parents: 3188
diff changeset
    12
using Web browsers like Netscape or Lynx.
3188
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    13
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    14
Besides the three HTML files that are made for every theory
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    15
(definition and theorems, ancestors, descendants), Isabelle stores
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    16
links to all theories in an index file. These indexes are themself
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    17
linked with other indexes to represent the hierarchic structure of
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    18
Isabelle's logics.
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    19
3217
d30d62128fe5 still under construction!
wenzelm
parents: 3188
diff changeset
    20
\medskip To make HTML files for logics that are part of the Isabelle
d30d62128fe5 still under construction!
wenzelm
parents: 3188
diff changeset
    21
distribution, simply append ``\texttt{-h true}'' to the
d30d62128fe5 still under construction!
wenzelm
parents: 3188
diff changeset
    22
\texttt{ISABELLE_USEDIR_OPTIONS} setting before making a logic.  For
d30d62128fe5 still under construction!
wenzelm
parents: 3188
diff changeset
    23
example, to generate HTML files for {\FOL}, first add something like
d30d62128fe5 still under construction!
wenzelm
parents: 3188
diff changeset
    24
this to your \texttt{\~\relax/isabelle/etc/settings} file:
3188
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    25
\begin{ttbox}
3217
d30d62128fe5 still under construction!
wenzelm
parents: 3188
diff changeset
    26
ISABELLE_USEDIR_OPTIONS="-h true"
3188
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    27
\end{ttbox}
3217
d30d62128fe5 still under construction!
wenzelm
parents: 3188
diff changeset
    28
Then \texttt{cd} into the \texttt{src/FOL} directory of the Isabelle
d30d62128fe5 still under construction!
wenzelm
parents: 3188
diff changeset
    29
distribution and do an \texttt{isatool make} (or even \texttt{isatool
d30d62128fe5 still under construction!
wenzelm
parents: 3188
diff changeset
    30
  make test}).
3188
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    31
3217
d30d62128fe5 still under construction!
wenzelm
parents: 3188
diff changeset
    32
\medskip As some of Isabelle's logics are based on others (e.g. {\tt
d30d62128fe5 still under construction!
wenzelm
parents: 3188
diff changeset
    33
  ZF} on {\tt FOL}) and because the HTML files list a theory's
d30d62128fe5 still under construction!
wenzelm
parents: 3188
diff changeset
    34
ancestors, you should not make HTML files for a logic if the HTML
d30d62128fe5 still under construction!
wenzelm
parents: 3188
diff changeset
    35
files for the base logic do not exist. Otherwise some of the hypertext
d30d62128fe5 still under construction!
wenzelm
parents: 3188
diff changeset
    36
links might point to non-existing documents.
3188
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    37
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    38
The entry point to all logics is the {\tt index.html} file located in
3217
d30d62128fe5 still under construction!
wenzelm
parents: 3188
diff changeset
    39
Isabelle's main directory.
3188
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    40
3217
d30d62128fe5 still under construction!
wenzelm
parents: 3188
diff changeset
    41
A complete HTML version of all distributed Isabelle object-logics and
d30d62128fe5 still under construction!
wenzelm
parents: 3188
diff changeset
    42
examples may be accessed on the WWW at:
3188
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    43
\begin{ttbox}
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    44
http://www4.informatik.tu-muenchen.de/~nipkow/isabelle/
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    45
\end{ttbox}
3217
d30d62128fe5 still under construction!
wenzelm
parents: 3188
diff changeset
    46
Note that this is not necessarily consistent with your local sources!
3188
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    47
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    48
3217
d30d62128fe5 still under construction!
wenzelm
parents: 3188
diff changeset
    49
\section*{*HTML generation internals}
3188
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    50
3217
d30d62128fe5 still under construction!
wenzelm
parents: 3188
diff changeset
    51
The generation of HTML files is controlled by the following {\ML}
d30d62128fe5 still under construction!
wenzelm
parents: 3188
diff changeset
    52
commands and reference variables:
3188
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    53
\begin{ttbox}
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    54
init_html   : unit -> unit
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    55
make_html   : bool ref
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    56
finish_html : unit -> unit
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    57
\end{ttbox}
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    58
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    59
\begin{ttdescription}
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    60
\item[\ttindexbold{init_html}]
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    61
activates the HTML facility. It stores the current working directory
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    62
as the place where the {\tt index.html} file for all theories loaded
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    63
afterwards will be stored.
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    64
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    65
\item[\ttindexbold{make_html}]
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    66
is a boolean reference variable read by {\tt use_thy} and other
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    67
functions to decide whether HTML files should be made. After you have
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    68
used {\tt init_html} you can manually change {\tt make_html}'s value
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    69
to temporarily disable HTML generation.
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    70
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    71
\item[\ttindexbold{finish_html}]
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    72
has to be called after all theories have been read that should be
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    73
listed in the current {\tt index.html} file. It reads a temporary
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    74
file with information about the theories read since the last use of
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    75
{\tt init_html} and makes the {\tt index.html} file. If {\tt
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    76
make_html} is {\tt false} nothing is done.
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    77
3217
d30d62128fe5 still under construction!
wenzelm
parents: 3188
diff changeset
    78
The indexes made by this function also contain a link to the
d30d62128fe5 still under construction!
wenzelm
parents: 3188
diff changeset
    79
\texttt{README.html} or \texttt{README} file if there exists one in
d30d62128fe5 still under construction!
wenzelm
parents: 3188
diff changeset
    80
the directory where the index is stored. If there's a {\tt
d30d62128fe5 still under construction!
wenzelm
parents: 3188
diff changeset
    81
  README.html} file it is used instead of {\tt README}.
3188
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    82
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    83
\end{ttdescription}
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    84
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    85
The above functions could be used in the following way:
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    86
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    87
\begin{ttbox}
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    88
init_html();
3217
d30d62128fe5 still under construction!
wenzelm
parents: 3188
diff changeset
    89
{\out Setting path for index.html to "/home/me/Isabelle-dist/src/HOL"}
3188
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    90
use_thy "List";
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    91
\dots
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    92
finish_html();
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    93
\end{ttbox}
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    94
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    95
Please note that HTML files are made only for those theories that are
3217
d30d62128fe5 still under construction!
wenzelm
parents: 3188
diff changeset
    96
read while \texttt{make_html} is \texttt{true}. These files may
d30d62128fe5 still under construction!
wenzelm
parents: 3188
diff changeset
    97
contain links to theories that were read with a \texttt{make_html} set
d30d62128fe5 still under construction!
wenzelm
parents: 3188
diff changeset
    98
to \texttt{false} and therefore point to non-existing files.
3188
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    99
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   100
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   101
\section*{Extending or adding a logic}
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   102
3217
d30d62128fe5 still under construction!
wenzelm
parents: 3188
diff changeset
   103
If you add a new subdirectory to Isabelle's logics (or add a
d30d62128fe5 still under construction!
wenzelm
parents: 3188
diff changeset
   104
completely new logic), you would have to call {\tt init_html} at the
d30d62128fe5 still under construction!
wenzelm
parents: 3188
diff changeset
   105
start of every directory's {\tt ROOT.ML} file and {\tt finish_html} at
d30d62128fe5 still under construction!
wenzelm
parents: 3188
diff changeset
   106
the end of it. This is automatically done if you use
3188
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   107
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   108
\begin{ttbox}\index{*use_dir}
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   109
use_dir : string -> unit
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   110
\end{ttbox}
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   111
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   112
This function takes a path as its parameter, changes the working
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   113
directory, calls {\tt init_html} if {\tt make_html} is {\tt true},
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   114
executes {\tt ROOT.ML}, and calls {\tt finish_html}. The {\tt
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   115
index.html} file written in this directory will be automatically
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   116
linked to the first index found in the (recursively searched)
3217
d30d62128fe5 still under construction!
wenzelm
parents: 3188
diff changeset
   117
super directories.
3188
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   118
3217
d30d62128fe5 still under construction!
wenzelm
parents: 3188
diff changeset
   119
The \texttt{usedir} utility (see also \S\ref{sec:tool-usedir}) will
d30d62128fe5 still under construction!
wenzelm
parents: 3188
diff changeset
   120
automatically take care of this.
3188
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   121
3217
d30d62128fe5 still under construction!
wenzelm
parents: 3188
diff changeset
   122
\medskip The generated HTML files contain all theorems that were
d30d62128fe5 still under construction!
wenzelm
parents: 3188
diff changeset
   123
proved in the theory's \ML{} file with {\tt qed}, {\tt qed_goal} and
d30d62128fe5 still under construction!
wenzelm
parents: 3188
diff changeset
   124
{\tt qed_goalw}, or stored with {\tt bind_thm} and {\tt store_thm}.
d30d62128fe5 still under construction!
wenzelm
parents: 3188
diff changeset
   125
Additionally, there is a hypertext link to the whole \ML{} file.
3188
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   126
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   127
You can add section headings to the list of theorems by using
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   128
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   129
\begin{ttbox}\index{*use_dir}
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   130
section: string -> unit
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   131
\end{ttbox}
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   132
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   133
in a theory's ML file, which converts a plain string to a HTML
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   134
heading and inserts it before the next theorem proved or stored with
3217
d30d62128fe5 still under construction!
wenzelm
parents: 3188
diff changeset
   135
one of the above functions.
3188
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   136
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   137
3217
d30d62128fe5 still under construction!
wenzelm
parents: 3188
diff changeset
   138
\section*{*Using someone else's database}
3188
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   139
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   140
To make them independent from their storage place, the HTML files only
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   141
contain relative paths which are derived from absolute ones like the
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   142
current working directory, {\tt gif_path} or {\tt base_path}. The
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   143
latter two are reference variables which are initialized at the time
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   144
when the {\tt Pure} database is made. Because you need write access
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   145
for the current directory to make HTML files and therefore (probably)
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   146
generate them in your home directory, the absolute {\tt base_path} is
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   147
not correct if you use someone else's database or a database derived
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   148
from it.
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   149
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   150
In that case you first should set {\tt base_path} to the value of {\em
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   151
your} Isabelle main directory, i.e. the directory that contains the
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   152
subdirectories where standard logics like {\tt FOL} and {\tt HOL} or
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   153
your own logics are stored. If you do not do this, the generated HTML
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   154
files will still be usable but may contain incomplete titles and lack
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   155
some hypertext links.
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   156
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   157
It's also a good idea to set {\tt gif_path} which points to the
3217
d30d62128fe5 still under construction!
wenzelm
parents: 3188
diff changeset
   158
directory containing two GIF images used in the HTML documents.
d30d62128fe5 still under construction!
wenzelm
parents: 3188
diff changeset
   159
Normally this is the \texttt{src/Tools} subdirectory of Isabelle's
3188
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   160
main directory. While its value in general is still valid, your HTML
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   161
files would depend on files not owned by you. This prevents you from
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   162
changing the location of the HTML files (as they contain relative
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   163
paths) and also causes trouble if the database's maker (re)moves the
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   164
GIFs.
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   165
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   166
Here's what you should do before invoking {\tt init_html} using
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   167
someone else's \ML{} database:
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   168
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   169
\begin{ttbox}
3217
d30d62128fe5 still under construction!
wenzelm
parents: 3188
diff changeset
   170
base_path := "/home/someone/Isabelle-dist/src";
d30d62128fe5 still under construction!
wenzelm
parents: 3188
diff changeset
   171
gif_path := "/home/someone/Isabelle-dist/src/Tools";
3188
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   172
init_html();
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   173
\dots
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   174
\end{ttbox}