src/Doc/System/Environment.thy
changeset 66789 feb36b73a7f0
parent 66787 64b47495676d
parent 66733 9180953b976b
child 66906 03a96b8c7c06
     1.1 --- a/src/Doc/System/Environment.thy	Sun Oct 08 11:58:01 2017 +0200
     1.2 +++ b/src/Doc/System/Environment.thy	Sun Oct 08 14:48:47 2017 +0200
     1.3 @@ -1,4 +1,4 @@
     1.4 -     (*:maxLineLen=78:*)
     1.5 +(*:maxLineLen=78:*)
     1.6  
     1.7  theory Environment
     1.8  imports Base
     1.9 @@ -118,22 +118,38 @@
    1.10    \<^descr>[@{setting_def ISABELLE_PLATFORM_FAMILY}\<open>\<^sup>*\<close>] is automatically set to the
    1.11    general platform family: \<^verbatim>\<open>linux\<close>, \<^verbatim>\<open>macos\<close>, \<^verbatim>\<open>windows\<close>. Note that
    1.12    platform-dependent tools usually need to refer to the more specific
    1.13 -  identification according to @{setting ISABELLE_PLATFORM}, @{setting
    1.14 -  ISABELLE_PLATFORM32}, @{setting ISABELLE_PLATFORM64}.
    1.15 +  identification according to @{setting ISABELLE_PLATFORM} etc.
    1.16 +
    1.17 +  \<^descr>[@{setting_def ISABELLE_PLATFORM32}\<open>\<^sup>*\<close>, @{setting_def
    1.18 +  ISABELLE_PLATFORM64}\<open>\<^sup>*\<close>, @{setting_def ISABELLE_PLATFORM}\<open>\<^sup>*\<close>] indicate the
    1.19 +  standard Posix platform: \<^verbatim>\<open>x86\<close> for 32 bit and \<^verbatim>\<open>x86_64\<close> for 64 bit,
    1.20 +  together with a symbolic name for the operating system (\<^verbatim>\<open>linux\<close>, \<^verbatim>\<open>darwin\<close>,
    1.21 +  \<^verbatim>\<open>cygwin\<close>). Some platforms support both 32 bit and 64 bit executables, but
    1.22 +  this depends on various side-conditions.
    1.23 +
    1.24 +  In GNU bash scripts, it is possible to use the following expressions
    1.25 +  (including the quotes) to specify a preference of 64 bit over 32 bit:
    1.26 +
    1.27 +  @{verbatim [display] \<open>"${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM32}"\<close>}
    1.28  
    1.29 -  \<^descr>[@{setting_def ISABELLE_PLATFORM}\<open>\<^sup>*\<close>] is automatically set to a symbolic
    1.30 -  identifier for the underlying hardware and operating system. The Isabelle
    1.31 -  platform identification always refers to the 32 bit variant, even this is a
    1.32 -  64 bit machine. Note that the ML or Java runtime may have a different idea,
    1.33 -  depending on which binaries are actually run.
    1.34 +  In contrast, the subsequent expression prefers the 32 bit variant; this is
    1.35 +  how @{setting ISABELLE_PLATFORM} is defined:
    1.36 +
    1.37 +  @{verbatim [display] \<open>"${ISABELLE_PLATFORM32:-$ISABELLE_PLATFORM64}"\<close>}
    1.38  
    1.39 -  \<^descr>[@{setting_def ISABELLE_PLATFORM64}\<open>\<^sup>*\<close>] is similar to @{setting
    1.40 -  ISABELLE_PLATFORM} but refers to the proper 64 bit variant on a platform
    1.41 -  that supports this; the value is empty for 32 bit. Note that the following
    1.42 -  bash expression (including the quotes) prefers the 64 bit platform, if that
    1.43 -  is available:
    1.44 +  \<^descr>[@{setting_def ISABELLE_WINDOWS_PLATFORM32}\<open>\<^sup>*\<close>, @{setting_def
    1.45 +  ISABELLE_WINDOWS_PLATFORM64}\<open>\<^sup>*\<close>,] @{setting_def
    1.46 +  ISABELLE_WINDOWS_PLATFORM}\<open>\<^sup>*\<close> indicate the native Windows platform. These
    1.47 +  settings are analogous (but independent) of those for the standard Posix
    1.48 +  subsystem: @{setting ISABELLE_PLATFORM32}, @{setting ISABELLE_PLATFORM64},
    1.49 +  @{setting ISABELLE_PLATFORM}.
    1.50  
    1.51 -  @{verbatim [display] \<open>"${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM}"\<close>}
    1.52 +  In GNU bash scripts, a preference for native Windows platform variants may
    1.53 +  be specified like this:
    1.54 +
    1.55 +  @{verbatim [display] \<open>"${ISABELLE_WINDOWS_PLATFORM:-$ISABELLE_PLATFORM}"\<close>}
    1.56 +
    1.57 +  @{verbatim [display] \<open>"${ISABELLE_WINDOWS_PLATFORM64:-${ISABELLE_WINDOWS_PLATFORM32:-${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM32}}}"\<close>}
    1.58  
    1.59    \<^descr>[@{setting ISABELLE_TOOL}\<open>\<^sup>*\<close>] is automatically set to the full path name
    1.60    of the @{executable isabelle} executable.
    1.61 @@ -155,11 +171,15 @@
    1.62    of @{setting ML_SYSTEM}, @{setting ML_PLATFORM} and the Isabelle version
    1.63    values.
    1.64  
    1.65 -  \<^descr>[@{setting_def ISABELLE_JDK_HOME}] needs to point to a full JDK (Java
    1.66 -  Development Kit) installation with \<^verbatim>\<open>javac\<close> and \<^verbatim>\<open>jar\<close> executables. This is
    1.67 -  essential for Isabelle/Scala and other JVM-based tools to work properly.
    1.68 -  Note that conventional \<^verbatim>\<open>JAVA_HOME\<close> usually points to the JRE (Java Runtime
    1.69 -  Environment), not JDK.
    1.70 +  \<^descr>[@{setting_def ISABELLE_JDK_HOME}] points to a full JDK (Java Development
    1.71 +  Kit) installation with \<^verbatim>\<open>javac\<close> and \<^verbatim>\<open>jar\<close> executables. Note that
    1.72 +  conventional \<^verbatim>\<open>JAVA_HOME\<close> points to the JRE (Java Runtime Environment), not
    1.73 +  the JDK.
    1.74 +
    1.75 +  \<^descr>[@{setting_def ISABELLE_JAVA_PLATFORM}] identifies the hardware and
    1.76 +  operating system platform for the Java installation of Isabelle. That is
    1.77 +  usually the (native) 64 bit variant: \<^verbatim>\<open>x86_64-linux\<close>, \<^verbatim>\<open>x86_64-darwin\<close>,
    1.78 +  \<^verbatim>\<open>x86_64-windows\<close>.
    1.79  
    1.80    \<^descr>[@{setting_def ISABELLE_PATH}] is a list of directories (separated by
    1.81    colons) where Isabelle logic images may reside. When looking up heaps files,