82 |
82 |
83 In order to present your own theories on the web, simply copy the whole |
83 In order to present your own theories on the web, simply copy the whole |
84 \texttt{ISABELLE_BROWSER_INFO} directory to your WWW server, after generating |
84 \texttt{ISABELLE_BROWSER_INFO} directory to your WWW server, after generating |
85 browser info like this: |
85 browser info like this: |
86 \begin{ttbox} |
86 \begin{ttbox} |
87 isatool usedir -i true HOL Foobar |
87 isatool usedir -i true HOL Foo |
88 \end{ttbox} |
88 \end{ttbox} |
89 This assumes that directory \texttt{Foobar} contains some \texttt{ROOT.ML} |
89 This assumes that directory \texttt{Foo} contains some \texttt{ROOT.ML} file |
90 file to load all your theories, and {\HOL} is your parent logic image. |
90 to load all your theories, and {\HOL} is your parent logic image. Ideally, |
91 Ideally, theory browser information would have been generated for {\HOL} |
91 theory browser information would have been generated for {\HOL} already. |
92 already. |
|
93 |
92 |
94 Alternatively, one may specify an external link to an existing body of HTML |
93 Alternatively, one may specify an external link to an existing body of HTML |
95 data by giving \texttt{usedir} a \texttt{-P} option like this: |
94 data by giving \texttt{usedir} a \texttt{-P} option like this: |
96 \begin{ttbox} |
95 \begin{ttbox} |
97 isatool usedir -i true -P http://isabelle.in.tum.de/library/ HOL Foobar |
96 isatool usedir -i true -P http://isabelle.in.tum.de/library/ HOL Foo |
98 \end{ttbox} |
97 \end{ttbox} |
99 |
98 |
100 |
99 |
101 |
100 |
102 \section{Browsing theory graphs} \label{sec:browse} |
101 \section{Browsing theory graphs} \label{sec:browse} |
238 |
237 |
239 \section{Preparing Isabelle session documents --- \texttt{isatool document}} |
238 \section{Preparing Isabelle session documents --- \texttt{isatool document}} |
240 \label{sec:tool-document} |
239 \label{sec:tool-document} |
241 |
240 |
242 The \tooldx{document} utility prepares logic session documents, processing the |
241 The \tooldx{document} utility prepares logic session documents, processing the |
243 combined sources as provided by the user and generated by Isabelle. Its usage is: |
242 sources both provided by the user and generated by Isabelle. Its usage is: |
244 \begin{ttbox} |
243 \begin{ttbox} |
245 Usage: document [OPTIONS] [DIR] |
244 Usage: document [OPTIONS] [DIR] |
246 |
245 |
247 Options are: |
246 Options are: |
248 -o FORMAT specify output format: dvi (default), dvi.gz, ps, |
247 -o FORMAT specify output format: dvi (default), dvi.gz, ps, |