src/Doc/System/Environment.thy

-     (*:maxLineLen=78:*)
+(*:maxLineLen=78:*)
 
 theory Environment
 imports Base
 begin
 

   defaults may be overridden by a private \<^verbatim>\<open>$ISABELLE_HOME_USER/etc/settings\<close>.
 
   \<^descr>[@{setting_def ISABELLE_PLATFORM_FAMILY}\<open>\<^sup>*\<close>] is automatically set to the
   general platform family: \<^verbatim>\<open>linux\<close>, \<^verbatim>\<open>macos\<close>, \<^verbatim>\<open>windows\<close>. Note that
   platform-dependent tools usually need to refer to the more specific
-  identification according to @{setting ISABELLE_PLATFORM}, @{setting
-  ISABELLE_PLATFORM32}, @{setting ISABELLE_PLATFORM64}.
-
-  \<^descr>[@{setting_def ISABELLE_PLATFORM}\<open>\<^sup>*\<close>] is automatically set to a symbolic
-  identifier for the underlying hardware and operating system. The Isabelle
-  platform identification always refers to the 32 bit variant, even this is a
-  64 bit machine. Note that the ML or Java runtime may have a different idea,
-  depending on which binaries are actually run.
-
-  \<^descr>[@{setting_def ISABELLE_PLATFORM64}\<open>\<^sup>*\<close>] is similar to @{setting
-  ISABELLE_PLATFORM} but refers to the proper 64 bit variant on a platform
-  that supports this; the value is empty for 32 bit. Note that the following
-  bash expression (including the quotes) prefers the 64 bit platform, if that
-  is available:
-
-  @{verbatim [display] \<open>"${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM}"\<close>}
+  identification according to @{setting ISABELLE_PLATFORM} etc.
+
+  \<^descr>[@{setting_def ISABELLE_PLATFORM32}\<open>\<^sup>*\<close>, @{setting_def
+  ISABELLE_PLATFORM64}\<open>\<^sup>*\<close>, @{setting_def ISABELLE_PLATFORM}\<open>\<^sup>*\<close>] indicate the
+  standard Posix platform: \<^verbatim>\<open>x86\<close> for 32 bit and \<^verbatim>\<open>x86_64\<close> for 64 bit,
+  together with a symbolic name for the operating system (\<^verbatim>\<open>linux\<close>, \<^verbatim>\<open>darwin\<close>,
+  \<^verbatim>\<open>cygwin\<close>). Some platforms support both 32 bit and 64 bit executables, but
+  this depends on various side-conditions.
+
+  In GNU bash scripts, it is possible to use the following expressions
+  (including the quotes) to specify a preference of 64 bit over 32 bit:
+
+  @{verbatim [display] \<open>"${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM32}"\<close>}
+
+  In contrast, the subsequent expression prefers the 32 bit variant; this is
+  how @{setting ISABELLE_PLATFORM} is defined:
+
+  @{verbatim [display] \<open>"${ISABELLE_PLATFORM32:-$ISABELLE_PLATFORM64}"\<close>}
+
+  \<^descr>[@{setting_def ISABELLE_WINDOWS_PLATFORM32}\<open>\<^sup>*\<close>, @{setting_def
+  ISABELLE_WINDOWS_PLATFORM64}\<open>\<^sup>*\<close>,] @{setting_def
+  ISABELLE_WINDOWS_PLATFORM}\<open>\<^sup>*\<close> indicate the native Windows platform. These
+  settings are analogous (but independent) of those for the standard Posix
+  subsystem: @{setting ISABELLE_PLATFORM32}, @{setting ISABELLE_PLATFORM64},
+  @{setting ISABELLE_PLATFORM}.
+
+  In GNU bash scripts, a preference for native Windows platform variants may
+  be specified like this:
+
+  @{verbatim [display] \<open>"${ISABELLE_WINDOWS_PLATFORM:-$ISABELLE_PLATFORM}"\<close>}
+
+  @{verbatim [display] \<open>"${ISABELLE_WINDOWS_PLATFORM64:-${ISABELLE_WINDOWS_PLATFORM32:-${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM32}}}"\<close>}
 
   \<^descr>[@{setting ISABELLE_TOOL}\<open>\<^sup>*\<close>] is automatically set to the full path name
   of the @{executable isabelle} executable.
 
   \<^descr>[@{setting_def ISABELLE_IDENTIFIER}\<open>\<^sup>*\<close>] refers to the name of this

   images, which is useful for cross-platform installations. The value of
   @{setting ML_IDENTIFIER} is automatically obtained by composing the values
   of @{setting ML_SYSTEM}, @{setting ML_PLATFORM} and the Isabelle version
   values.
 
-  \<^descr>[@{setting_def ISABELLE_JDK_HOME}] needs to point to a full JDK (Java
-  Development Kit) installation with \<^verbatim>\<open>javac\<close> and \<^verbatim>\<open>jar\<close> executables. This is
-  essential for Isabelle/Scala and other JVM-based tools to work properly.
-  Note that conventional \<^verbatim>\<open>JAVA_HOME\<close> usually points to the JRE (Java Runtime
-  Environment), not JDK.
+  \<^descr>[@{setting_def ISABELLE_JDK_HOME}] points to a full JDK (Java Development
+  Kit) installation with \<^verbatim>\<open>javac\<close> and \<^verbatim>\<open>jar\<close> executables. Note that
+  conventional \<^verbatim>\<open>JAVA_HOME\<close> points to the JRE (Java Runtime Environment), not
+  the JDK.
+
+  \<^descr>[@{setting_def ISABELLE_JAVA_PLATFORM}] identifies the hardware and
+  operating system platform for the Java installation of Isabelle. That is
+  usually the (native) 64 bit variant: \<^verbatim>\<open>x86_64-linux\<close>, \<^verbatim>\<open>x86_64-darwin\<close>,
+  \<^verbatim>\<open>x86_64-windows\<close>.
 
   \<^descr>[@{setting_def ISABELLE_PATH}] is a list of directories (separated by
   colons) where Isabelle logic images may reside. When looking up heaps files,
   the value of @{setting ML_IDENTIFIER} is appended to each component
   internally.