doc-src/System/present.tex
author paulson
Fri, 27 Nov 1998 13:13:22 +0100
changeset 5980 2e9314c07146
parent 5364 ffa6d795c4b3
child 6148 d97a944c6ea3
permissions -rw-r--r--
added Real/Hyperreal
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
4540
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
     1
3753
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
     2
%% $Id$
3188
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
     3
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
     4
\chapter{Presenting theories}
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
     5
3753
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
     6
\section{Generating theory browsing information} \label{sec:info}
4540
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
     7
\index{theory browsing information|bold}
3188
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
     8
4540
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
     9
Isabelle is able to generate theory browsing information, such as HTML
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
    10
documents that show a theory's definition, the theorems proved in its
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
    11
ML file and the relationship with its ancestors and descendants. HTML
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
    12
is the hypertext markup language used on the World Wide Web to
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
    13
represent text containing links to other documents.  These documents
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
    14
may be viewed using Web browsers like Netscape or Lynx.
3188
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    15
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    16
Besides the three HTML files that are made for every theory
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    17
(definition and theorems, ancestors, descendants), Isabelle stores
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    18
links to all theories in an index file. These indexes are themself
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    19
linked with other indexes to represent the hierarchic structure of
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    20
Isabelle's logics.
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    21
4555
wenzelm
parents: 4540
diff changeset
    22
In addition to the HTML files, Isabelle also generates \emph{graph}
4540
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
    23
files that represent the theory hierarchy of a logic.  These graphs
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
    24
can be comfortably displayed by a graph browser Java applet embedded
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
    25
in the generated HTML pages. There is also a stand-alone version of
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
    26
the graph browser which allows browsing theory graphs without having
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
    27
to start a Web browser first. This version also includes features such
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
    28
as generating {\sc PostScript} files, which are not available in the
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
    29
applet version. The graph browser will be described later in this
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
    30
chapter.
3753
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
    31
4540
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
    32
\medskip To generate theory browsing information for logics that are
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
    33
part of the Isabelle distribution, simply append ``\texttt{-i true}''
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
    34
to the \settdx{ISABELLE_USEDIR_OPTIONS} setting before making a logic.
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
    35
For example, to generate browsing information for {\FOL}, first add
4555
wenzelm
parents: 4540
diff changeset
    36
something like this to your Isabelle settings file:
3188
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    37
\begin{ttbox}
3753
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
    38
ISABELLE_USEDIR_OPTIONS="-i true"
3188
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    39
\end{ttbox}
3217
d30d62128fe5 still under construction!
wenzelm
parents: 3188
diff changeset
    40
Then \texttt{cd} into the \texttt{src/FOL} directory of the Isabelle
4555
wenzelm
parents: 4540
diff changeset
    41
distribution and do \texttt{isatool make} (or even \texttt{isatool
wenzelm
parents: 4540
diff changeset
    42
  make all}).
3753
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
    43
4540
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
    44
\medskip The directory in which to store theory browsing information
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
    45
is determined by the \settdx{ISABELLE_BROWSER_INFO} setting.
3188
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    46
3217
d30d62128fe5 still under construction!
wenzelm
parents: 3188
diff changeset
    47
\medskip As some of Isabelle's logics are based on others (e.g. {\tt
d30d62128fe5 still under construction!
wenzelm
parents: 3188
diff changeset
    48
  ZF} on {\tt FOL}) and because the HTML files list a theory's
d30d62128fe5 still under construction!
wenzelm
parents: 3188
diff changeset
    49
ancestors, you should not make HTML files for a logic if the HTML
d30d62128fe5 still under construction!
wenzelm
parents: 3188
diff changeset
    50
files for the base logic do not exist. Otherwise some of the hypertext
d30d62128fe5 still under construction!
wenzelm
parents: 3188
diff changeset
    51
links might point to non-existing documents.
3188
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    52
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    53
The entry point to all logics is the {\tt index.html} file located in
3753
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
    54
the directory denoted by \texttt{ISABELLE_BROWSER_INFO}.
3188
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    55
3217
d30d62128fe5 still under construction!
wenzelm
parents: 3188
diff changeset
    56
A complete HTML version of all distributed Isabelle object-logics and
d30d62128fe5 still under construction!
wenzelm
parents: 3188
diff changeset
    57
examples may be accessed on the WWW at:
3188
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    58
\begin{ttbox}
3753
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
    59
http://www4.informatik.tu-muenchen.de/~isabelle/library/
3188
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    60
\end{ttbox}
4555
wenzelm
parents: 4540
diff changeset
    61
Of course, this is not necessarily consistent with your local version!
3188
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    62
3753
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
    63
To present your own theories on the WWW, simply copy the whole
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
    64
\texttt{ISABELLE_BROWSER_INFO} directory to your WWW server.
3188
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    65
4540
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
    66
3753
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
    67
\section{Extending or adding a logic}
3188
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    68
3217
d30d62128fe5 still under construction!
wenzelm
parents: 3188
diff changeset
    69
If you add a new subdirectory to Isabelle's logics (or add a
3753
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
    70
completely new logic), provide a {\tt ROOT.ML} file which reads in the
4540
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
    71
theory files. The {\tt ROOT.ML} file will then be processed via the
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
    72
function
3188
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    73
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    74
\begin{ttbox}\index{*use_dir}
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    75
use_dir : string -> unit
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    76
\end{ttbox}
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    77
4540
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
    78
which takes a path as its parameter, changes the working directory,
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
    79
executes {\tt ROOT.ML}, and makes sure that theory browsing
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
    80
information is generated properly. The {\tt index.html} file written
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
    81
in this directory will be automatically linked to the first index
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
    82
found in the (recursively searched) super directories.
3188
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    83
3217
d30d62128fe5 still under construction!
wenzelm
parents: 3188
diff changeset
    84
The \texttt{usedir} utility (see also \S\ref{sec:tool-usedir}) will
d30d62128fe5 still under construction!
wenzelm
parents: 3188
diff changeset
    85
automatically take care of this.
3188
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    86
3217
d30d62128fe5 still under construction!
wenzelm
parents: 3188
diff changeset
    87
\medskip The generated HTML files contain all theorems that were
d30d62128fe5 still under construction!
wenzelm
parents: 3188
diff changeset
    88
proved in the theory's \ML{} file with {\tt qed}, {\tt qed_goal} and
d30d62128fe5 still under construction!
wenzelm
parents: 3188
diff changeset
    89
{\tt qed_goalw}, or stored with {\tt bind_thm} and {\tt store_thm}.
d30d62128fe5 still under construction!
wenzelm
parents: 3188
diff changeset
    90
Additionally, there is a hypertext link to the whole \ML{} file.
3188
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    91
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    92
You can add section headings to the list of theorems by using
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    93
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    94
\begin{ttbox}\index{*use_dir}
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    95
section: string -> unit
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    96
\end{ttbox}
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
    97
4540
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
    98
in a theory's ML file, which converts a plain string to a HTML heading
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
    99
and inserts it before the next theorem proved or stored with one of
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   100
the above functions.
3188
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   101
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   102
3753
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
   103
%\section*{*Using someone else's database}
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
   104
%
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
   105
%To make them independent from their storage place, the HTML files only
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
   106
%contain relative paths which are derived from absolute ones like the
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
   107
%current working directory, {\tt gif_path} or {\tt base_path}. The
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
   108
%latter two are reference variables which are initialized at the time
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
   109
%when the {\tt Pure} database is made. Because you need write access
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
   110
%for the current directory to make HTML files and therefore (probably)
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
   111
%generate them in your home directory, the absolute {\tt base_path} is
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
   112
%not correct if you use someone else's database or a database derived
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
   113
%from it.
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
   114
%
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
   115
%In that case you first should set {\tt base_path} to the value of {\em
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
   116
%your} Isabelle main directory, i.e. the directory that contains the
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
   117
%subdirectories where standard logics like {\tt FOL} and {\tt HOL} or
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
   118
%your own logics are stored. If you do not do this, the generated HTML
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
   119
%files will still be usable but may contain incomplete titles and lack
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
   120
%some hypertext links.
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
   121
%
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
   122
%It's also a good idea to set {\tt gif_path} which points to the
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
   123
%directory containing two GIF images used in the HTML documents.
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
   124
%Normally this is the \texttt{src/Tools} subdirectory of Isabelle's
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
   125
%main directory. While its value in general is still valid, your HTML
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
   126
%files would depend on files not owned by you. This prevents you from
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
   127
%changing the location of the HTML files (as they contain relative
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
   128
%paths) and also causes trouble if the database's maker (re)moves the
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
   129
%GIFs.
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
   130
%
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
   131
%Here's what you should do before invoking {\tt init_html} using
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
   132
%someone else's \ML{} database:
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
   133
%
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
   134
%\begin{ttbox}
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
   135
%base_path := "/home/someone/Isabelle-dist/src";
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
   136
%gif_path := "/home/someone/Isabelle-dist/src/Tools";
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
   137
%init_html();
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
   138
%\dots
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
   139
%\end{ttbox}
3188
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   140
3753
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
   141
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
   142
\section{Browsing theory graphs} \label{sec:browse}
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
   143
\index{theory graph browser|bold} 
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
   144
4540
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   145
The graph browser is a tool for visualizing dependency graphs of
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   146
Isabelle theories. Certain nodes of the graph (i.e.~theories) can be
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   147
grouped together in ``directories'', whose contents may be hidden,
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   148
thus enabling the user to filter out irrelevant information.  The
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   149
browser is written in Java, it can be used both as a stand-alone
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   150
application and as an applet.
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   151
3188
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   152
3753
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
   153
\subsection{Invoking the graph browser}
4540
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   154
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   155
The stand-alone version of the graph browser is wrapped up as an
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   156
Isabelle tool called \tooldx{browser}:
3753
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
   157
\begin{ttbox}
4540
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   158
Usage: browser [GRAPHFILE]
3753
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
   159
\end{ttbox}
4540
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   160
When no filename is specified, the browser automatically changes to
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   161
the directory \texttt{ISABELLE_BROWSER_INFO/graph/data}.
3753
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
   162
4540
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   163
\medskip The applet version of the browser can be invoked by opening
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   164
the {\tt index.html} file in the directory
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   165
\texttt{ISABELLE_BROWSER_INFO} from your Web browser and selecting
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   166
``version for Java capable browsers''.  There is also a link to the
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   167
corresponding theory graph in every logic's {\tt index.html} file.
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   168
3188
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   169
3753
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
   170
\subsection{Using the graph browser}
4540
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   171
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   172
The browser's main window, which is shown in figure
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   173
\ref{browserwindow}, consists of two subwindows: In the left
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   174
subwindow, the directory tree is displayed. The graph itself is
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   175
displayed in the right subwindow.
3753
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
   176
\begin{figure}[h]
4540
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   177
  \includegraphics[width=\textwidth]{browser_screenshot.eps}
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   178
  \caption{\label{browserwindow} Browser main window}
3753
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
   179
\end{figure}
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
   180
4540
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   181
3753
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
   182
\subsubsection*{The directory tree window}
4540
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   183
3753
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
   184
This section describes the usage of the directory browser and the
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
   185
meaning of the different items in the browser window.
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
   186
\begin{itemize}
4540
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   187
  
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   188
\item A red arrow before a directory name indicates that the directory
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   189
  is currently ``folded'', i.e.~the nodes in this directory are
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   190
  collapsed to one single node. In the right subwindow, the names of
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   191
  nodes corresponding to folded directories are enclosed in square
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   192
  brackets and displayed in red colour.
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   193
  
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   194
\item A green downward arrow before a directory name indicates that
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   195
  the directory is currently ``unfolded''. It can be folded by
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   196
  clicking on the directory name.  Clicking on the name for a second
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   197
  time unfolds the directory again.  Alternatively, a directory can
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   198
  also be unfolded by clicking on the corresponding node in the right
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   199
  subwindow.
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   200
  
3753
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
   201
\item Blue arrows stand before ordinary node (i.e.~theory) names. When
4540
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   202
  clicking on such a name, the graph display window focuses to the
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   203
  corresponding node. Double clicking invokes a text viewer window in
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   204
  which the contents of the theory file are displayed.
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   205
3753
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
   206
\end{itemize}
3188
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   207
4540
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   208
3753
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
   209
\subsubsection*{The graph display window}
4540
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   210
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   211
When pointing on an ordinary node, an upward and a downward arrow is
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   212
shown.  Initially, both of these arrows are green. Clicking on the
3753
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
   213
upward or downward arrow collapses all predecessor or successor nodes,
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
   214
respectively. The arrow's colour then changes to red, indicating that
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
   215
the predecessor or successor nodes are currently collapsed. The node
4540
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   216
corresponding to the collapsed nodes has the name ``{\tt [....]}''. To
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   217
uncollapse the nodes again, simply click on the red arrow or on the
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   218
node with the name ``{\tt [....]}''. Similar to the directory browser,
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   219
the contents of theory files can be displayed by double clicking on
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   220
the corresponding node.
3188
445555a7b714 preliminary!
wenzelm
parents:
diff changeset
   221
4540
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   222
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   223
\subsubsection*{The ``File'' menu}
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   224
4555
wenzelm
parents: 4540
diff changeset
   225
Please note that due to Java security restrictions this menu is not
4540
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   226
available in the applet version. The meaning of the menu items is as
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   227
follows:
3753
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
   228
\begin{description}
4540
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   229
  
3753
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
   230
\item[Open$\ldots$] Open a new graph file.
4540
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   231
  
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   232
\item[Export to PostScript] Outputs the current graph in {\sc
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   233
    PostScript} format, appropriately scaled to fit on one single
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   234
  sheet of paper.  The resulting file can printed directly.
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   235
  
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   236
\item[Export to EPS] Outputs the current graph in Encapsulated {\sc
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   237
    PostScript} format. The resulting file can be included in other
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   238
  documents.
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   239
3753
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
   240
\item[Quit] Quit the graph browser.
4540
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   241
3753
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
   242
\end{description}
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
   243
4540
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   244
3753
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
   245
\subsection*{*Syntax of graph definition files}
4540
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   246
3753
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
   247
A graph definition file has the following syntax:
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
   248
\begin{eqnarray*}
4540
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   249
  \mbox{\it graph} & = & \{ \: \mbox{\it vertex \tt ;} \: \} ^ + \\
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   250
  vertex & = & \mbox{\it vertexname} \: \mbox{\it vertexID} \: \mbox{\it dirname} \: [ \mbox{\tt +} ]
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   251
  \: \mbox{\it path} \: [ \mbox{\tt <} | \mbox{\tt >} ] \: \{ \: \mbox{\it vertexID} \: \} ^ *
3753
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
   252
\end{eqnarray*}
4540
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   253
3753
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
   254
The meaning of the items in a vertex description is as follows:
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
   255
\begin{description}
4540
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   256
  
3753
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
   257
\item[vertexname] The name of the vertex.
4540
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   258
  
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   259
\item[vertexID] The vertex identifier. Note that there may be two
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   260
  vertices with equal names, whereas identifiers must be unique.
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   261
  
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   262
\item[dirname] The name of the ``directory'' the vertex should be
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   263
  placed in.  A ``{\tt +}'' sign after {\it dirname} indicates that
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   264
  the nodes in the directory are initially visible. Directories are
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   265
  initially invisible by default.
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   266
  
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   267
\item[path] The path of the corresponding theory file. This is
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   268
  specified relatively to the path of the graph definition file.
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   269
  
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   270
\item[List of successor/predecessor nodes] A ``{\tt <}'' sign before
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   271
  the list means that successor nodes are listed, a ``{\tt >}'' sign
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   272
  means that predecessor nodes are listed. If neither ``{\tt <}'' nor
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   273
  ``{\tt >}'' is found, the browser assumes that successor nodes are
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   274
  listed.
24fcf5ecae88 updated to Isabelle98;
wenzelm
parents: 3753
diff changeset
   275
3753
5fd734bed0d4 Added section describing the theory browser.
berghofe
parents: 3217
diff changeset
   276
\end{description}
5364
ffa6d795c4b3 emacs local vars;
wenzelm
parents: 4555
diff changeset
   277
ffa6d795c4b3 emacs local vars;
wenzelm
parents: 4555
diff changeset
   278
ffa6d795c4b3 emacs local vars;
wenzelm
parents: 4555
diff changeset
   279
%%% Local Variables: 
ffa6d795c4b3 emacs local vars;
wenzelm
parents: 4555
diff changeset
   280
%%% mode: latex
ffa6d795c4b3 emacs local vars;
wenzelm
parents: 4555
diff changeset
   281
%%% TeX-master: "system"
ffa6d795c4b3 emacs local vars;
wenzelm
parents: 4555
diff changeset
   282
%%% End: