more and updated documentation;
authorwenzelm
Sat Sep 30 20:06:26 2017 +0200 (20 months ago)
changeset 66732e566fb4d43d4
parent 66731 fe2a6ec20b4d
child 66733 9180953b976b
more and updated documentation;
Admin/PLATFORMS
src/Doc/System/Environment.thy
     1.1 --- a/Admin/PLATFORMS	Sat Sep 30 19:49:13 2017 +0200
     1.2 +++ b/Admin/PLATFORMS	Sat Sep 30 20:06:26 2017 +0200
     1.3 @@ -70,10 +70,9 @@
     1.4    ISABELLE_PLATFORM32  (potentially empty)
     1.5    ISABELLE_PLATFORM
     1.6  
     1.7 -The ISABELLE_PLATFORM setting variable refers to the 32 bit version of
     1.8 -the platform, even on 64 bit hardware.  Using regular bash notation,
     1.9 -tools may express their preference for 64 bit with a fall-back for 32
    1.10 -bit as follows:
    1.11 +The ISABELLE_PLATFORM setting variable prefers the 32 bit version of the
    1.12 +platform, if possible. Using regular bash notation, tools may express their
    1.13 +preference for 64 bit with a fall-back for 32 bit as follows:
    1.14  
    1.15    "${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM32}"
    1.16  
    1.17 @@ -81,7 +80,7 @@
    1.18  There is a second set of settings for native Windows (instead of the
    1.19  POSIX emulation of Cygwin used before):
    1.20  
    1.21 -  ISABELLE_WINDOWS_PLATFORM64  (potentially empty)
    1.22 +  ISABELLE_WINDOWS_PLATFORM64
    1.23    ISABELLE_WINDOWS_PLATFORM32
    1.24    ISABELLE_WINDOWS_PLATFORM
    1.25  
     2.1 --- a/src/Doc/System/Environment.thy	Sat Sep 30 19:49:13 2017 +0200
     2.2 +++ b/src/Doc/System/Environment.thy	Sat Sep 30 20:06:26 2017 +0200
     2.3 @@ -1,4 +1,4 @@
     2.4 -     (*:maxLineLen=78:*)
     2.5 +(*:maxLineLen=78:*)
     2.6  
     2.7  theory Environment
     2.8  imports Base
     2.9 @@ -118,22 +118,38 @@
    2.10    \<^descr>[@{setting_def ISABELLE_PLATFORM_FAMILY}\<open>\<^sup>*\<close>] is automatically set to the
    2.11    general platform family: \<^verbatim>\<open>linux\<close>, \<^verbatim>\<open>macos\<close>, \<^verbatim>\<open>windows\<close>. Note that
    2.12    platform-dependent tools usually need to refer to the more specific
    2.13 -  identification according to @{setting ISABELLE_PLATFORM}, @{setting
    2.14 -  ISABELLE_PLATFORM32}, @{setting ISABELLE_PLATFORM64}.
    2.15 +  identification according to @{setting ISABELLE_PLATFORM} etc.
    2.16 +
    2.17 +  \<^descr>[@{setting_def ISABELLE_PLATFORM32}\<open>\<^sup>*\<close>, @{setting_def
    2.18 +  ISABELLE_PLATFORM64}\<open>\<^sup>*\<close>, @{setting_def ISABELLE_PLATFORM}\<open>\<^sup>*\<close>] indicate the
    2.19 +  standard Posix platform: \<^verbatim>\<open>x86\<close> for 32 bit and \<^verbatim>\<open>x86_64\<close> for 64 bit,
    2.20 +  together with a symbolic name for the operating system (\<^verbatim>\<open>linux\<close>, \<^verbatim>\<open>darwin\<close>,
    2.21 +  \<^verbatim>\<open>cygwin\<close>). Some platforms support both 32 bit and 64 bit executables, but
    2.22 +  this depends on various side-conditions.
    2.23 +
    2.24 +  In GNU bash scripts, it is possible to use the following expressions
    2.25 +  (including the quotes) to specify a preference of 64 bit over 32 bit:
    2.26 +
    2.27 +  @{verbatim [display] \<open>"${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM32}"\<close>}
    2.28  
    2.29 -  \<^descr>[@{setting_def ISABELLE_PLATFORM}\<open>\<^sup>*\<close>] is automatically set to a symbolic
    2.30 -  identifier for the underlying hardware and operating system. The Isabelle
    2.31 -  platform identification always refers to the 32 bit variant, even this is a
    2.32 -  64 bit machine. Note that the ML or Java runtime may have a different idea,
    2.33 -  depending on which binaries are actually run.
    2.34 +  In contrast, the subsequent expression prefers the 32 bit variant; this is
    2.35 +  how @{setting ISABELLE_PLATFORM} is defined:
    2.36 +
    2.37 +  @{verbatim [display] \<open>"${ISABELLE_PLATFORM32:-$ISABELLE_PLATFORM64}"\<close>}
    2.38  
    2.39 -  \<^descr>[@{setting_def ISABELLE_PLATFORM64}\<open>\<^sup>*\<close>] is similar to @{setting
    2.40 -  ISABELLE_PLATFORM} but refers to the proper 64 bit variant on a platform
    2.41 -  that supports this; the value is empty for 32 bit. Note that the following
    2.42 -  bash expression (including the quotes) prefers the 64 bit platform, if that
    2.43 -  is available:
    2.44 +  \<^descr>[@{setting_def ISABELLE_WINDOWS_PLATFORM32}\<open>\<^sup>*\<close>, @{setting_def
    2.45 +  ISABELLE_WINDOWS_PLATFORM64}\<open>\<^sup>*\<close>,] @{setting_def
    2.46 +  ISABELLE_WINDOWS_PLATFORM}\<open>\<^sup>*\<close> indicate the native Windows platform. These
    2.47 +  settings are analogous (but independent) of those for the standard Posix
    2.48 +  subsystem: @{setting ISABELLE_PLATFORM32}, @{setting ISABELLE_PLATFORM64},
    2.49 +  @{setting ISABELLE_PLATFORM}.
    2.50  
    2.51 -  @{verbatim [display] \<open>"${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM}"\<close>}
    2.52 +  In GNU bash scripts, a preference for native Windows platform variants may
    2.53 +  be specified like this:
    2.54 +
    2.55 +  @{verbatim [display] \<open>"${ISABELLE_WINDOWS_PLATFORM:-$ISABELLE_PLATFORM}"\<close>}
    2.56 +
    2.57 +  @{verbatim [display] \<open>"${ISABELLE_WINDOWS_PLATFORM64:-${ISABELLE_WINDOWS_PLATFORM32:-${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM32}}}"\<close>}
    2.58  
    2.59    \<^descr>[@{setting ISABELLE_TOOL}\<open>\<^sup>*\<close>] is automatically set to the full path name
    2.60    of the @{executable isabelle} executable. Thus other tools and scripts need