# HG changeset patch
# User wenzelm
# Date 1357939008 -3600
# Node ID db0012672241d181a937f071cb88cc8d33b08439
# Parent  fc4025435b517f2ae5ffaad7a9fa6473bc029789# Parent  c95af99e003bf222944cc0ee9e7284f66ded3701
merged

diff -r fc4025435b51 -r db0012672241 Admin/Windows/Cygwin/Cygwin-Setup-Default.bat
--- a/Admin/Windows/Cygwin/Cygwin-Setup-Default.bat	Fri Jan 11 16:30:56 2013 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,4 +0,0 @@
-@echo off
-
-setup.exe --local-package-dir "%TEMP%" --root "%CD%\cygwin-root" -P libgmp3,perl,python,texlive-collection-basic,texlive-collection-fontsrecommended,texlive-collection-genericrecommended,texlive-collection-latex,texlive-collection-latexrecommended
-
diff -r fc4025435b51 -r db0012672241 Admin/Windows/Cygwin/Cygwin-Setup.bat
--- a/Admin/Windows/Cygwin/Cygwin-Setup.bat	Fri Jan 11 16:30:56 2013 +0100
+++ b/Admin/Windows/Cygwin/Cygwin-Setup.bat	Fri Jan 11 22:16:48 2013 +0100
@@ -1,4 +1,4 @@
 @echo off
 
-"%CD%\cygwin\isabelle\cygwin" --site http://isabelle.in.tum.de/cygwin_2013 --no-verify --only-site --local-package-dir "%TEMP%" --root "%CD%\cygwin"
+"%CD%\contrib\cygwin\isabelle\cygwin" --site http://isabelle.in.tum.de/cygwin_2013 --no-verify --only-site --local-package-dir "%TEMP%" --root "%CD%\contrib\cygwin"
 
diff -r fc4025435b51 -r db0012672241 Admin/Windows/Cygwin/Cygwin-Terminal.bat
--- a/Admin/Windows/Cygwin/Cygwin-Terminal.bat	Fri Jan 11 16:30:56 2013 +0100
+++ b/Admin/Windows/Cygwin/Cygwin-Terminal.bat	Fri Jan 11 22:16:48 2013 +0100
@@ -6,4 +6,4 @@
 
 echo This is the GNU Bash interpreter of Cygwin.
 echo Use command "isabelle" to invoke Isabelle tools.
-"%CD%\cygwin\bin\bash" --login -i
+"%CD%\contrib\cygwin\bin\bash" --login -i
diff -r fc4025435b51 -r db0012672241 Admin/Windows/Cygwin/isabelle/init.bat
--- a/Admin/Windows/Cygwin/isabelle/init.bat	Fri Jan 11 16:30:56 2013 +0100
+++ b/Admin/Windows/Cygwin/isabelle/init.bat	Fri Jan 11 22:16:48 2013 +0100
@@ -6,6 +6,6 @@
 set CYGWIN=nodosfilewarning
 
 echo Initializing Cygwin ...
-"cygwin\bin\dash" /isabelle/rebaseall contrib/polyml-5.5.0
-"cygwin\bin\bash" /isabelle/postinstall
+"contrib\cygwin\bin\dash" /isabelle/rebaseall contrib/polyml-5.5.0
+"contrib\cygwin\bin\bash" /isabelle/postinstall
 
diff -r fc4025435b51 -r db0012672241 Admin/Windows/Cygwin/sfx.txt
--- a/Admin/Windows/Cygwin/sfx.txt	Fri Jan 11 16:30:56 2013 +0100
+++ b/Admin/Windows/Cygwin/sfx.txt	Fri Jan 11 22:16:48 2013 +0100
@@ -4,6 +4,6 @@
 BeginPrompt="Unpack Isabelle2013?"
 ExtractPathText="Target directory"
 ExtractTitle="Unpacking Isabelle2013 ..."
-Shortcut="Du,{%%T\Isabelle2013\Isabelle2013.exe},{},{},{},{},{%%T\Isabelle2013}"
-RunProgram="\"%%T\Isabelle2013\cygwin\init.bat\""
+Shortcut="Du,{%%T\Isabelle2013\Isabelle2013.exe},{},{},{},{Isabelle2013},{%%T\Isabelle2013}"
+RunProgram="\"%%T\Isabelle2013\contrib\cygwin\isabelle\init.bat\""
 ;!@InstallEnd@!
diff -r fc4025435b51 -r db0012672241 Admin/Windows/launch4j/Isabelle.exe
Binary file Admin/Windows/launch4j/Isabelle.exe has changed
diff -r fc4025435b51 -r db0012672241 Admin/Windows/launch4j/isabelle.xml
--- a/Admin/Windows/launch4j/isabelle.xml	Fri Jan 11 16:30:56 2013 +0100
+++ b/Admin/Windows/launch4j/isabelle.xml	Fri Jan 11 22:16:48 2013 +0100
@@ -24,7 +24,7 @@
     <minVersion></minVersion>
     <maxVersion></maxVersion>
     <jdkPreference>jdkOnly</jdkPreference>
-    <opt>-Disabelle.home=&quot;%EXEDIR%&quot; -Dcygwin.root=&quot;%EXEDIR%\\cygwin&quot;</opt>
+    <opt>-Disabelle.home=&quot;%EXEDIR%&quot; -Dcygwin.root=&quot;%EXEDIR%\\contrib\\cygwin&quot;</opt>
   </jre>
   <splash>
     <file>isabelle.bmp</file>
diff -r fc4025435b51 -r db0012672241 Admin/lib/Tools/makedist_bundles
--- a/Admin/lib/Tools/makedist_bundles	Fri Jan 11 16:30:56 2013 +0100
+++ b/Admin/lib/Tools/makedist_bundles	Fri Jan 11 22:16:48 2013 +0100
@@ -117,8 +117,6 @@
     perl -pi -e "s,lookAndFeel=.*,lookAndFeel=com.sun.java.swing.plaf.windows.WindowsLookAndFeel,g;" \
       "$TMP/$ISABELLE_NAME/src/Tools/jEdit/dist/properties/jEdit.props"
 
-    mv "$ISABELLE_TARGET/contrib/cygwin" "$ISABELLE_TARGET"
-
     cp "$ISABELLE_HOME/Admin/Windows/launch4j/Isabelle.exe" "$ISABELLE_TARGET/Isabelle2013.exe"
     cp "$ISABELLE_HOME/Admin/Windows/Cygwin/Cygwin-Setup.bat" \
       "$ISABELLE_HOME/Admin/Windows/Cygwin/Cygwin-Terminal.bat" "$ISABELLE_TARGET"
diff -r fc4025435b51 -r db0012672241 Admin/lib/Tools/makedist_cygwin
--- a/Admin/lib/Tools/makedist_cygwin	Fri Jan 11 16:30:56 2013 +0100
+++ b/Admin/lib/Tools/makedist_cygwin	Fri Jan 11 22:16:48 2013 +0100
@@ -2,6 +2,11 @@
 #
 # DESCRIPTION: produce pre-canned Cygwin distribution for Isabelle
 
+## global parameters
+
+CYGWIN_MIRROR="http://isabelle.in.tum.de/cygwin_2013"
+
+
 ## diagnostics
 
 PRG=$(basename "$0")
@@ -38,7 +43,7 @@
 [ ! -e "$TARGET" ] || fail "Target already exists: \"$TARGET\""
 mkdir -p "$TARGET/isabelle" || fail "Failed to create target directory: \"$TARGET\""
 
-perl -MLWP::Simple -e "getprint 'http://cygwin.com/setup.exe';" > "$TARGET/isabelle/cygwin.exe"
+perl -MLWP::Simple -e "getprint '$CYGWIN_MIRROR/setup.exe';" > "$TARGET/isabelle/cygwin.exe"
 chmod +x "$TARGET/isabelle/cygwin.exe"
 
 "$TARGET/isabelle/cygwin.exe" -h </dev/null >/dev/null || exit 2
@@ -47,7 +52,8 @@
 # install
 
 "$TARGET/isabelle/cygwin.exe" \
-  --local-package-dir "$(cygpath -w "$TMP/cygwin")" \
+  --site "$CYGWIN_MIRROR" --no-verify \
+  --local-package-dir 'C:\tmp' \
   --root "$(cygpath -w "$TARGET")" \
   --packages libgmp3,perl,python,rlwrap \
   --no-shortcuts --no-startmenu --no-desktop --quiet-mode
@@ -71,4 +77,5 @@
 
 # archive
 
-tar cvzf "${TARGET}.tar.gz" "$TARGET"
+DATE=$(date +%Y%m%d)
+tar -C "$TARGET/.." -cz -f "cygwin-${DATE}.tar.gz" cygwin
diff -r fc4025435b51 -r db0012672241 NEWS
--- a/NEWS	Fri Jan 11 16:30:56 2013 +0100
+++ b/NEWS	Fri Jan 11 22:16:48 2013 +0100
@@ -101,7 +101,8 @@
 
 * Actions isabelle.increase-font-size and isabelle.decrease-font-size
 adjust the main text area font size, and its derivatives for output,
-tooltips etc.  Cf. keyboard shortcuts C-PLUS and C-MINUS.
+tooltips etc.  Cf. keyboard shortcuts C-PLUS and C-MINUS, which often
+need to be adapted to local keyboard layouts.
 
 * More reactive completion popup by default: use \t (TAB) instead of
 \n (NEWLINE) to minimize intrusion into regular flow of editing.  See
diff -r fc4025435b51 -r db0012672241 src/HOL/ROOT
--- a/src/HOL/ROOT	Fri Jan 11 16:30:56 2013 +0100
+++ b/src/HOL/ROOT	Fri Jan 11 22:16:48 2013 +0100
@@ -8,24 +8,6 @@
     "document/root.bib"
     "document/root.tex"
 
-session "HOL-Base" = Pure +
-  description {* Raw HOL base, with minimal tools *}
-  options [document = false]
-  theories HOL
-
-session "HOL-Plain" = Pure +
-  description {* HOL side-entry after bootstrap of many tools and packages *}
-  options [document = false]
-  theories Plain
-
-session "HOL-Main" = Pure +
-  description {* HOL side-entry for Main only, without Complex_Main *}
-  options [document = false]
-  theories Main
-  files
-    "Tools/Quickcheck/Narrowing_Engine.hs"
-    "Tools/Quickcheck/PNF_Narrowing_Engine.hs"
-
 session "HOL-Proofs" = Pure +
   description {* HOL-Main with explicit proof terms *}
   options [document = false, proofs = 2, parallel_proofs = 0]