--- a/doc-src/System/Thy/Misc.thy Wed Aug 15 12:36:38 2012 +0200
+++ b/doc-src/System/Thy/Misc.thy Wed Aug 15 12:54:25 2012 +0200
@@ -116,31 +116,17 @@
subsubsection {* Examples *}
-text {*
- Get the ML system name and the location where the compiler binaries
- are supposed to reside as follows:
+text {* Get the location of @{setting ISABELLE_HOME_USER} where
+ user-specific information is stored:
\begin{ttbox}
-isabelle getenv ML_SYSTEM ML_HOME
-{\out ML_SYSTEM=polyml}
-{\out ML_HOME=/usr/share/polyml/x86-linux}
+isabelle getenv ISABELLE_HOME_USER
\end{ttbox}
- The next one peeks at the output directory for Isabelle logic
- images:
+ \medskip Get the value only of the same settings variable, which is
+particularly useful in shell scripts:
\begin{ttbox}
isabelle getenv -b ISABELLE_OUTPUT
-{\out /home/me/isabelle/heaps/polyml_x86-linux}
\end{ttbox}
- Here we have used the @{verbatim "-b"} option to suppress the
- @{verbatim "ISABELLE_OUTPUT="} prefix. The value above is what
- became of the following assignment in the default settings file:
-\begin{ttbox}
-ISABELLE_OUTPUT="\$ISABELLE_HOME_USER/heaps"
-\end{ttbox}
-
- Note how the @{setting ML_IDENTIFIER} value got appended
- automatically to each path component. This is a special feature of
- @{setting ISABELLE_OUTPUT}.
*}
@@ -167,14 +153,15 @@
distribution directory as determined by @{setting ISABELLE_HOME}.
The @{verbatim "-p"} option installs executable wrapper scripts for
- @{executable "isabelle-process"}, @{executable isabelle},
- @{executable Isabelle}, containing proper absolute references to the
- Isabelle distribution directory. A typical @{verbatim DIR}
- specification would be some directory expected to be in the shell's
- @{setting PATH}, such as @{verbatim "/usr/local/bin"}. It is
- important to note that a plain manual copy of the original Isabelle
- executables does not work, since it disrupts the integrity of the
- Isabelle distribution.
+ @{executable "isabelle-process"}, @{executable isabelle}, containing
+ proper absolute references to the Isabelle distribution directory.
+ A typical @{verbatim DIR} specification would be some directory
+ expected to be in the shell's @{setting PATH}, such as @{verbatim
+ "$HOME/bin"}.
+
+ It is possible to make symbolic links of the main Isabelle
+ executables, but making separate copies outside the Isabelle
+ distribution directory will not work.
*}
--- a/doc-src/System/Thy/Scala.thy Wed Aug 15 12:36:38 2012 +0200
+++ b/doc-src/System/Thy/Scala.thy Wed Aug 15 12:54:25 2012 +0200
@@ -46,7 +46,8 @@
\begin{alltt}
isabelle scala
scala> isabelle.Isabelle_System.getenv("ISABELLE_HOME")
- scala> isabelle.Isabelle_System.find_logics()
+ scala> val options = isabelle.Options.init()
+ scala> options.bool("browser_info")
\end{alltt}
*}
--- a/doc-src/System/Thy/document/Misc.tex Wed Aug 15 12:36:38 2012 +0200
+++ b/doc-src/System/Thy/document/Misc.tex Wed Aug 15 12:54:25 2012 +0200
@@ -149,30 +149,17 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-Get the ML system name and the location where the compiler binaries
- are supposed to reside as follows:
+Get the location of \hyperlink{setting.ISABELLE-HOME-USER}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}HOME{\isaliteral{5F}{\isacharunderscore}}USER}}}} where
+ user-specific information is stored:
\begin{ttbox}
-isabelle getenv ML_SYSTEM ML_HOME
-{\out ML_SYSTEM=polyml}
-{\out ML_HOME=/usr/share/polyml/x86-linux}
+isabelle getenv ISABELLE_HOME_USER
\end{ttbox}
- The next one peeks at the output directory for Isabelle logic
- images:
+ \medskip Get the value only of the same settings variable, which is
+particularly useful in shell scripts:
\begin{ttbox}
isabelle getenv -b ISABELLE_OUTPUT
-{\out /home/me/isabelle/heaps/polyml_x86-linux}
-\end{ttbox}
- Here we have used the \verb|-b| option to suppress the
- \verb|ISABELLE_OUTPUT=| prefix. The value above is what
- became of the following assignment in the default settings file:
-\begin{ttbox}
-ISABELLE_OUTPUT="\$ISABELLE_HOME_USER/heaps"
-\end{ttbox}
-
- Note how the \hyperlink{setting.ML-IDENTIFIER}{\mbox{\isa{\isatt{ML{\isaliteral{5F}{\isacharunderscore}}IDENTIFIER}}}} value got appended
- automatically to each path component. This is a special feature of
- \hyperlink{setting.ISABELLE-OUTPUT}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}OUTPUT}}}}.%
+\end{ttbox}%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -201,14 +188,14 @@
distribution directory as determined by \hyperlink{setting.ISABELLE-HOME}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}HOME}}}}.
The \verb|-p| option installs executable wrapper scripts for
- \hyperlink{executable.isabelle-process}{\mbox{\isa{\isatt{isabelle{\isaliteral{2D}{\isacharminus}}process}}}}, \hyperlink{executable.isabelle}{\mbox{\isa{\isatt{isabelle}}}},
- \hyperlink{executable.Isabelle}{\mbox{\isa{\isatt{Isabelle}}}}, containing proper absolute references to the
- Isabelle distribution directory. A typical \verb|DIR|
- specification would be some directory expected to be in the shell's
- \hyperlink{setting.PATH}{\mbox{\isa{\isatt{PATH}}}}, such as \verb|/usr/local/bin|. It is
- important to note that a plain manual copy of the original Isabelle
- executables does not work, since it disrupts the integrity of the
- Isabelle distribution.%
+ \hyperlink{executable.isabelle-process}{\mbox{\isa{\isatt{isabelle{\isaliteral{2D}{\isacharminus}}process}}}}, \hyperlink{executable.isabelle}{\mbox{\isa{\isatt{isabelle}}}}, containing
+ proper absolute references to the Isabelle distribution directory.
+ A typical \verb|DIR| specification would be some directory
+ expected to be in the shell's \hyperlink{setting.PATH}{\mbox{\isa{\isatt{PATH}}}}, such as \verb|$HOME/bin|.
+
+ It is possible to make symbolic links of the main Isabelle
+ executables, but making separate copies outside the Isabelle
+ distribution directory will not work.%
\end{isamarkuptext}%
\isamarkuptrue%
%
--- a/doc-src/System/Thy/document/Scala.tex Wed Aug 15 12:36:38 2012 +0200
+++ b/doc-src/System/Thy/document/Scala.tex Wed Aug 15 12:54:25 2012 +0200
@@ -70,7 +70,8 @@
\begin{alltt}
isabelle scala
scala> isabelle.Isabelle_System.getenv("ISABELLE_HOME")
- scala> isabelle.Isabelle_System.find_logics()
+ scala> val options = isabelle.Options.init()
+ scala> options.bool("browser_info")
\end{alltt}%
\end{isamarkuptext}%
\isamarkuptrue%