--- a/Admin/launch4j/isabelle.xml Sun Apr 22 17:54:47 2012 +0200
+++ b/Admin/launch4j/isabelle.xml Sun Apr 22 19:18:26 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="%EXEDIR%"</opt>
</jre>
</launch4jConfig>
\ No newline at end of file
--- a/NEWS Sun Apr 22 17:54:47 2012 +0200
+++ b/NEWS Sun Apr 22 19:18:26 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).
--- a/doc-src/IsarRef/Thy/Misc.thy Sun Apr 22 17:54:47 2012 +0200
+++ b/doc-src/IsarRef/Thy/Misc.thy Sun Apr 22 19:18:26 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
--- a/doc-src/IsarRef/Thy/document/Misc.tex Sun Apr 22 17:54:47 2012 +0200
+++ b/doc-src/IsarRef/Thy/document/Misc.tex Sun Apr 22 19:18:26 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%
%
--- a/doc-src/System/Thy/Basics.thy Sun Apr 22 17:54:47 2012 +0200
+++ b/doc-src/System/Thy/Basics.thy Sun Apr 22 19:18:26 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
--- a/doc-src/System/Thy/document/Basics.tex Sun Apr 22 17:54:47 2012 +0200
+++ b/doc-src/System/Thy/document/Basics.tex Sun Apr 22 19:18:26 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
--- a/etc/settings Sun Apr 22 17:54:47 2012 +0200
+++ b/etc/settings Sun Apr 22 19:18:26 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"
--- a/lib/scripts/getsettings Sun Apr 22 17:54:47 2012 +0200
+++ b/lib/scripts/getsettings Sun Apr 22 19:18:26 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; }
--- a/src/Pure/General/path.ML Sun Apr 22 17:54:47 2012 +0200
+++ b/src/Pure/General/path.ML Sun Apr 22 19:18:26 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
--- a/src/Pure/General/path.scala Sun Apr 22 17:54:47 2012 +0200
+++ b/src/Pure/General/path.scala Sun Apr 22 19:18:26 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)
--- a/src/Pure/System/isabelle_system.scala Sun Apr 22 17:54:47 2012 +0200
+++ b/src/Pure/System/isabelle_system.scala Sun Apr 22 19:18:26 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 =
{
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/System/main.scala Sun Apr 22 19:18:26 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)
+ }
+}
+
--- a/src/Pure/build-jars Sun Apr 22 17:54:47 2012 +0200
+++ b/src/Pure/build-jars Sun Apr 22 19:18:26 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
--- a/src/Tools/jEdit/lib/Tools/jedit Sun Apr 22 17:54:47 2012 +0200
+++ b/src/Tools/jEdit/lib/Tools/jedit Sun Apr 22 19:18:26 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