doc-src/System/present.tex
author wenzelm
Wed, 14 May 1997 19:27:21 +0200
changeset 3188 445555a7b714
child 3217 d30d62128fe5
permissions -rw-r--r--
preliminary!
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
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
     9
with its ancestors and descendants. HTML stands for Hypertext Markup
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    10
Language and is used in the World Wide Web to represent text
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    11
containing images and links to other documents. Web browsers like
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    12
{\tt xmosaic} or {\tt netscape} are used to view these documents.
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
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    20
To make HTML files for logics that are part of the Isabelle
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    21
distribution, simply set the shell environment variable {\tt
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    22
MAKE_HTML} before compiling a logic. This works for single logics as
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    23
well as for the shell script {\tt make-all} (see
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    24
\ref{sec:shell-scripts}). To make HTML files for {\tt FOL} using a
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    25
{\tt csh} style shell, the following commands can be used:
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    26
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    27
\begin{ttbox}
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    28
cd FOL
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    29
setenv MAKE_HTML
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    30
make
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    31
\end{ttbox}
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    32
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    33
The databases made this way do not differ from the ones made with an
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    34
unset {\tt MAKE_HTML}; in particular no HTML files are written if the
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    35
database is used to manually load a theory.
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    36
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    37
As you will see below, the HTML generation is controlled by a boolean
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    38
reference variable. If you want to make databases which define this
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    39
variable's value as {\tt true} and where therefore HTML files are
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    40
written each time {\tt use_thy} is invoked, you have to set {\tt
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    41
MAKE_HTML} to ``{\tt true}'':
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    42
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    43
\begin{ttbox}
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    44
cd FOL
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    45
setenv MAKE_HTML true
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    46
make
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    47
\end{ttbox}
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    48
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    49
All theories loaded from within the {\tt FOL} database and all
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    50
databases derived from it will now cause HTML files to be written.
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    51
This behaviour can be changed by assigning a value of {\tt false} to
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    52
the boolean reference variable {\tt make_html}. Be careful when making
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    53
such databases publicly available since it means that your users will
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    54
generate HTML files though they might not intend to do so.
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    55
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    56
As some of Isabelle's logics are based on others (e.g. {\tt ZF} on
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    57
{\tt FOL}) and because the HTML files list a theory's ancestors, you
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    58
should not make HTML files for a logic if the HTML files for the base
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    59
logic do not exist. Otherwise some of the hypertext links might point
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    60
to non-existing documents.
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    61
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    62
The entry point to all logics is the {\tt index.html} file located in
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    63
Isabelle's main directory. You can also access a HTML version of the
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    64
distribution package at
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    65
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    66
\begin{ttbox}
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    67
http://www4.informatik.tu-muenchen.de/~nipkow/isabelle/
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    68
\end{ttbox}
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    69
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    70
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    71
\section*{Manual HTML generation}
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    72
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    73
To manually control the generation of HTML files the following
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    74
commands and reference variables are used:
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    75
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    76
\begin{ttbox}
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    77
init_html   : unit -> unit
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    78
make_html   : bool ref
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    79
finish_html : unit -> unit
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    80
\end{ttbox}
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    81
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    82
\begin{ttdescription}
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    83
\item[\ttindexbold{init_html}]
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    84
activates the HTML facility. It stores the current working directory
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    85
as the place where the {\tt index.html} file for all theories loaded
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    86
afterwards will be stored.
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    87
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    88
\item[\ttindexbold{make_html}]
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    89
is a boolean reference variable read by {\tt use_thy} and other
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    90
functions to decide whether HTML files should be made. After you have
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    91
used {\tt init_html} you can manually change {\tt make_html}'s value
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    92
to temporarily disable HTML generation.
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    93
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    94
\item[\ttindexbold{finish_html}]
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    95
has to be called after all theories have been read that should be
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    96
listed in the current {\tt index.html} file. It reads a temporary
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    97
file with information about the theories read since the last use of
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    98
{\tt init_html} and makes the {\tt index.html} file. If {\tt
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    99
make_html} is {\tt false} nothing is done.
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   100
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   101
The indexes made by this function also contain a link to the {\tt
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   102
README} file if there exists one in the directory where the index is
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   103
stored. If there's a {\tt README.html} file it is used instead of
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   104
{\tt README}.
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   105
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   106
\end{ttdescription}
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   107
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   108
The above functions could be used in the following way:
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   109
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   110
\begin{ttbox}
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   111
init_html();
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   112
{\out Setting path for index.html to "/home/clasohm/isabelle/HOL"}
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   113
use_thy "List";
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   114
\dots
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   115
finish_html();
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   116
\end{ttbox}
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   117
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   118
Please note that HTML files are made only for those theories that are
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   119
read while {\tt make_html} is {\tt true}. These files may contain
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   120
links to theories that were read with a {\tt false} {\tt make_html}
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   121
and therefore point to non-existing files.
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   122
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   123
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   124
\section*{Extending or adding a logic}
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   125
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   126
If you add a new subdirectory to Isabelle's logics (or add a completly
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   127
new logic), you would have to call {\tt init_html} at the start of every
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   128
directory's {\tt ROOT.ML} file and {\tt finish_html} at the end of
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   129
it. This is automatically done if you use
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   130
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   131
\begin{ttbox}\index{*use_dir}
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   132
use_dir : string -> unit
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   133
\end{ttbox}
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   134
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   135
This function takes a path as its parameter, changes the working
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   136
directory, calls {\tt init_html} if {\tt make_html} is {\tt true},
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   137
executes {\tt ROOT.ML}, and calls {\tt finish_html}. The {\tt
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   138
index.html} file written in this directory will be automatically
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   139
linked to the first index found in the (recursively searched)
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   140
superdirectories.
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   141
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   142
Instead of adding something like
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   143
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   144
\begin{ttbox}
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   145
use"ex/ROOT.ML";
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   146
\end{ttbox}
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   147
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   148
to the logic's makefile you have to use this:
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   149
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   150
\begin{ttbox}
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   151
use_dir"ex";
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   152
\end{ttbox}
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   153
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   154
Since {\tt use_dir} calls {\tt init_html} only if {\tt make_html} is
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   155
{\tt true} the generation of HTML files depends on the value this
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   156
reference variable has. It can either be inherited from the used \ML{}
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   157
database or set in the makefile before {\tt use_dir} is invoked,
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   158
e.g. to set it's value according to the environment variable {\tt
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   159
MAKE_HTML}.
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   160
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   161
The generated HTML files contain all theorems that were proved in the
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   162
theory's \ML{} file with {\tt qed}, {\tt qed_goal} and {\tt qed_goalw},
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   163
or stored with {\tt bind_thm} and {\tt store_thm}. Additionally there
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   164
is a hypertext link to the whole \ML{} file.
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   165
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   166
You can add section headings to the list of theorems by using
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   167
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   168
\begin{ttbox}\index{*use_dir}
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   169
section: string -> unit
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   170
\end{ttbox}
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   171
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   172
in a theory's ML file, which converts a plain string to a HTML
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   173
heading and inserts it before the next theorem proved or stored with
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   174
one of the above functions. If {\tt make_html} is {\tt false} nothing
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   175
is done.
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   176
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   177
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   178
\section*{Using someone else's database}
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   179
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   180
To make them independent from their storage place, the HTML files only
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   181
contain relative paths which are derived from absolute ones like the
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   182
current working directory, {\tt gif_path} or {\tt base_path}. The
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   183
latter two are reference variables which are initialized at the time
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   184
when the {\tt Pure} database is made. Because you need write access
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   185
for the current directory to make HTML files and therefore (probably)
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   186
generate them in your home directory, the absolute {\tt base_path} is
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   187
not correct if you use someone else's database or a database derived
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   188
from it.
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   189
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   190
In that case you first should set {\tt base_path} to the value of {\em
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   191
your} Isabelle main directory, i.e. the directory that contains the
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   192
subdirectories where standard logics like {\tt FOL} and {\tt HOL} or
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   193
your own logics are stored. If you do not do this, the generated HTML
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   194
files will still be usable but may contain incomplete titles and lack
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   195
some hypertext links.
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   196
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   197
It's also a good idea to set {\tt gif_path} which points to the
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   198
directory containing two GIF images used in the HTML
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   199
documents. Normally this is the {\tt Tools} subdirectory of Isabelle's
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   200
main directory. While its value in general is still valid, your HTML
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   201
files would depend on files not owned by you. This prevents you from
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   202
changing the location of the HTML files (as they contain relative
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   203
paths) and also causes trouble if the database's maker (re)moves the
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   204
GIFs.
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   205
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   206
Here's what you should do before invoking {\tt init_html} using
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   207
someone else's \ML{} database:
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   208
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   209
\begin{ttbox}
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   210
base_path := "/home/smith/isabelle";
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   211
gif_path := "/home/smith/isabelle/Tools";
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   212
init_html();
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   213
\dots
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   214
\end{ttbox}