equal
deleted
inserted
replaced
86 \begin{ttbox} |
86 \begin{ttbox} |
87 ISABELLE_USEDIR_OPTIONS="-i true" |
87 ISABELLE_USEDIR_OPTIONS="-i true" |
88 \end{ttbox} |
88 \end{ttbox} |
89 |
89 |
90 and then change into the @{"file" "~~/src/FOL"} directory and run |
90 and then change into the @{"file" "~~/src/FOL"} directory and run |
91 @{verbatim isabelle} @{tool make}, or even @{verbatim isabelle} @{tool |
91 @{verbatim isabelle} @{tool make}, or even @{verbatim isabelle} |
92 make}~@{verbatim all}. The presentation output will appear in |
92 @{tool make}~@{verbatim all}. The presentation output will appear |
93 @{verbatim "ISABELLE_BROWSER_INFO/FOL"}, which usually refers to |
93 in @{verbatim "ISABELLE_BROWSER_INFO/FOL"}, which usually refers to |
94 @{verbatim "~/.isabelle/browser_info/FOL"}. Note that option |
94 something like @{verbatim |
|
95 "~/.isabelle/IsabelleXXXX/browser_info/FOL"}. Note that option |
95 @{verbatim "-v true"} will make the internal runs of @{tool usedir} |
96 @{verbatim "-v true"} will make the internal runs of @{tool usedir} |
96 more explicit about such details. |
97 more explicit about such details. |
97 |
98 |
98 Many standard Isabelle sessions (such as @{"file" "~~/src/HOL/ex"}) |
99 Many standard Isabelle sessions (such as @{"file" "~~/src/HOL/ex"}) |
99 also provide actual printable documents. These are prepared |
100 also provide actual printable documents. These are prepared |
766 process leaves the sources at a certain place within @{setting |
767 process leaves the sources at a certain place within @{setting |
767 ISABELLE_BROWSER_INFO}, see the runtime error message for details. |
768 ISABELLE_BROWSER_INFO}, see the runtime error message for details. |
768 This enables users to inspect {\LaTeX} runs in further detail, e.g.\ |
769 This enables users to inspect {\LaTeX} runs in further detail, e.g.\ |
769 like this: |
770 like this: |
770 \begin{ttbox} |
771 \begin{ttbox} |
771 cd ~/.isabelle/browser_info/HOL/Test/document |
772 cd ~/.isabelle/IsabelleXXXX/browser_info/HOL/Test/document |
772 isabelle latex -o pdf |
773 isabelle latex -o pdf |
773 \end{ttbox} |
774 \end{ttbox} |
774 *} |
775 *} |
775 |
776 |
776 end |
777 end |