# HG changeset patch
# User wenzelm
# Date 1412868710 -7200
# Node ID 8d108c0e7da240ba7634948f9cfbb846a5ed0c3d
# Parent  3094b0edd6b52a6c9b85e91147bdb6e475dc1531# Parent  5697ae9a683a10a7cf854d8a60a04df93cb0104d
merged

diff -r 3094b0edd6b5 -r 8d108c0e7da2 Admin/Windows/Cygwin/Cygwin-Terminal.bat
--- 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
diff -r 3094b0edd6b5 -r 8d108c0e7da2 etc/settings
--- 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"
diff -r 3094b0edd6b5 -r 8d108c0e7da2 lib/Tools/browser
--- 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
diff -r 3094b0edd6b5 -r 8d108c0e7da2 lib/scripts/getsettings
--- 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
diff -r 3094b0edd6b5 -r 8d108c0e7da2 lib/scripts/timestart.bash
--- 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"
diff -r 3094b0edd6b5 -r 8d108c0e7da2 src/Doc/System/Basics.thy
--- 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>
diff -r 3094b0edd6b5 -r 8d108c0e7da2 src/Pure/System/isabelle_system.scala
--- 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 =
diff -r 3094b0edd6b5 -r 8d108c0e7da2 src/Pure/System/system_channel.scala
--- 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)
diff -r 3094b0edd6b5 -r 8d108c0e7da2 src/Tools/jEdit/etc/settings
--- 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"
 
diff -r 3094b0edd6b5 -r 8d108c0e7da2 src/ZF/Induct/Primrec.thy
--- 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}.
 *}
 
 
diff -r 3094b0edd6b5 -r 8d108c0e7da2 src/ZF/Induct/document/root.bib
--- 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}}
+