--- a/Admin/Windows/Cygwin/Cygwin-Terminal.bat Thu Oct 09 11:00:40 2014 +0200
+++ b/Admin/Windows/Cygwin/Cygwin-Terminal.bat Thu Oct 09 17:31:50 2014 +0200
@@ -1,5 +1,6 @@
@echo off
+set TEMP_WINDOWS=%TEMP%
set HOME=%HOMEDRIVE%%HOMEPATH%
set PATH=%CD%\bin;%PATH%
set CHERE_INVOKING=true
--- a/etc/settings Thu Oct 09 11:00:40 2014 +0200
+++ b/etc/settings Thu Oct 09 17:31:50 2014 +0200
@@ -65,7 +65,7 @@
ISABELLE_TOOLS="$ISABELLE_HOME/lib/Tools"
# Location for temporary files (should be on a local file system).
-ISABELLE_TMP_PREFIX="/tmp/isabelle-$USER"
+ISABELLE_TMP_PREFIX="${TMPDIR:-/tmp}/isabelle-$USER"
# Heap input locations. ML system identifier is included in lookup.
ISABELLE_PATH="$ISABELLE_HOME_USER/heaps:$ISABELLE_HOME/heaps"
--- a/lib/Tools/browser Thu Oct 09 11:00:40 2014 +0200
+++ b/lib/Tools/browser Thu Oct 09 17:31:50 2014 +0200
@@ -70,7 +70,7 @@
classpath "$ISABELLE_HOME/lib/browser/GraphBrowser.jar"
if [ -n "$GRAPHFILE" ]; then
- PRIVATE_FILE="${ISABELLE_TMP:-/tmp}/$$"$(basename "$GRAPHFILE")
+ PRIVATE_FILE="${ISABELLE_TMP:-${TMPDIR:-/tmp}}/$$"$(basename "$GRAPHFILE")
if [ -n "$CLEAN" ]; then
mv -f "$GRAPHFILE" "$PRIVATE_FILE" || fail "Cannot move file: $GRAPHFILE"
else
--- a/lib/scripts/getsettings Thu Oct 09 11:00:40 2014 +0200
+++ b/lib/scripts/getsettings Thu Oct 09 17:31:50 2014 +0200
@@ -26,6 +26,12 @@
then
unset INI_DIR
+ if [ -n "$TEMP_WINDOWS" ]; then
+ TMPDIR="$(cygpath -u "$TEMP_WINDOWS")"
+ TMP="$TMPDIR"
+ TEMP="$TMPDIR"
+ fi
+
if [ -z "$USER_HOME" ]; then
USER_HOME="$(cygpath -u "$HOMEDRIVE\\$HOMEPATH")"
fi
--- a/lib/scripts/timestart.bash Thu Oct 09 11:00:40 2014 +0200
+++ b/lib/scripts/timestart.bash Thu Oct 09 17:31:50 2014 +0200
@@ -8,7 +8,7 @@
TIMES_RESULT=""
function get_times () {
- local TMP="/tmp/get_times$$"
+ local TMP="${TMPDIR:-/tmp}/get_times$$"
times > "$TMP" # No pipe here!
TIMES_RESULT="$SECONDS $(echo $(cat "$TMP") | perl -pe 's,\d+m\d+\.\d+s \d+m\d+\.\d+s (\d+)m(\d+)\.\d+s +(\d+)m(\d+)\.\d+s, $1 * 60 + $2 + $3 * 60 + $4,e')"
rm -f "$TMP"
--- a/src/Doc/System/Basics.thy Thu Oct 09 11:00:40 2014 +0200
+++ b/src/Doc/System/Basics.thy Thu Oct 09 17:31:50 2014 +0200
@@ -272,8 +272,7 @@
\item[@{setting_def ISABELLE_TMP_PREFIX}@{text "\<^sup>*"}] is the
prefix from which any running @{executable "isabelle_process"}
- derives an individual directory for temporary files. The default is
- somewhere in @{file_unchecked "/tmp"}.
+ derives an individual directory for temporary files.
\end{description}
\<close>
--- a/src/Pure/System/isabelle_system.scala Thu Oct 09 11:00:40 2014 +0200
+++ b/src/Pure/System/isabelle_system.scala Thu Oct 09 17:31:50 2014 +0200
@@ -76,20 +76,26 @@
set_cygwin_root()
+ def default(env: Map[String, String], entry: (String, String)): Map[String, String] =
+ if (env.isDefinedAt(entry._1) || entry._2 == "") env
+ else env + entry
+
val env =
{
+ val temp_windows =
+ {
+ val temp = System.getenv("TEMP")
+ if (temp != null && temp.contains('\\')) temp else ""
+ }
val user_home = System.getProperty("user.home", "")
val isabelle_app = System.getProperty("isabelle.app", "")
- val env0 = sys.env + ("ISABELLE_JDK_HOME" -> posix_path(jdk_home()))
- val env1 =
- if (user_home == "" || env0.isDefinedAt("HOME")) env0
- else env0 + ("HOME" -> user_home)
- val env2 =
- if (isabelle_app == "") env1
- else env1 + ("ISABELLE_APP" -> "true")
-
- env2
+ default(
+ default(
+ default(sys.env + ("ISABELLE_JDK_HOME" -> posix_path(jdk_home())),
+ ("TEMP_WINDOWS" -> temp_windows)),
+ ("HOME" -> user_home)),
+ ("ISABELLE_APP" -> "true"))
}
val system_home =
--- a/src/Pure/System/system_channel.scala Thu Oct 09 11:00:40 2014 +0200
+++ b/src/Pure/System/system_channel.scala Thu Oct 09 17:31:50 2014 +0200
@@ -43,7 +43,7 @@
{
val i = Fifo_Channel.next_fifo()
val script =
- "FIFO=\"/tmp/isabelle-fifo-${PPID}-$$" + i + "\"\n" +
+ "FIFO=\"${TMPDIR:-/tmp}/isabelle-fifo-${PPID}-$$" + i + "\"\n" +
"echo -n \"$FIFO\"\n" +
"mkfifo -m 600 \"$FIFO\"\n"
val result = Isabelle_System.bash(script)
--- a/src/Tools/jEdit/etc/settings Thu Oct 09 11:00:40 2014 +0200
+++ b/src/Tools/jEdit/etc/settings Thu Oct 09 17:31:50 2014 +0200
@@ -5,7 +5,7 @@
JEDIT_OPTIONS="-reuseview -noserver -nobackground -log=9"
#JEDIT_JAVA_OPTIONS="-Xms128m -Xmx512m -Xss1m"
-JEDIT_JAVA_OPTIONS="-Xms128m -Xmx1024m -Xss2m"
+JEDIT_JAVA_OPTIONS="-Xms128m -Xmx1024m -Xss4m"
#JEDIT_JAVA_OPTIONS="-Xms512m -Xmx4096m -Xss8m"
JEDIT_SYSTEM_OPTIONS="-Dawt.useSystemAAFontSettings=on -Dswing.aatext=true -Dapple.laf.useScreenMenuBar=true -Dapple.awt.application.name=Isabelle"
--- a/src/ZF/Induct/Primrec.thy Thu Oct 09 11:00:40 2014 +0200
+++ b/src/ZF/Induct/Primrec.thy Thu Oct 09 17:31:50 2014 +0200
@@ -10,7 +10,7 @@
text {*
Proof adopted from @{cite szasz93}.
- See also \cite[page 250, exercise 11]{mendelson}.
+ See also @{cite \<open>page 250, exercise 11\<close> mendelson}.
*}
--- a/src/ZF/Induct/document/root.bib Thu Oct 09 11:00:40 2014 +0200
+++ b/src/ZF/Induct/document/root.bib Thu Oct 09 17:31:50 2014 +0200
@@ -27,3 +27,10 @@
publisher = CUP,
year = 1993}
+@book{mendelson,
+ Author = {E. Mendelson},
+ Edition = {Fourth},
+ Publisher = {Chapman \& Hall},
+ Title = {Introduction to Mathematical Logic},
+ Year = {1997}}
+