# HG changeset patch
# User wenzelm
# Date 1335105221 -7200
# Node ID dd253cfa5b23f086fb4edb17ea3966c15ebdf825
# Parent  1bf4fa90cd037e0360c642e1132a632a71c25715# Parent  cf5fe7eb6793a20dd809cb51b2ecd7bb154aa1e7
merged

diff -r 1bf4fa90cd03 -r dd253cfa5b23 Admin/launch4j/isabelle.xml
--- a/Admin/launch4j/isabelle.xml	Sun Apr 22 14:16:46 2012 +0200
+++ b/Admin/launch4j/isabelle.xml	Sun Apr 22 16:33:41 2012 +0200
@@ -1,23 +1,29 @@
 <launch4jConfig>
   <dontWrapJar>true</dontWrapJar>
   <headerType>gui</headerType>
-  <jar>lib\classes\isabelle-scala.jar</jar>
+  <jar></jar>
   <outfile>Isabelle.exe</outfile>
   <errTitle></errTitle>
   <cmdLine></cmdLine>
   <chdir></chdir>
   <priority>normal</priority>
-  <downloadUrl>http://java.com/download</downloadUrl>
+  <downloadUrl></downloadUrl>
   <supportUrl></supportUrl>
   <customProcName>false</customProcName>
   <stayAlive>true</stayAlive>
   <manifest></manifest>
   <icon>isabelle.ico</icon>
+  <classPath>
+    <mainClass>isabelle.Main</mainClass>
+    <cp>lib\classes\ext\Pure.jar</cp>
+    <cp>lib\classes\ext\scala-library.jar</cp>
+    <cp>lib\classes\ext\scala-swing.jar</cp>
+  </classPath>
   <jre>
-    <path></path>
-    <minVersion>1.6.0</minVersion>
+    <path>contrib\jdk-7u3_x86-cygwin\jdk1.7.0_03</path>
+    <minVersion></minVersion>
     <maxVersion></maxVersion>
-    <jdkPreference>preferJre</jdkPreference>
+    <jdkPreference>jdkOnly</jdkPreference>
     <opt>-Disabelle.home=&quot;%EXEDIR%&quot;</opt>
   </jre>
 </launch4jConfig>
\ No newline at end of file
diff -r 1bf4fa90cd03 -r dd253cfa5b23 NEWS
--- a/NEWS	Sun Apr 22 14:16:46 2012 +0200
+++ b/NEWS	Sun Apr 22 16:33:41 2012 +0200
@@ -869,6 +869,14 @@
 
 *** System ***
 
+* USER_HOME settings variable points to cross-platform user home
+directory, which coincides with HOME on POSIX systems only.  Likewise,
+the Isabelle path specification "~" now expands to $USER_HOME, instead
+of former $HOME.  A different default for USER_HOME may be set
+explicitly in shell environment, before Isabelle settings are
+evaluated.  Minor INCOMPATIBILITY: need to adapt Isabelle path where
+the generic user home was intended.
+
 * ISABELLE_JDK_HOME settings variable points to JDK with javac and jar
 (not just JRE).
 
diff -r 1bf4fa90cd03 -r dd253cfa5b23 doc-src/IsarRef/Thy/Misc.thy
--- a/doc-src/IsarRef/Thy/Misc.thy	Sun Apr 22 14:16:46 2012 +0200
+++ b/doc-src/IsarRef/Thy/Misc.thy	Sun Apr 22 16:33:41 2012 +0200
@@ -143,9 +143,9 @@
   %FIXME proper place (!?)
   Isabelle file specification may contain path variables (e.g.\
   @{verbatim "$ISABELLE_HOME"}) that are expanded accordingly.  Note
-  that @{verbatim "~"} abbreviates @{verbatim "$HOME"}, and @{verbatim
-  "~~"} abbreviates @{verbatim "$ISABELLE_HOME"}.  The general syntax
-  for path specifications follows POSIX conventions.
+  that @{verbatim "~"} abbreviates @{verbatim "$USER_HOME"}, and
+  @{verbatim "~~"} abbreviates @{verbatim "$ISABELLE_HOME"}.  The
+  general syntax for path specifications follows POSIX conventions.
 *}
 
 end
diff -r 1bf4fa90cd03 -r dd253cfa5b23 doc-src/IsarRef/Thy/document/Misc.tex
--- a/doc-src/IsarRef/Thy/document/Misc.tex	Sun Apr 22 14:16:46 2012 +0200
+++ b/doc-src/IsarRef/Thy/document/Misc.tex	Sun Apr 22 16:33:41 2012 +0200
@@ -256,8 +256,9 @@
   %FIXME proper place (!?)
   Isabelle file specification may contain path variables (e.g.\
   \verb|$ISABELLE_HOME|) that are expanded accordingly.  Note
-  that \verb|~| abbreviates \verb|$HOME|, and \verb|~~| abbreviates \verb|$ISABELLE_HOME|.  The general syntax
-  for path specifications follows POSIX conventions.%
+  that \verb|~| abbreviates \verb|$USER_HOME|, and
+  \verb|~~| abbreviates \verb|$ISABELLE_HOME|.  The
+  general syntax for path specifications follows POSIX conventions.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
diff -r 1bf4fa90cd03 -r dd253cfa5b23 doc-src/System/Thy/Basics.thy
--- a/doc-src/System/Thy/Basics.thy	Sun Apr 22 14:16:46 2012 +0200
+++ b/doc-src/System/Thy/Basics.thy	Sun Apr 22 16:33:41 2012 +0200
@@ -96,7 +96,7 @@
   exists) is run in the same way as the site default settings. Note
   that the variable @{setting ISABELLE_HOME_USER} has already been set
   before --- usually to something like @{verbatim
-  "$HOME/.isabelle/IsabelleXXXX"}.
+  "$USER_HOME/.isabelle/IsabelleXXXX"}.
   
   Thus individual users may override the site-wide defaults.  See also
   file @{file "$ISABELLE_HOME/etc/user-settings.sample"} in the
@@ -149,19 +149,24 @@
 
   \begin{description}
 
-  \item[@{setting_def ISABELLE_HOME}@{text "\<^sup>*"}] is the
-  location of the top-level Isabelle distribution directory. This is
-  automatically determined from the Isabelle executable that has been
-  invoked.  Do not attempt to set @{setting ISABELLE_HOME} yourself
-  from the shell!
+  \item[@{setting_def USER_HOME}@{text "\<^sup>*"}] Is the
+  cross-platform user home directory.  On Unix systems this is usually
+  the same as @{setting HOME}, but on Windows it is the regular home
+  directory of the user, not the one of within the Cygwin root
+  file-system.
+
+ \item[@{setting_def ISABELLE_HOME}@{text "\<^sup>*"}] is the location of the
+  top-level Isabelle distribution directory. This is automatically
+  determined from the Isabelle executable that has been invoked.  Do
+  not attempt to set @{setting ISABELLE_HOME} yourself from the shell!
   
   \item[@{setting_def ISABELLE_HOME_USER}] is the user-specific
   counterpart of @{setting ISABELLE_HOME}. The default value is
-  relative to @{verbatim "$HOME/.isabelle"}, under rare circumstances
-  this may be changed in the global setting file.  Typically, the
-  @{setting ISABELLE_HOME_USER} directory mimics @{setting
-  ISABELLE_HOME} to some extend. In particular, site-wide defaults may
-  be overridden by a private @{verbatim
+  relative to @{verbatim "$USER_HOME/.isabelle"}, under rare
+  circumstances this may be changed in the global setting file.
+  Typically, the @{setting ISABELLE_HOME_USER} directory mimics
+  @{setting ISABELLE_HOME} to 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
diff -r 1bf4fa90cd03 -r dd253cfa5b23 doc-src/System/Thy/document/Basics.tex
--- a/doc-src/System/Thy/document/Basics.tex	Sun Apr 22 14:16:46 2012 +0200
+++ b/doc-src/System/Thy/document/Basics.tex	Sun Apr 22 16:33:41 2012 +0200
@@ -114,7 +114,7 @@
   \item The file \verb|$ISABELLE_HOME_USER/etc/settings| (if it
   exists) is run in the same way as the site default settings. Note
   that the variable \hyperlink{setting.ISABELLE-HOME-USER}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}HOME{\isaliteral{5F}{\isacharunderscore}}USER}}}} has already been set
-  before --- usually to something like \verb|$HOME/.isabelle/IsabelleXXXX|.
+  before --- usually to something like \verb|$USER_HOME/.isabelle/IsabelleXXXX|.
   
   Thus individual users may override the site-wide defaults.  See also
   file \verb|$ISABELLE_HOME/etc/user-settings.sample| in the
@@ -167,18 +167,23 @@
 
   \begin{description}
 
-  \item[\indexdef{}{setting}{ISABELLE\_HOME}\hypertarget{setting.ISABELLE-HOME}{\hyperlink{setting.ISABELLE-HOME}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}HOME}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}}] is the
-  location of the top-level Isabelle distribution directory. This is
-  automatically determined from the Isabelle executable that has been
-  invoked.  Do not attempt to set \hyperlink{setting.ISABELLE-HOME}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}HOME}}}} yourself
-  from the shell!
+  \item[\indexdef{}{setting}{USER\_HOME}\hypertarget{setting.USER-HOME}{\hyperlink{setting.USER-HOME}{\mbox{\isa{\isatt{USER{\isaliteral{5F}{\isacharunderscore}}HOME}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}}] Is the cross-platform
+  user home directory.  On Unix systems this is usually the same as
+  \hyperlink{setting.HOME}{\mbox{\isa{\isatt{HOME}}}}, but on Windows it is the regular home directory of
+  the, not the one of within the Cygwin root file-system.
+
+ \item[\indexdef{}{setting}{ISABELLE\_HOME}\hypertarget{setting.ISABELLE-HOME}{\hyperlink{setting.ISABELLE-HOME}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}HOME}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}}] is the location of the
+  top-level Isabelle distribution directory. This is automatically
+  determined from the Isabelle executable that has been invoked.  Do
+  not attempt to set \hyperlink{setting.ISABELLE-HOME}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}HOME}}}} yourself from the shell!
   
   \item[\indexdef{}{setting}{ISABELLE\_HOME\_USER}\hypertarget{setting.ISABELLE-HOME-USER}{\hyperlink{setting.ISABELLE-HOME-USER}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}HOME{\isaliteral{5F}{\isacharunderscore}}USER}}}}}] is the user-specific
   counterpart of \hyperlink{setting.ISABELLE-HOME}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}HOME}}}}. The default value is
-  relative to \verb|$HOME/.isabelle|, under rare circumstances
-  this may be changed in the global setting file.  Typically, the
-  \hyperlink{setting.ISABELLE-HOME-USER}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}HOME{\isaliteral{5F}{\isacharunderscore}}USER}}}} directory mimics \hyperlink{setting.ISABELLE-HOME}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}HOME}}}} to some extend. In particular, site-wide defaults may
-  be overridden by a private \verb|$ISABELLE_HOME_USER/etc/settings|.
+  relative to \verb|$USER_HOME/.isabelle|, under rare
+  circumstances this may be changed in the global setting file.
+  Typically, the \hyperlink{setting.ISABELLE-HOME-USER}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}HOME{\isaliteral{5F}{\isacharunderscore}}USER}}}} directory mimics
+  \hyperlink{setting.ISABELLE-HOME}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}HOME}}}} to 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{\isaliteral{5F}{\isacharunderscore}}PLATFORM}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}}] is automatically
   set to a symbolic identifier for the underlying hardware and
diff -r 1bf4fa90cd03 -r dd253cfa5b23 etc/settings
--- a/etc/settings	Sun Apr 22 14:16:46 2012 +0200
+++ b/etc/settings	Sun Apr 22 16:33:41 2012 +0200
@@ -93,7 +93,7 @@
 ###
 
 # The place for user configuration, heap files, etc.
-ISABELLE_HOME_USER="$HOME/.isabelle/${ISABELLE_IDENTIFIER:-.}"
+ISABELLE_HOME_USER="$USER_HOME/.isabelle/${ISABELLE_IDENTIFIER:-.}"
 
 # Where to look for isabelle tools (multiple dirs separated by ':').
 ISABELLE_TOOLS="$ISABELLE_HOME/lib/Tools"
diff -r 1bf4fa90cd03 -r dd253cfa5b23 lib/scripts/getsettings
--- a/lib/scripts/getsettings	Sun Apr 22 14:16:46 2012 +0200
+++ b/lib/scripts/getsettings	Sun Apr 22 16:33:41 2012 +0200
@@ -11,9 +11,13 @@
 
 ISABELLE_SETTINGS_PRESENT=true
 
-#JVM path wrapper
+#Cygwin vs Posix
 if [ "$OSTYPE" = cygwin ]
 then
+  if [ -z "$USER_HOME" ]; then
+    USER_HOME="$(cygpath -u "$HOMEDRIVE\\$HOMEPATH")"
+  fi
+
   ISABELLE_HOME_WINDOWS="$(cygpath -w "$(dirname "$ISABELLE_HOME")")\\$(basename "$ISABELLE_HOME")"
   ISABELLE_HOME="$(cygpath -u "$ISABELLE_HOME_WINDOWS")"
 
@@ -21,10 +25,13 @@
   function jvmpath() { cygpath -i -C UTF8 -w -p "$@"; }
   THIS_CYGWIN="$(jvmpath "/")"
 else
+  if [ -z "$USER_HOME" ]; then
+    USER_HOME="$HOME"
+  fi
+
   function jvmpath() { echo "$@"; }
   CLASSPATH="$CLASSPATH"
 fi
-HOME_JVM="$HOME"
 
 export ISABELLE_HOME
 if { echo -n "$ISABELLE_HOME" | fgrep " " >/dev/null; }
diff -r 1bf4fa90cd03 -r dd253cfa5b23 src/Pure/General/path.ML
--- a/src/Pure/General/path.ML	Sun Apr 22 14:16:46 2012 +0200
+++ b/src/Pure/General/path.ML	Sun Apr 22 16:33:41 2012 +0200
@@ -127,7 +127,7 @@
 local
 
 fun explode_elem ".." = Parent
-  | explode_elem "~" = Variable "HOME"
+  | explode_elem "~" = Variable "USER_HOME"
   | explode_elem "~~" = Variable "ISABELLE_HOME"
   | explode_elem s =
       (case raw_explode s of
diff -r 1bf4fa90cd03 -r dd253cfa5b23 src/Pure/General/path.scala
--- a/src/Pure/General/path.scala	Sun Apr 22 14:16:46 2012 +0200
+++ b/src/Pure/General/path.scala	Sun Apr 22 16:33:41 2012 +0200
@@ -72,7 +72,7 @@
 
   private def explode_elem(s: String): Elem =
     if (s == "..") Parent
-    else if (s == "~") Variable("HOME")
+    else if (s == "~") Variable("USER_HOME")
     else if (s == "~~") Variable("ISABELLE_HOME")
     else if (s.startsWith("$")) variable_elem(s.substring(1))
     else basic_elem(s)
diff -r 1bf4fa90cd03 -r dd253cfa5b23 src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Sun Apr 22 14:16:46 2012 +0200
+++ b/src/Pure/System/isabelle_system.scala	Sun Apr 22 16:33:41 2012 +0200
@@ -79,9 +79,7 @@
                   if (i <= 0) (entry -> "")
                   else (entry.substring(0, i) -> entry.substring(i + 1))
                 }
-              Map(entries: _*) +
-                ("HOME" -> System.getenv("HOME")) +
-                ("PATH" -> System.getenv("PATH"))
+              Map(entries: _*) + ("PATH" -> System.getenv("PATH"))
             }
           }
       _state = Some(State(standard_system, settings))
@@ -91,8 +89,7 @@
 
   /* getenv */
 
-  def getenv(name: String): String =
-    settings.getOrElse(if (name == "HOME") "HOME_JVM" else name, "")
+  def getenv(name: String): String = settings.getOrElse(name, "")
 
   def getenv_strict(name: String): String =
   {
diff -r 1bf4fa90cd03 -r dd253cfa5b23 src/Pure/System/main.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/System/main.scala	Sun Apr 22 16:33:41 2012 +0200
@@ -0,0 +1,33 @@
+/*  Title:      Pure/System/main.scala
+    Author:     Makarius
+
+Default Isabelle application wrapper.
+*/
+
+package isabelle
+
+import scala.swing.TextArea
+
+
+object Main
+{
+  def main(args: Array[String]) =
+  {
+    val (out, rc) =
+      try {
+        Platform.init_laf()
+        Isabelle_System.init()
+        Isabelle_System.isabelle_tool("jedit", args: _*)
+      }
+      catch { case exn: Throwable => (Exn.message(exn), 2) }
+
+    if (rc != 0) {
+      val text = new TextArea(out + "\nReturn code: " + rc)
+      text.editable = false
+      Library.dialog(null, "Isabelle", "Isabelle output", text)
+    }
+
+    System.exit(rc)
+  }
+}
+
diff -r 1bf4fa90cd03 -r dd253cfa5b23 src/Pure/build-jars
--- a/src/Pure/build-jars	Sun Apr 22 14:16:46 2012 +0200
+++ b/src/Pure/build-jars	Sun Apr 22 16:33:41 2012 +0200
@@ -47,6 +47,7 @@
   System/isabelle_charset.scala
   System/isabelle_process.scala
   System/isabelle_system.scala
+  System/main.scala
   System/platform.scala
   System/session.scala
   System/session_manager.scala
diff -r 1bf4fa90cd03 -r dd253cfa5b23 src/Tools/jEdit/lib/Tools/jedit
--- a/src/Tools/jEdit/lib/Tools/jedit	Sun Apr 22 14:16:46 2012 +0200
+++ b/src/Tools/jEdit/lib/Tools/jedit	Sun Apr 22 16:33:41 2012 +0200
@@ -189,8 +189,10 @@
   else
     if [ -n "$ISABELLE_JEDIT_BUILD_HOME" ]; then
       declare -a DEPS=("$JEDIT_JAR" "${JEDIT_JARS[@]}" "$PURE_JAR" "${SOURCES[@]}" "${RESOURCES[@]}")
+    elif [ -e "$ISABELLE_HOME/Admin/build" ]; then
+      declare -a DEPS=("$PURE_JAR" "${SOURCES[@]}" "${RESOURCES[@]}")
     else
-      declare -a DEPS=("$PURE_JAR" "${SOURCES[@]}" "${RESOURCES[@]}")
+      declare -a DEPS=()
     fi
     for DEP in "${DEPS[@]}"
     do