equal
deleted
inserted
replaced
35 \isamarkupsection{Java Runtime Environment within Isabelle \label{sec:tool-java}% |
35 \isamarkupsection{Java Runtime Environment within Isabelle \label{sec:tool-java}% |
36 } |
36 } |
37 \isamarkuptrue% |
37 \isamarkuptrue% |
38 % |
38 % |
39 \begin{isamarkuptext}% |
39 \begin{isamarkuptext}% |
40 The Isabelle \indexdef{}{tool}{java}\hypertarget{tool.java}{\hyperlink{tool.java}{\mbox{\isa{\isatt{java}}}}} utility is a direct wrapper for |
40 The \indexdef{}{tool}{java}\hypertarget{tool.java}{\hyperlink{tool.java}{\mbox{\isa{\isatool{java}}}}} tool is a direct wrapper for the Java |
41 the Java Runtime Environment, within the regular Isabelle settings |
41 Runtime Environment, within the regular Isabelle settings |
42 environment (\secref{sec:settings}). The command line arguments are |
42 environment (\secref{sec:settings}). The command line arguments are |
43 that of the underlying Java version. It is run in \verb|-server| mode if possible, to improve performance (at the cost of |
43 that of the underlying Java version. It is run in \verb|-server| mode if possible, to improve performance (at the cost of |
44 extra startup time). |
44 extra startup time). |
45 |
45 |
46 The \verb|java| executable is the one within \hyperlink{setting.ISABELLE-JDK-HOME}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}JDK{\isaliteral{5F}{\isacharunderscore}}HOME}}}}, according to the standard directory layout for |
46 The \verb|java| executable is the one within \hyperlink{setting.ISABELLE-JDK-HOME}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}JDK{\isaliteral{5F}{\isacharunderscore}}HOME}}}}, according to the standard directory layout for |
60 \isamarkupsection{Scala toplevel \label{sec:tool-scala}% |
60 \isamarkupsection{Scala toplevel \label{sec:tool-scala}% |
61 } |
61 } |
62 \isamarkuptrue% |
62 \isamarkuptrue% |
63 % |
63 % |
64 \begin{isamarkuptext}% |
64 \begin{isamarkuptext}% |
65 The Isabelle \indexdef{}{tool}{scala}\hypertarget{tool.scala}{\hyperlink{tool.scala}{\mbox{\isa{\isatt{scala}}}}} utility is a direct wrapper for |
65 The \indexdef{}{tool}{scala}\hypertarget{tool.scala}{\hyperlink{tool.scala}{\mbox{\isa{\isatool{scala}}}}} tool is a direct wrapper for the Scala |
66 the Scala toplevel; see also \hyperlink{tool.java}{\mbox{\isa{\isatt{java}}}} above. The command line |
66 toplevel; see also \hyperlink{tool.java}{\mbox{\isa{\isatool{java}}}} above. The command line arguments |
67 arguments are that of the underlying Scala version. |
67 are that of the underlying Scala version. |
68 |
68 |
69 This allows to interact with Isabelle/Scala in TTY mode like this: |
69 This allows to interact with Isabelle/Scala in TTY mode like this: |
70 \begin{alltt} |
70 \begin{alltt} |
71 isabelle scala |
71 isabelle scala |
72 scala> isabelle.Isabelle_System.getenv("ISABELLE_HOME") |
72 scala> isabelle.Isabelle_System.getenv("ISABELLE_HOME") |
78 \isamarkupsection{Scala compiler \label{sec:tool-scalac}% |
78 \isamarkupsection{Scala compiler \label{sec:tool-scalac}% |
79 } |
79 } |
80 \isamarkuptrue% |
80 \isamarkuptrue% |
81 % |
81 % |
82 \begin{isamarkuptext}% |
82 \begin{isamarkuptext}% |
83 The Isabelle \indexdef{}{tool}{scalac}\hypertarget{tool.scalac}{\hyperlink{tool.scalac}{\mbox{\isa{\isatt{scalac}}}}} utility is a direct wrapper |
83 The \indexdef{}{tool}{scalac}\hypertarget{tool.scalac}{\hyperlink{tool.scalac}{\mbox{\isa{\isatool{scalac}}}}} tool is a direct wrapper for the Scala |
84 for the Scala compiler; see also \hyperlink{tool.scala}{\mbox{\isa{\isatt{scala}}}} above. The command |
84 compiler; see also \hyperlink{tool.scala}{\mbox{\isa{\isatool{scala}}}} above. The command line arguments |
85 line arguments are that of the underlying Scala version. |
85 are that of the underlying Scala version. |
86 |
86 |
87 This allows to compile further Scala modules, depending on existing |
87 This allows to compile further Scala modules, depending on existing |
88 Isabelle/Scala functionality. The resulting class or jar files can |
88 Isabelle/Scala functionality. The resulting class or jar files can |
89 be added to the \hyperlink{setting.CLASSPATH}{\mbox{\isa{\isatt{CLASSPATH}}}} via the \verb|classpath| |
89 be added to the \hyperlink{setting.CLASSPATH}{\mbox{\isa{\isatt{CLASSPATH}}}} via the \verb|classpath| |
90 Bash function that is provided by the Isabelle process environment. |
90 Bash function that is provided by the Isabelle process environment. |