# HG changeset patch
# User wenzelm
# Date 1271537909 -7200
# Node ID cbb9ee265cddd0bf217636af7cfd28dc35f23a9c
# Parent  9c098598db2a4c41f5e60fbbf9bd3db2c8cbee4a
added ISABELLE_PLATFORM and ISABELLE_PLATFORM64 -- NB: ML and JVM may have a different idea;

diff -r 9c098598db2a -r cbb9ee265cdd doc-src/System/Thy/Basics.thy
--- a/doc-src/System/Thy/Basics.thy	Sat Apr 17 21:40:29 2010 +0200
+++ b/doc-src/System/Thy/Basics.thy	Sat Apr 17 22:58:29 2010 +0200
@@ -162,6 +162,17 @@
   some extend. In particular, site-wide defaults may be overridden by
   a private @{verbatim "$ISABELLE_HOME_USER/etc/settings"}.
   
+  \item[@{setting_def ISABELLE_PLATFORM}@{text "\<^sup>*"}] 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.
+
+  \item[@{setting_def ISABELLE_PLATFORM64}@{text "\<^sup>*"}] 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.
+
   \item[@{setting_def ISABELLE_PROCESS}@{text "\<^sup>*"}, @{setting
   ISABELLE_TOOL}@{text "\<^sup>*"}] are automatically set to the full path
   names of the @{executable "isabelle-process"} and @{executable
diff -r 9c098598db2a -r cbb9ee265cdd doc-src/System/Thy/document/Basics.tex
--- a/doc-src/System/Thy/document/Basics.tex	Sat Apr 17 21:40:29 2010 +0200
+++ b/doc-src/System/Thy/document/Basics.tex	Sat Apr 17 22:58:29 2010 +0200
@@ -180,6 +180,17 @@
   some extend. In particular, site-wide defaults may be overridden by
   a private \verb|$ISABELLE_HOME_USER/etc/settings|.
   
+  \item[\indexdef{}{setting}{ISABELLE\_PLATFORM}\hypertarget{setting.ISABELLE-PLATFORM}{\hyperlink{setting.ISABELLE-PLATFORM}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}PLATFORM}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}}] 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.
+
+  \item[\indexdef{}{setting}{ISABELLE\_PLATFORM64}\hypertarget{setting.ISABELLE-PLATFORM64}{\hyperlink{setting.ISABELLE-PLATFORM64}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}PLATFORM{\isadigit{6}}{\isadigit{4}}}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}}] is similar to
+  \hyperlink{setting.ISABELLE-PLATFORM}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}PLATFORM}}}} but refers to the proper 64 bit variant
+  on a platform that supports this; the value is empty for 32 bit.
+
   \item[\indexdef{}{setting}{ISABELLE\_PROCESS}\hypertarget{setting.ISABELLE-PROCESS}{\hyperlink{setting.ISABELLE-PROCESS}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}PROCESS}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}}, \hyperlink{setting.ISABELLE-TOOL}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}TOOL}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}}] are automatically set to the full path
   names of the \hyperlink{executable.isabelle-process}{\mbox{\isa{\isatt{isabelle{\isacharminus}process}}}} and \hyperlink{executable.isabelle}{\mbox{\isa{\isatt{isabelle}}}} executables, respectively.  Thus other tools and scripts
   need not assume that the \hyperlink{file.$ISABELLE-HOME/bin}{\mbox{\isa{\isatt{{\isachardollar}ISABELLE{\isacharunderscore}HOME{\isacharslash}bin}}}} directory is
diff -r 9c098598db2a -r cbb9ee265cdd lib/scripts/getsettings
--- a/lib/scripts/getsettings	Sat Apr 17 21:40:29 2010 +0200
+++ b/lib/scripts/getsettings	Sat Apr 17 22:58:29 2010 +0200
@@ -27,6 +27,9 @@
   "$ISABELLE_TOOL" "$@"
 }
 
+#platform
+. "$ISABELLE_HOME/lib/scripts/isabelle-platform"
+
 #Isabelle distribution identifier -- filled in automatically!
 ISABELLE_IDENTIFIER=""
 
diff -r 9c098598db2a -r cbb9ee265cdd lib/scripts/isabelle-platform
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/scripts/isabelle-platform	Sat Apr 17 22:58:29 2010 +0200
@@ -0,0 +1,63 @@
+#
+# determine general hardware and operating system type for Isabelle
+#
+# NOTE: The ML system or JVM may have their own idea about the platform!
+
+ISABELLE_PLATFORM="unknown-platform"
+ISABELLE_PLATFORM64=""
+
+case $(uname -s) in
+  Linux)
+    case $(uname -m) in
+      i?86)
+        ISABELLE_PLATFORM=x86-linux
+        ;;
+      x86_64)
+        ISABELLE_PLATFORM=x86-linux
+        ISABELLE_PLATFORM64=x86_64-linux
+        ;;
+    esac
+    ;;
+  Darwin)
+    case $(uname -m) in
+      i?86)
+        ISABELLE_PLATFORM=x86-darwin
+        if [ "$(sysctl -n hw.optional.x86_64 2>/dev/null)" = 1 ]; then
+          ISABELLE_PLATFORM64=x86_64-darwin
+        fi
+        ;;
+      Power* | power* | ppc)
+        ISABELLE_PLATFORM=ppc-darwin
+        ;;
+    esac
+    ;;
+  CYGWIN_NT*)
+    case $(uname -m) in
+      i?86)
+        ISABELLE_PLATFORM=x86-cygwin
+        ;;
+    esac
+    ;;
+  SunOS)
+    case $(uname -r) in
+      5.*)
+        case $(uname -p) in
+          sparc)
+            ISABELLE_PLATFORM=sparc-solaris
+            ;;
+          i?86)
+            ISABELLE_PLATFORM=x86-solaris
+            ;;
+        esac
+        ;;
+    esac
+    ;;
+  FreeBSD|NetBSD)
+    case $(uname -m) in
+      i?86)
+        ISABELLE_PLATFORM=x86-bsd
+        ;;
+    esac
+    ;;
+esac
+