# HG changeset patch
# User wenzelm
# Date 1374010473 -7200
# Node ID c16f35e5a5aa3861a5f94dc1230d8859363de879
# Parent  c7cae5ce217d3614855ce3b9edc8817d101c01ed# Parent  24e02408feed4dd57bf67a49e3ff487dd49c3597
merged

diff -r c7cae5ce217d -r c16f35e5a5aa Admin/MacOS/App3/Info.plist
--- a/Admin/MacOS/App3/Info.plist	Tue Jul 16 15:59:55 2013 +0200
+++ b/Admin/MacOS/App3/Info.plist	Tue Jul 16 23:34:33 2013 +0200
@@ -11,11 +11,11 @@
 <key>CFBundleIdentifier</key>
 <string>de.tum.in.isabelle</string>
 <key>CFBundleDisplayName</key>
-<string>Isabelle</string>
+<string>{ISABELLE_NAME}</string>
 <key>CFBundleInfoDictionaryVersion</key>
 <string>6.0</string>
 <key>CFBundleName</key>
-<string>Isabelle</string>
+<string>{ISABELLE_NAME}</string>
 <key>CFBundlePackageType</key>
 <string>APPL</string>
 <key>CFBundleShortVersionString</key>
@@ -35,7 +35,7 @@
 <key>JVMOptions</key>
 <array>
 <string>-Dapple.laf.useScreenMenuBar=true</string>
-<string>-Disabelle.home=$APP_ROOT/Isabelle</string>
+<string>-Disabelle.home=$APP_ROOT/Contents/Resources/{ISABELLE_NAME}</string>
 </array>
 <key>JVMArguments</key>
 <array>
diff -r c7cae5ce217d -r c16f35e5a5aa Admin/MacOS/App3/mk
--- a/Admin/MacOS/App3/mk	Tue Jul 16 15:59:55 2013 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,27 +0,0 @@
-#!/bin/bash
-#
-# Make Isabelle/JVM application bundle
-
-THIS="$(cd "$(dirname "$0")"; pwd)"
-
-APP="$THIS/Isabelle.app"
-
-for NAME in Java MacOS PlugIns Resources
-do
-  mkdir -p "$APP/Contents/$NAME"
-done
-
-cp "$THIS/Info.plist" "$APP/Contents/."
-
-for NAME in Pure.jar scala-library.jar scala-swing.jar
-do
-  ln -sf "../Resources/Isabelle/lib/classes/ext/$NAME" "$APP/Contents/Java"
-done
-
-cp -R "$THIS/Resources/." "$APP/Contents/Resources/."
-cp "$THIS/../isabelle.icns" "$APP/Contents/Resources/."
-
-ln -sf "../Resources/Isabelle/contrib/jdk-7u13/x86_64-darwin/jdk1.7.0_13.jdk" "$APP/Contents/PlugIns/jdk"
-
-cp "$THIS/JavaAppLauncher" "$APP/Contents/MacOS/." && chmod +x "$APP/Contents/MacOS/JavaAppLauncher"
-
diff -r c7cae5ce217d -r c16f35e5a5aa Admin/Release/CHECKLIST
--- a/Admin/Release/CHECKLIST	Tue Jul 16 15:59:55 2013 +0200
+++ b/Admin/Release/CHECKLIST	Tue Jul 16 23:34:33 2013 +0200
@@ -50,9 +50,9 @@
 Packaging
 =========
 
-- hg up -r DISTNAME && Admin/Release/build -r DISTNAME /home/isabelle/dist
+- fully-automated packaging (requires Mac OS X):
 
-- manual packaging of .app (Mac OS) and .exe (Windows)
+  hg up -r DISTNAME && Admin/Release/build -r DISTNAME /home/isabelle/dist
 
 
 Final release stage
diff -r c7cae5ce217d -r c16f35e5a5aa Admin/Windows/Cygwin/isabelle/init.bat
--- a/Admin/Windows/Cygwin/isabelle/init.bat	Tue Jul 16 15:59:55 2013 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,11 +0,0 @@
-@echo off
-
-cd "%~dp0"
-cd "..\..\.."
-
-set CYGWIN=nodosfilewarning
-
-echo Initializing Cygwin ...
-"contrib\cygwin\bin\dash" /isabelle/rebaseall
-"contrib\cygwin\bin\bash" /isabelle/postinstall
-
diff -r c7cae5ce217d -r c16f35e5a5aa Admin/Windows/Cygwin/isabelle/postinstall
--- a/Admin/Windows/Cygwin/isabelle/postinstall	Tue Jul 16 15:59:55 2013 +0200
+++ b/Admin/Windows/Cygwin/isabelle/postinstall	Tue Jul 16 23:34:33 2013 +0200
@@ -1,9 +1,14 @@
 #!/bin/bash
 
-PATH=/bin
+export PATH=/bin
 
 bash /etc/postinstall/base-files-mketc.sh.done
 
 mkpasswd -l >/etc/passwd
 mkgroup -l >/etc/group
 
+find -type d -exec chmod 755 '{}' +
+find -type f \( -name '*.exe' -o -name '*.dll' \) -exec chmod 755 '{}' +
+find -type f -not -name '*.exe' -not -name '*.dll' -exec chmod 644 '{}' +
+xargs -0 < contrib/cygwin/isabelle/executables chmod 755
+
diff -r c7cae5ce217d -r c16f35e5a5aa Admin/Windows/Cygwin/isabelle/rebaseall
--- a/Admin/Windows/Cygwin/isabelle/rebaseall	Tue Jul 16 15:59:55 2013 +0200
+++ b/Admin/Windows/Cygwin/isabelle/rebaseall	Tue Jul 16 23:34:33 2013 +0200
@@ -1,6 +1,6 @@
 #!/bin/dash
 
-PATH=/bin
+export PATH=/bin
 
 FILE_LIST="$(mktemp)"
 
diff -r c7cae5ce217d -r c16f35e5a5aa Admin/Windows/Installer/sfx.txt
--- a/Admin/Windows/Installer/sfx.txt	Tue Jul 16 15:59:55 2013 +0200
+++ b/Admin/Windows/Installer/sfx.txt	Tue Jul 16 23:34:33 2013 +0200
@@ -1,9 +1,9 @@
 ;!@Install@!UTF-8!
 GUIFlags="64"
 InstallPath="%UserDesktop%"
-BeginPrompt="Unpack Isabelle2013?"
+BeginPrompt="Unpack {ISABELLE_NAME}?"
 ExtractPathText="Target directory"
-ExtractTitle="Unpacking Isabelle2013 ..."
-Shortcut="Du,{%%T\Isabelle2013\Isabelle2013.exe},{},{},{},{Isabelle2013},{%%T\Isabelle2013}"
-RunProgram="\"%%T\Isabelle2013\contrib\cygwin\isabelle\init.bat\""
+ExtractTitle="Unpacking {ISABELLE_NAME} ..."
+Shortcut="Du,{%%T\{ISABELLE_NAME}\{ISABELLE_NAME}.exe},{},{},{},{{ISABELLE_NAME}},{%%T\{ISABELLE_NAME}}"
+RunProgram="\"%%T\{ISABELLE_NAME}\{ISABELLE_NAME}.exe\" -i"
 ;!@InstallEnd@!
diff -r c7cae5ce217d -r c16f35e5a5aa Admin/Windows/launch4j/Isabelle.exe
Binary file Admin/Windows/launch4j/Isabelle.exe has changed
diff -r c7cae5ce217d -r c16f35e5a5aa Admin/Windows/launch4j/isabelle.xml
--- a/Admin/Windows/launch4j/isabelle.xml	Tue Jul 16 15:59:55 2013 +0200
+++ b/Admin/Windows/launch4j/isabelle.xml	Tue Jul 16 23:34:33 2013 +0200
@@ -20,7 +20,7 @@
     <cp>%EXEDIR%\lib\classes\ext\scala-swing.jar</cp>
   </classPath>
   <jre>
-    <path>%EXEDIR%\contrib\jdk-7u13\x86-cygwin\jdk1.7.0_13</path>
+    <path>%EXEDIR%\contrib\jdk-7u21\x86-cygwin\jdk1.7.0_21</path>
     <minVersion></minVersion>
     <maxVersion></maxVersion>
     <jdkPreference>jdkOnly</jdkPreference>
diff -r c7cae5ce217d -r c16f35e5a5aa Admin/components/bundled-macos
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/components/bundled-macos	Tue Jul 16 23:34:33 2013 +0200
@@ -0,0 +1,2 @@
+#additional components to be bundled for release
+macos_app-20130716
diff -r c7cae5ce217d -r c16f35e5a5aa Admin/components/bundled-windows
--- a/Admin/components/bundled-windows	Tue Jul 16 15:59:55 2013 +0200
+++ b/Admin/components/bundled-windows	Tue Jul 16 23:34:33 2013 +0200
@@ -1,2 +1,3 @@
 #additional components to be bundled for release
 cygwin-20130117
+windows_app-20130716
diff -r c7cae5ce217d -r c16f35e5a5aa Admin/components/components.sha1
--- a/Admin/components/components.sha1	Tue Jul 16 15:59:55 2013 +0200
+++ b/Admin/components/components.sha1	Tue Jul 16 23:34:33 2013 +0200
@@ -2,6 +2,7 @@
 842d9526f37b928cf9e22f141884365129990d63  cygwin-20130110.tar.gz
 cb3b0706d208f104b800267697204f6d82f7b48a  cygwin-20130114.tar.gz
 3b44cca04855016d5f8cfb5101b2e0579ab80197  cygwin-20130117.tar.gz
+1fde9ddf0fa4f398965113d0c0c4f0e97c78d008  cygwin-20130716.tar.gz
 0fe549949a025d65d52d6deca30554de8fca3b6e  e-1.5.tar.gz
 2e293256a134eb8e5b1a283361b15eb812fbfbf1  e-1.6-1.tar.gz
 e1919e72416cbd7ac8de5455caba8901acc7b44d  e-1.6-2.tar.gz
@@ -32,6 +33,7 @@
 8122526f1fc362ddae1a328bdbc2152853186fee  jfreechart-1.0.14.tar.gz
 6c737137cc597fc920943783382e928ea79e3feb  kodkodi-1.2.16.tar.gz
 5f95c96bb99927f3a026050f85bd056f37a9189e  kodkodi-1.5.2.tar.gz
+0aab4f73ff7f5e36f33276547e10897e1e56fb1d  macos_app-20130716.tar.gz
 1c8cb6a8f4cbeaedce2d6d1ba8fc7e2ab3663aeb  polyml-5.4.1.tar.gz
 a3f9c159a0ee9a63b7a5d0c835ed9c2c908f8b56  polyml-5.5.0-1.tar.gz
 7d604a99355efbfc1459d80db3279ffa7ade3e39  polyml-5.5.0-2.tar.gz
@@ -48,6 +50,7 @@
 43b5afbcad575ab6817d2289756ca22fd2ef43a9  spass-3.8ds.tar.gz
 1f4a2053cc1f34fa36c4d9d2ac906ad4ebc863fd  sumatra_pdf-2.1.1.tar.gz
 869ea6d8ea35c8ba68d7fcb028f16b2b7064c5fd  vampire-1.0.tar.gz
+81d21dfd0ea5c58f375301f5166be9dbf8921a7a  windows_app-20130716.tar.gz
 2ae13aa17d0dc95ce254a52f1dba10929763a10d  xz-java-1.2.tar.gz
 4530a1aa6f4498ee3d78d6000fa71a3f63bd077f  yices-1.0.28.tar.gz
 12ae71acde43bd7bed1e005c43034b208c0cba4c  z3-3.2.tar.gz
diff -r c7cae5ce217d -r c16f35e5a5aa Admin/lib/Tools/makedist_bundle
--- a/Admin/lib/Tools/makedist_bundle	Tue Jul 16 15:59:55 2013 +0200
+++ b/Admin/lib/Tools/makedist_bundle	Tue Jul 16 23:34:33 2013 +0200
@@ -121,6 +121,7 @@
     ;;
   macos)
     purge_contrib '-name "x86*-linux" -o -name "x86*-cygwin" -o -name "x86*-windows"'
+    mv "$ISABELLE_TARGET/contrib/macos_app" "$TMP/."
 
     perl -pi -e "s,lookAndFeel=.*,lookAndFeel=com.apple.laf.AquaLookAndFeel,g;" \
       -e "s,delete-line.shortcut=.*,delete-line.shortcut=C+d,g;" \
@@ -129,11 +130,12 @@
     ;;
   windows)
     purge_contrib '-name "x86*-linux" -o -name "x86*-darwin"'
+    mv "$ISABELLE_TARGET/contrib/windows_app" "$TMP/."
 
     perl -pi -e "s,lookAndFeel=.*,lookAndFeel=com.sun.java.swing.plaf.windows.WindowsLookAndFeel,g;" \
       "$TMP/$ISABELLE_NAME/src/Tools/jEdit/dist/properties/jEdit.props"
 
-    cp "$ISABELLE_HOME/Admin/Windows/launch4j/Isabelle.exe" "$ISABELLE_TARGET/Isabelle2013.exe"
+    cp "$TMP/windows_app/Isabelle.exe" "$ISABELLE_TARGET/${ISABELLE_NAME}.exe"
     cp "$ISABELLE_HOME/Admin/Windows/Cygwin/Cygwin-Setup.bat" \
       "$ISABELLE_HOME/Admin/Windows/Cygwin/Cygwin-Latex-Setup.bat" \
       "$ISABELLE_HOME/Admin/Windows/Cygwin/Cygwin-Terminal.bat" "$ISABELLE_TARGET"
@@ -141,7 +143,7 @@
     (
       cd "$ISABELLE_TARGET"
 
-      for NAME in init.bat postinstall rebaseall
+      for NAME in postinstall rebaseall
       do
         cp -a "$ISABELLE_HOME/Admin/Windows/Cygwin/isabelle/$NAME" \
           "contrib/cygwin/isabelle/."
@@ -150,15 +152,8 @@
       find . -type f -not -name '*.exe' -not -name '*.dll' -perm +100 \
         -print0 > "contrib/cygwin/isabelle/executables"
 
-      cat >> "contrib/cygwin/isabelle/postinstall" <<EOF
-
-find -type d -exec chmod 755 '{}' +
-find -type f \( -name '*.exe' -o -name '*.dll' \) -exec chmod 755 '{}' +
-find -type f -not -name '*.exe' -not -name '*.dll' -exec chmod 644 '{}' +
-xargs -0 < contrib/cygwin/isabelle/executables chmod 755
-
-EOF
-
+      find . -type l -exec echo "{}" ";" -exec readlink "{}" ";" \
+        > "contrib/cygwin/isabelle/symlinks"
     )
 
     perl -pi -e "s,/bin/rebaseall.*,/isabelle/rebaseall,g;" \
@@ -178,5 +173,71 @@
 tar -C "$TMP" -c -z -f "$BUNDLE_ARCHIVE" "$ISABELLE_NAME" || exit 2
 
 
+# application
+
+if [ "$ISABELLE_PLATFORM_FAMILY" = linux -a "$PLATFORM_FAMILY" != macos -o "$ISABELLE_PLATFORM_FAMILY" = macos ]
+then
+  case "$PLATFORM_FAMILY" in
+    macos)
+      echo "application for $PLATFORM_FAMILY"
+      (
+        cd "$TMP"
+
+        APP_TEMPLATE="$ISABELLE_HOME/Admin/MacOS/App3"
+        APP="${ISABELLE_NAME}.app"
+
+        for NAME in Java MacOS PlugIns Resources
+        do
+          mkdir -p "$APP/Contents/$NAME"
+        done
+
+        cat "$APP_TEMPLATE/Info.plist" | \
+          perl -p -e "s,{ISABELLE_NAME},${ISABELLE_NAME},g;" > "$APP/Contents/Info.plist"
+
+        for NAME in Pure.jar scala-library.jar scala-swing.jar
+        do
+          ln -sf "../Resources/${ISABELLE_NAME}/lib/classes/ext/$NAME" "$APP/Contents/Java"
+        done
+
+        cp -R "$APP_TEMPLATE/Resources/." "$APP/Contents/Resources/."
+        cp "$APP_TEMPLATE/../isabelle.icns" "$APP/Contents/Resources/."
+
+        ln -sf "../Resources/${ISABELLE_NAME}/contrib/jdk-7u21/x86_64-darwin/jdk1.7.0_21.jdk" \
+          "$APP/Contents/PlugIns/jdk"
+
+        cp macos_app/JavaAppLauncher "$APP/Contents/MacOS/." && \
+          chmod +x "$APP/Contents/MacOS/JavaAppLauncher"
+
+        mv "$ISABELLE_NAME" "$APP/Contents/Resources/."
+        ln -sf "Contents/Resources/$ISABELLE_NAME" "$APP/Isabelle"
+
+        rm -f "${ARCHIVE_DIR}/${ISABELLE_NAME}.dmg"
+        hdiutil create -srcfolder "$APP" "${ARCHIVE_DIR}/${ISABELLE_NAME}.dmg"
+      )
+      ;;
+    windows)
+      (
+        cd "$TMP"
+        rm -f "${ARCHIVE_DIR}/${ISABELLE_NAME}.7z"
+        7z -y -bd a "$TMP/${ISABELLE_NAME}.7z" "$ISABELLE_NAME" || exit 2
+
+        echo "application for $PLATFORM_FAMILY"
+        (
+          cat "windows_app/7zsd_All.sfx"
+          cat "$ISABELLE_HOME/Admin/Windows/Installer/sfx.txt" | \
+            perl -p -e "s,{ISABELLE_NAME},${ISABELLE_NAME},g;"
+          cat "$TMP/${ISABELLE_NAME}.7z"
+        ) > "${ARCHIVE_DIR}/${ISABELLE_NAME}.exe"
+        chmod +x "${ARCHIVE_DIR}/${ISABELLE_NAME}.exe"
+      )
+      ;;
+    *)
+      ;;
+  esac
+else
+  echo "### Cannot build application for $PLATFORM_FAMILY on $ISABELLE_PLATFORM_FAMILY"
+fi
+
+
 # clean up
 rm -rf "$TMP"
diff -r c7cae5ce217d -r c16f35e5a5aa Isabelle
--- a/Isabelle	Tue Jul 16 15:59:55 2013 +0200
+++ b/Isabelle	Tue Jul 16 23:34:33 2013 +0200
@@ -4,5 +4,5 @@
 #
 # Default Isabelle application wrapper.
 
-exec "$(dirname "$0")"/bin/isabelle jedit -s "$@"
+exec "$(dirname "$0")"/bin/isabelle jedit -s -- "$@"
 
diff -r c7cae5ce217d -r c16f35e5a5aa src/Doc/Codegen/Adaptation.thy
--- a/src/Doc/Codegen/Adaptation.thy	Tue Jul 16 15:59:55 2013 +0200
+++ b/src/Doc/Codegen/Adaptation.thy	Tue Jul 16 23:34:33 2013 +0200
@@ -119,7 +119,7 @@
   The @{theory HOL} @{theory Main} theory already provides a code
   generator setup which should be suitable for most applications.
   Common extensions and modifications are available by certain
-  theories in @{text "HOL/Library"}; beside being useful in
+  theories in @{file "~~/src/HOL/Library"}; beside being useful in
   applications, they may serve as a tutorial for customising the code
   generator setup (see below \secref{sec:adaptation_mechanisms}).
 
diff -r c7cae5ce217d -r c16f35e5a5aa src/Doc/Codegen/Further.thy
--- a/src/Doc/Codegen/Further.thy	Tue Jul 16 15:59:55 2013 +0200
+++ b/src/Doc/Codegen/Further.thy	Tue Jul 16 23:34:33 2013 +0200
@@ -222,7 +222,7 @@
 subsection {* Parallel computation *}
 
 text {*
-  Theory @{text Parallel} in @{text "HOL/Library"} contains
+  Theory @{text Parallel} in @{file "~~/src/HOL/Library"} contains
   operations to exploit parallelism inside the Isabelle/ML
   runtime engine.
 *}
diff -r c7cae5ce217d -r c16f35e5a5aa src/Doc/Codegen/Inductive_Predicate.thy
--- a/src/Doc/Codegen/Inductive_Predicate.thy	Tue Jul 16 15:59:55 2013 +0200
+++ b/src/Doc/Codegen/Inductive_Predicate.thy	Tue Jul 16 23:34:33 2013 +0200
@@ -265,7 +265,7 @@
 
 text {*
   Further examples for compiling inductive predicates can be found in
-  the @{text "HOL/Predicate_Compile_Examples.thy"} theory file.  There are
+  @{file "~~/src/HOL/Predicate_Compile_Examples"}.  There are
   also some examples in the Archive of Formal Proofs, notably in the
   @{text "POPLmark-deBruijn"} and the @{text "FeatherweightJava"}
   sessions.
diff -r c7cae5ce217d -r c16f35e5a5aa src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy
--- a/src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy	Tue Jul 16 15:59:55 2013 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy	Tue Jul 16 23:34:33 2013 +0200
@@ -19,7 +19,10 @@
 declare size_list_def[symmetric, code_pred_inline]
 
 
-setup {* Context.theory_map (Quickcheck.add_tester ("prolog", (Code_Prolog.active, Code_Prolog.test_goals))) *}
+setup {*
+  Context.theory_map
+    (Quickcheck.add_tester ("prolog", (Code_Prolog.active, Code_Prolog.test_goals)))
+*}
 
 datatype alphabet = a | b
 
diff -r c7cae5ce217d -r c16f35e5a5aa src/HOL/Predicate_Compile_Examples/Examples.thy
--- a/src/HOL/Predicate_Compile_Examples/Examples.thy	Tue Jul 16 15:59:55 2013 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Examples.thy	Tue Jul 16 23:34:33 2013 +0200
@@ -29,7 +29,8 @@
                          (s1 @ rhs @ s2) = rsl \<and>
                          (rule lhs rhs) \<in> fst g }"
 
-definition derivesp :: "(('nts, 'ts) rule => bool) * 'nts => ('nts, 'ts) symbol list => ('nts, 'ts) symbol list => bool"
+definition derivesp ::
+  "(('nts, 'ts) rule => bool) * 'nts => ('nts, 'ts) symbol list => ('nts, 'ts) symbol list => bool"
 where
   "derivesp g = (\<lambda> lhs rhs. (lhs, rhs) \<in> derives (Collect (fst g), snd g))"
  
@@ -252,7 +253,8 @@
 where
   irconst: "eval_var (IrConst i) conf (IntVal i)"
 | objaddr: "\<lbrakk> Env conf n = i \<rbrakk> \<Longrightarrow> eval_var (ObjAddr n) conf (IntVal i)"
-| plus: "\<lbrakk> eval_var l conf (IntVal vl); eval_var r conf (IntVal vr) \<rbrakk> \<Longrightarrow> eval_var (Add l r) conf (IntVal (vl+vr))"
+| plus: "\<lbrakk> eval_var l conf (IntVal vl); eval_var r conf (IntVal vr) \<rbrakk> \<Longrightarrow>
+    eval_var (Add l r) conf (IntVal (vl+vr))"
 
 
 code_pred eval_var .
diff -r c7cae5ce217d -r c16f35e5a5aa src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy
--- a/src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy	Tue Jul 16 15:59:55 2013 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy	Tue Jul 16 23:34:33 2013 +0200
@@ -31,7 +31,9 @@
 
 lemma [code_pred_def]:
   "cardsp [] g k = False"
-  "cardsp (e # s) g k = (let C = cardsp s g in case e of Check_in g' r c => if g' = g then k = c \<or> C k else C k | _ => C k)"
+  "cardsp (e # s) g k =
+    (let C = cardsp s g
+     in case e of Check_in g' r c => if g' = g then k = c \<or> C k else C k | _ => C k)"
 unfolding cardsp_def [abs_def] cards.simps by (auto simp add: Let_def split: event.split)
 
 definition
@@ -79,7 +81,10 @@
 
 values 40 "{s. hotel s}"
 
-setup {* Context.theory_map (Quickcheck.add_tester ("prolog", (Code_Prolog.active, Code_Prolog.test_goals))) *}
+setup {*
+  Context.theory_map
+    (Quickcheck.add_tester ("prolog", (Code_Prolog.active, Code_Prolog.test_goals)))
+*}
 
 lemma "\<lbrakk> hotel s; isinp s r g \<rbrakk> \<Longrightarrow> owns s r = Some g"
 quickcheck[tester = prolog, iterations = 1, expect = counterexample]
diff -r c7cae5ce217d -r c16f35e5a5aa src/HOL/Predicate_Compile_Examples/Lambda_Example.thy
--- a/src/HOL/Predicate_Compile_Examples/Lambda_Example.thy	Tue Jul 16 15:59:55 2013 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Lambda_Example.thy	Tue Jul 16 23:34:33 2013 +0200
@@ -79,7 +79,10 @@
 
 section {* Manual setup to find counterexample *}
 
-setup {* Context.theory_map (Quickcheck.add_tester ("prolog", (Code_Prolog.active, Code_Prolog.test_goals))) *}
+setup {*
+  Context.theory_map
+    (Quickcheck.add_tester ("prolog", (Code_Prolog.active, Code_Prolog.test_goals)))
+*}
 
 setup {* Code_Prolog.map_code_options (K 
   { ensure_groundness = true,
diff -r c7cae5ce217d -r c16f35e5a5aa src/HOL/Predicate_Compile_Examples/List_Examples.thy
--- a/src/HOL/Predicate_Compile_Examples/List_Examples.thy	Tue Jul 16 15:59:55 2013 +0200
+++ b/src/HOL/Predicate_Compile_Examples/List_Examples.thy	Tue Jul 16 23:34:33 2013 +0200
@@ -5,7 +5,10 @@
   "~~/src/HOL/Library/Code_Prolog"
 begin
 
-setup {* Context.theory_map (Quickcheck.add_tester ("prolog", (Code_Prolog.active, Code_Prolog.test_goals))) *}
+setup {*
+  Context.theory_map
+    (Quickcheck.add_tester ("prolog", (Code_Prolog.active, Code_Prolog.test_goals)))
+*}
 
 setup {* Code_Prolog.map_code_options (K 
   {ensure_groundness = true,
diff -r c7cae5ce217d -r c16f35e5a5aa src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy
--- a/src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy	Tue Jul 16 15:59:55 2013 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy	Tue Jul 16 23:34:33 2013 +0200
@@ -85,7 +85,8 @@
  
 fun prop_regex :: "Nat * Nat * RE * RE * Sym list \<Rightarrow> bool"
 where
-  "prop_regex (n, (k, (p, (q, s)))) = ((accepts (repInt n k (And p q)) s) = (accepts (And (repInt n k p) (repInt n k q)) s))"
+  "prop_regex (n, (k, (p, (q, s)))) =
+    ((accepts (repInt n k (And p q)) s) = (accepts (And (repInt n k p) (repInt n k q)) s))"
 
 
 
@@ -97,7 +98,10 @@
 oops
 
 
-setup {* Context.theory_map (Quickcheck.add_tester ("prolog", (Code_Prolog.active, Code_Prolog.test_goals))) *}
+setup {*
+  Context.theory_map
+    (Quickcheck.add_tester ("prolog", (Code_Prolog.active, Code_Prolog.test_goals)))
+*}
 
 setup {* Code_Prolog.map_code_options (K 
   {ensure_groundness = true,
diff -r c7cae5ce217d -r c16f35e5a5aa src/Pure/General/file.scala
--- a/src/Pure/General/file.scala	Tue Jul 16 15:59:55 2013 +0200
+++ b/src/Pure/General/file.scala	Tue Jul 16 23:34:33 2013 +0200
@@ -14,8 +14,6 @@
 
 import scala.collection.mutable
 
-import org.tukaani.xz.{LZMA2Options, XZInputStream, XZOutputStream}
-
 
 object File
 {
@@ -77,11 +75,6 @@
 
   def read_gzip(path: Path): String = read_gzip(path.file)
 
-  def read_xz(file: JFile): String =
-    read_stream(new XZInputStream(new BufferedInputStream(new FileInputStream(file))))
-
-  def read_xz(path: Path): String = read_xz(path.file)
-
 
   /* read lines */
 
@@ -113,7 +106,7 @@
 
   /* write */
 
-  private def write_file(file: JFile, text: Iterable[CharSequence],
+  def write_file(file: JFile, text: Iterable[CharSequence],
     make_stream: OutputStream => OutputStream)
   {
     val stream = make_stream(new FileOutputStream(file))
@@ -133,14 +126,6 @@
   def write_gzip(path: Path, text: Iterable[CharSequence]): Unit = write_gzip(path.file, text)
   def write_gzip(path: Path, text: CharSequence): Unit = write_gzip(path.file, text)
 
-  def write_xz(file: JFile, text: Iterable[CharSequence], preset: Int = 3)
-  {
-    val options = new LZMA2Options
-    options.setPreset(preset)
-    write_file(file, text, (s: OutputStream) =>
-      new XZOutputStream(new BufferedOutputStream(s), options))
-  }
-
 
   /* copy */
 
diff -r c7cae5ce217d -r c16f35e5a5aa src/Pure/General/xz_file.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/xz_file.scala	Tue Jul 16 23:34:33 2013 +0200
@@ -0,0 +1,31 @@
+/*  Title:      Pure/General/xz_file.scala
+    Author:     Makarius
+
+XZ file system operations.
+*/
+
+package isabelle
+
+
+import java.io.{BufferedOutputStream, OutputStream, FileInputStream, BufferedInputStream,
+  File => JFile}
+
+import org.tukaani.xz.{LZMA2Options, XZInputStream, XZOutputStream}
+
+
+object XZ_File
+{
+  def read(file: JFile): String =
+    File.read_stream(new XZInputStream(new BufferedInputStream(new FileInputStream(file))))
+
+  def read(path: Path): String = read(path.file)
+
+  def write(file: JFile, text: Iterable[CharSequence], preset: Int = 3)
+  {
+    val options = new LZMA2Options
+    options.setPreset(preset)
+    File.write_file(file, text, (s: OutputStream) =>
+      new XZOutputStream(new BufferedOutputStream(s), options))
+  }
+}
+
diff -r c7cae5ce217d -r c16f35e5a5aa src/Pure/ML/ml_context.ML
--- a/src/Pure/ML/ml_context.ML	Tue Jul 16 15:59:55 2013 +0200
+++ b/src/Pure/ML/ml_context.ML	Tue Jul 16 23:34:33 2013 +0200
@@ -131,9 +131,12 @@
   >> (fn ((x, pos), y) => Args.src ((x, y), pos));
 
 val begin_env0 = ML_Lex.tokenize "structure Isabelle =\nstruct\n";
-val begin_env =
+
+fun begin_env visible =
   ML_Lex.tokenize
-    "structure Isabelle =\nstruct\nval ML_context = ML_Context.the_local_context ();\n";
+    ("structure Isabelle =\nstruct\n\
+     \val ML_context = Context_Position.set_visible " ^ Bool.toString visible ^
+     " (ML_Context.the_local_context ());\n");
 
 val end_env = ML_Lex.tokenize "end;";
 val reset_env = ML_Lex.tokenize "structure Isabelle = struct end";
@@ -142,7 +145,12 @@
 
 fun eval_antiquotes (ants, pos) opt_context =
   let
+    val visible =
+      (case opt_context of
+        SOME (Context.Proof ctxt) => Context_Position.is_visible ctxt
+      | _ => true);
     val opt_ctxt = Option.map (Context.Proof o Context.proof_of) opt_context;
+
     val ((ml_env, ml_body), opt_ctxt') =
       if forall Antiquote.is_text ants
       then ((begin_env0, map (fn Antiquote.Text tok => tok) ants), opt_ctxt)
@@ -171,8 +179,9 @@
                 (no_decl, (Stack.pop scope, background));
 
           val (decls, (_, ctxt')) = fold_map expand ants (Stack.init ctxt, ctxt);
-          val (ml_env, ml_body) = decls |> map (fn decl => decl ctxt') |> split_list |> pairself flat;
-        in ((begin_env @ ml_env, ml_body), SOME (Context.Proof ctxt')) end;
+          val (ml_env, ml_body) =
+            decls |> map (fn decl => decl ctxt') |> split_list |> pairself flat;
+        in ((begin_env visible @ ml_env, ml_body), SOME (Context.Proof ctxt')) end;
   in ((ml_env @ end_env, ml_body), opt_ctxt') end;
 
 val trace_raw = Config.declare "ML_trace" (fn _ => Config.Bool false);
diff -r c7cae5ce217d -r c16f35e5a5aa src/Pure/System/cygwin.scala
--- a/src/Pure/System/cygwin.scala	Tue Jul 16 15:59:55 2013 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,31 +0,0 @@
-/*  Title:      Pure/System/cygwin.scala
-    Author:     Makarius
-
-Support for Cygwin.
-*/
-
-package isabelle
-
-
-import java.io.{File => JFile}
-import java.nio.file.{Paths, Files}
-
-
-object Cygwin
-{
-  /* symlinks */
-
-  def write_symlink(file: JFile, content: String)
-  {
-    require(Platform.is_windows)
-
-    val path = file.toPath
-
-    val writer = Files.newBufferedWriter(path, UTF8.charset)
-    try { writer.write("!<symlink>" + content + "\0") }
-    finally { writer.close }
-
-    Files.setAttribute(path, "dos:system", true)
-  }
-}
-
diff -r c7cae5ce217d -r c16f35e5a5aa src/Pure/System/cygwin_init.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/System/cygwin_init.scala	Tue Jul 16 23:34:33 2013 +0200
@@ -0,0 +1,185 @@
+/*  Title:      Pure/System/cygwin_init.scala
+    Author:     Makarius
+
+Initialize Isabelle distribution after extracting via 7zip.
+*/
+
+package isabelle
+
+
+import java.lang.System
+import java.io.{File => JFile, BufferedReader, InputStreamReader}
+import java.nio.file.{Paths, Files}
+import java.awt.{GraphicsEnvironment, Point, Font}
+import javax.swing.ImageIcon
+
+import scala.annotation.tailrec
+import scala.swing.{ScrollPane, Button, FlowPanel,
+  BorderPanel, MainFrame, TextArea, SwingApplication}
+import scala.swing.event.ButtonClicked
+
+
+object Cygwin_Init
+{
+  /* command-line entry point */
+
+  def main(args: Array[String]) =
+  {
+    GUI.init_laf()
+    try {
+      require(Platform.is_windows)
+
+      val isabelle_home = System.getProperty("isabelle.home")
+      if (isabelle_home == null || isabelle_home == "")
+        error("Unknown Isabelle home directory")
+      if (!(new JFile(isabelle_home)).isDirectory)
+        error("Bad Isabelle home directory: " + quote(isabelle_home))
+
+      Swing_Thread.later { main_frame(isabelle_home) }
+    }
+    catch {
+      case exn: Throwable =>
+        GUI.error_dialog(null, "Isabelle init failure", GUI.scrollable_text(Exn.message(exn)))
+        sys.exit(2)
+    }
+  }
+
+
+  /* main window */
+
+  private def main_frame(isabelle_home: String) = new MainFrame
+  {
+    title = "Isabelle system initialization"
+    iconImage = new ImageIcon(isabelle_home + "\\lib\\logo\\isabelle.gif").getImage
+
+    val layout_panel = new BorderPanel
+    contents = layout_panel
+
+
+    /* text area */
+
+    def echo(msg: String) { text_area.append(msg + "\n") }
+
+    val text_area = new TextArea {
+      font = new Font("SansSerif", Font.PLAIN, GUI.resolution_scale(10) max 14)
+      editable = false
+      columns = 50
+      rows = 15
+    }
+
+    layout_panel.layout(new ScrollPane(text_area)) = BorderPanel.Position.Center
+
+
+    /* exit button */
+
+    var _return_code: Option[Int] = None
+    def maybe_exit(): Unit = _return_code.foreach(sys.exit(_))
+
+    def return_code(rc: Int): Unit =
+      Swing_Thread.later {
+        _return_code = Some(rc)
+        button.peer.getRootPane.setDefaultButton(button.peer)
+        layout_panel.repaint
+      }
+
+    override def closeOperation { maybe_exit() }
+
+    val button = new Button {
+      text = "Done"
+      reactions += { case ButtonClicked(_) => maybe_exit() }
+    }
+    val button_panel = new FlowPanel(FlowPanel.Alignment.Center)(button)
+
+    layout_panel.layout(button_panel) = BorderPanel.Position.South
+
+
+    /* show window */
+
+    pack()
+    val point = GraphicsEnvironment.getLocalGraphicsEnvironment().getCenterPoint()
+    location = new Point(point.x - size.width / 2, point.y - size.height / 2)
+    visible = true
+
+    default_thread_pool.submit(() =>
+      try {
+        init(isabelle_home, echo)
+        return_code(0)
+      }
+      catch {
+        case exn: Throwable =>
+          text_area.append("Error:\n" + Exn.message(exn) + "\n")
+          return_code(2)
+      }
+    )
+  }
+
+
+  /* init Cygwin file-system */
+
+  private def init(isabelle_home: String, echo: String => Unit)
+  {
+    val cygwin_root = isabelle_home + "\\contrib\\cygwin"
+
+    if (!(new JFile(cygwin_root)).isDirectory)
+      error("Bad Isabelle Cygwin directory: " + quote(cygwin_root))
+
+    def execute(args: String*): Int =
+    {
+      val cwd = new JFile(isabelle_home)
+      val env = Map("CYGWIN" -> "nodosfilewarning")
+      val proc = Isabelle_System.raw_execute(cwd, env, true, args: _*)
+      proc.getOutputStream.close
+
+      val stdout = new BufferedReader(new InputStreamReader(proc.getInputStream, UTF8.charset))
+      try {
+        var line = stdout.readLine
+        while (line != null) {
+          echo(line)
+          line = stdout.readLine
+        }
+      }
+      finally { stdout.close }
+
+      proc.waitFor
+    }
+
+    echo("Initializing Cygwin:")
+
+    echo("symlinks ...")
+    val symlinks =
+    {
+      val path = (new JFile(cygwin_root, "isabelle\\symlinks")).toPath
+      Files.readAllLines(path, UTF8.charset).toArray.toList.asInstanceOf[List[String]]
+    }
+    @tailrec def recover_symlinks(list: List[String]): Unit =
+    {
+      list match {
+        case Nil | List("") =>
+        case link :: content :: rest =>
+          val path = (new JFile(isabelle_home, link)).toPath
+
+          val writer = Files.newBufferedWriter(path, UTF8.charset)
+          try { writer.write("!<symlink>" + content + "\0") }
+          finally { writer.close }
+
+          Files.setAttribute(path, "dos:system", true)
+
+          recover_symlinks(rest)
+        case _ => error("Unbalanced symlinks list")
+      }
+    }
+    recover_symlinks(symlinks)
+
+    echo("rebaseall ...")
+    execute(cygwin_root + "\\bin\\dash.exe", "/isabelle/rebaseall")
+
+    echo("postinstall ...")
+    execute(cygwin_root + "\\bin\\bash.exe", "/isabelle/postinstall")
+
+    echo("init ...")
+    System.setProperty("cygwin.root", cygwin_root)
+    Isabelle_System.init()
+    echo("OK")
+  }
+}
+
diff -r c7cae5ce217d -r c16f35e5a5aa src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Tue Jul 16 15:59:55 2013 +0200
+++ b/src/Pure/System/isabelle_system.scala	Tue Jul 16 23:34:33 2013 +0200
@@ -230,8 +230,7 @@
 
   /* raw execute for bootstrapping */
 
-  private def raw_execute(cwd: JFile, env: Map[String, String], redirect: Boolean, args: String*)
-    : Process =
+  def raw_execute(cwd: JFile, env: Map[String, String], redirect: Boolean, args: String*): Process =
   {
     val cmdline = new java.util.LinkedList[String]
     for (s <- args) cmdline.add(s)
diff -r c7cae5ce217d -r c16f35e5a5aa src/Pure/Tools/main.scala
--- a/src/Pure/Tools/main.scala	Tue Jul 16 15:59:55 2013 +0200
+++ b/src/Pure/Tools/main.scala	Tue Jul 16 23:34:33 2013 +0200
@@ -13,19 +13,25 @@
 {
   def main(args: Array[String])
   {
-    val (out, rc) =
-      try {
-        GUI.init_laf()
-        Isabelle_System.init()
-        Isabelle_System.isabelle_tool("jedit", ("-s" :: args.toList): _*)
-      }
-      catch { case exn: Throwable => (Exn.message(exn), 2) }
+    args.toList match {
+      case "-i" :: rest =>
+        if (Platform.is_windows) Cygwin_Init.main(rest.toArray)
 
-    if (rc != 0)
-      GUI.dialog(null, "Isabelle", "Isabelle output",
-        GUI.scrollable_text(out + "\nReturn code: " + rc))
+      case _ =>
+        val (out, rc) =
+          try {
+            GUI.init_laf()
+            Isabelle_System.init()
+            Isabelle_System.isabelle_tool("jedit", ("-s" :: "--" :: args.toList): _*)
+          }
+          catch { case exn: Throwable => (Exn.message(exn), 2) }
 
-    sys.exit(rc)
+        if (rc != 0)
+          GUI.dialog(null, "Isabelle", "Isabelle output",
+            GUI.scrollable_text(out + "\nReturn code: " + rc))
+
+        sys.exit(rc)
+    }
   }
 }
 
diff -r c7cae5ce217d -r c16f35e5a5aa src/Pure/build-jars
--- a/src/Pure/build-jars	Tue Jul 16 15:59:55 2013 +0200
+++ b/src/Pure/build-jars	Tue Jul 16 23:34:33 2013 +0200
@@ -27,6 +27,7 @@
   General/symbol.scala
   General/time.scala
   General/timing.scala
+  General/xz_file.scala
   Isar/keyword.scala
   Isar/outer_syntax.scala
   Isar/parse.scala
@@ -42,7 +43,7 @@
   PIDE/yxml.scala
   System/color_value.scala
   System/command_line.scala
-  System/cygwin.scala
+  System/cygwin_init.scala
   System/event_bus.scala
   System/gui.scala
   System/gui_setup.scala
diff -r c7cae5ce217d -r c16f35e5a5aa src/Tools/jEdit/src/pretty_tooltip.scala
--- a/src/Tools/jEdit/src/pretty_tooltip.scala	Tue Jul 16 15:59:55 2013 +0200
+++ b/src/Tools/jEdit/src/pretty_tooltip.scala	Tue Jul 16 23:34:33 2013 +0200
@@ -85,6 +85,12 @@
       }
     }
 
+  def revoke(): Unit =
+    Swing_Thread.required {
+      pending = None
+      pending_delay.revoke()
+    }
+
   private lazy val reactivate_delay =
     Swing_Thread.delay_last(PIDE.options.seconds("jedit_tooltip_delay")) {
       active = true
@@ -92,9 +98,8 @@
 
   private def deactivate(): Unit =
     Swing_Thread.required {
-      pending = None
+      revoke()
       active = false
-      pending_delay.revoke()
       reactivate_delay.invoke()
     }
 
@@ -118,13 +123,15 @@
   }
 
   def dismissed_all(): Boolean =
+  {
+    deactivate()
     if (stack.isEmpty) false
     else {
-      deactivate()
       stack.foreach(_.hide_popup)
       stack = Nil
       true
     }
+  }
 
 
   /* auxiliary geometry measurement */