# HG changeset patch
# User wenzelm
# Date 1345028065 -7200
# Node ID eed6698b2ba0b4c7f4c351ae11f09251f93f0889
# Parent  d488a5f25bf668a7a2ad7d03d63e1016b37a8259
tuned;

diff -r d488a5f25bf6 -r eed6698b2ba0 doc-src/System/Thy/Misc.thy
--- 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.
 *}
 
 
diff -r d488a5f25bf6 -r eed6698b2ba0 doc-src/System/Thy/Scala.thy
--- 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}
 *}
 
diff -r d488a5f25bf6 -r eed6698b2ba0 doc-src/System/Thy/document/Misc.tex
--- 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%
 %
diff -r d488a5f25bf6 -r eed6698b2ba0 doc-src/System/Thy/document/Scala.tex
--- 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%