equal
deleted
inserted
replaced
196 |
196 |
197 \begin{ttbox} |
197 \begin{ttbox} |
198 Usage: browser [OPTIONS] [GRAPHFILE] |
198 Usage: browser [OPTIONS] [GRAPHFILE] |
199 |
199 |
200 Options are: |
200 Options are: |
|
201 -b Admin/build only |
201 -c cleanup -- remove GRAPHFILE after use |
202 -c cleanup -- remove GRAPHFILE after use |
202 -o FILE output to FILE (ps, eps, pdf) |
203 -o FILE output to FILE (ps, eps, pdf) |
203 \end{ttbox} |
204 \end{ttbox} |
204 When no filename is specified, the browser automatically changes to |
205 When no filename is specified, the browser automatically changes to |
205 the directory \hyperlink{setting.ISABELLE-BROWSER-INFO}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}BROWSER{\isacharunderscore}INFO}}}}. |
206 the directory \hyperlink{setting.ISABELLE-BROWSER-INFO}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}BROWSER{\isacharunderscore}INFO}}}}. |
206 |
207 |
207 \medskip The \verb|-c| option causes the input file to be |
208 \medskip The \verb|-b| option indicates that this is for |
208 removed after use. |
209 administrative build only, i.e.\ no browser popup if no files are |
|
210 given. |
|
211 |
|
212 The \verb|-c| option causes the input file to be removed |
|
213 after use. |
209 |
214 |
210 The \verb|-o| option indicates batch-mode operation, with the |
215 The \verb|-o| option indicates batch-mode operation, with the |
211 output written to the indicated file; note that \verb|pdf| |
216 output written to the indicated file; note that \verb|pdf| |
212 produces an \verb|eps| copy as well. |
217 produces an \verb|eps| copy as well. |
213 |
218 |