# HG changeset patch
# User wenzelm
# Date 1358199233 -3600
# Node ID a9c1b1428e873ebe5f207e7fa22366b32d2b6ec7
# Parent  2b21b4e2d7cb2af6dbbc9c9a1af3011057dac282# Parent  d55eb82ae77b31d9b262dd2d6d46d317f95dce20
merged

diff -r 2b21b4e2d7cb -r a9c1b1428e87 Admin/Windows/Cygwin/isabelle/init.bat
--- a/Admin/Windows/Cygwin/isabelle/init.bat	Mon Jan 14 18:30:36 2013 +0100
+++ b/Admin/Windows/Cygwin/isabelle/init.bat	Mon Jan 14 22:33:53 2013 +0100
@@ -1,11 +1,11 @@
 @echo off
 
 cd "%~dp0"
-cd "..\.."
+cd ".."
 
 set CYGWIN=nodosfilewarning
 
 echo Initializing Cygwin ...
-"contrib\cygwin\bin\dash" /isabelle/rebaseall contrib/polyml-5.5.0
-"contrib\cygwin\bin\bash" /isabelle/postinstall
+"bin\dash" /isabelle/rebaseall
+"bin\bash" /isabelle/postinstall
 
diff -r 2b21b4e2d7cb -r a9c1b1428e87 Admin/Windows/Cygwin/isabelle/rebaseall
--- a/Admin/Windows/Cygwin/isabelle/rebaseall	Mon Jan 14 18:30:36 2013 +0100
+++ b/Admin/Windows/Cygwin/isabelle/rebaseall	Mon Jan 14 22:33:53 2013 +0100
@@ -4,7 +4,9 @@
 
 FILE_LIST="$(mktemp)"
 
-for DIR in "$@"
+CONTRIB="$(cygpath -u "$(cygpath -w /)\..")"
+
+for DIR in "$CONTRIB/polyml-5.5.0"
 do
   find "$DIR" -name "*.dll" >> "$FILE_LIST"
 done
diff -r 2b21b4e2d7cb -r a9c1b1428e87 Admin/components/bundled-windows
--- a/Admin/components/bundled-windows	Mon Jan 14 18:30:36 2013 +0100
+++ b/Admin/components/bundled-windows	Mon Jan 14 22:33:53 2013 +0100
@@ -1,3 +1,3 @@
 #additional components to be bundled for release
-cygwin-20130110
+cygwin-20130114
 
diff -r 2b21b4e2d7cb -r a9c1b1428e87 Admin/components/components.sha1
--- a/Admin/components/components.sha1	Mon Jan 14 18:30:36 2013 +0100
+++ b/Admin/components/components.sha1	Mon Jan 14 22:33:53 2013 +0100
@@ -1,5 +1,6 @@
 2f6417b8e96a0e4e8354fe0f1a253c18fb55d9a7  cvc3-2.4.1.tar.gz
 842d9526f37b928cf9e22f141884365129990d63  cygwin-20130110.tar.gz
+cb3b0706d208f104b800267697204f6d82f7b48a  cygwin-20130114.tar.gz
 0fe549949a025d65d52d6deca30554de8fca3b6e  e-1.5.tar.gz
 b98a98025d1f7e560ca6864a53296137dae736b4  e-1.6.tar.gz
 6d34b18ca0aa1e10bab6413045d079188c0e2dfb  exec_process-1.0.1.tar.gz
@@ -8,6 +9,7 @@
 ae7ee5becb26512f18c609e83b34612918bae5f0  exec_process-1.0.tar.gz
 683acd94761ef460cca1a628f650355370de5afb  hol-light-bundle-0.5-126.tar.gz
 8d83e433c1419e0c0cc5fd1762903d11b4a5752c  jdk-6u31.tar.gz
+38d2d2a91c66714c18430e136e7e5191af3996e6  jdk-7u11.tar.gz
 ec740ee9ffd43551ddf1e5b91641405116af6291  jdk-7u6.tar.gz
 7d5b152ac70f720bb9e783fa45ecadcf95069584  jdk-7u9.tar.gz
 44775a22f42a9d665696bfb49e53c79371c394b0  jedit_build-20111217.tar.gz
diff -r 2b21b4e2d7cb -r a9c1b1428e87 Admin/components/main
--- a/Admin/components/main	Mon Jan 14 18:30:36 2013 +0100
+++ b/Admin/components/main	Mon Jan 14 22:33:53 2013 +0100
@@ -2,7 +2,7 @@
 cvc3-2.4.1
 e-1.6
 exec_process-1.0.3
-jdk-7u9
+jdk-7u11
 jedit_build-20130104
 jfreechart-1.0.14
 kodkodi-1.5.2
diff -r 2b21b4e2d7cb -r a9c1b1428e87 Admin/java/build
--- a/Admin/java/build	Mon Jan 14 18:30:36 2013 +0100
+++ b/Admin/java/build	Mon Jan 14 22:33:53 2013 +0100
@@ -11,31 +11,13 @@
 
 ## parameters
 
-ARCHIVE_LINUX32="jdk-7u9-linux-i586.tar.gz"
-ARCHIVE_LINUX64="jdk-7u9-linux-x64.tar.gz"
-ARCHIVE_DARWIN="jdk1.7.0_09.jdk.tar.gz"
-ARCHIVE_WINDOWS="jdk1.7.0_09.tar.gz"
-
-VERSION="7u9"
-
-
-## variations on version
+VERSION="7u11"
+FULL_VERSION="1.7.0_11"
 
-case "$VERSION" in
-  *u?)
-    MAJOR="$(echo "$VERSION" | cut -du -f1)"
-    MINOR="0$(echo "$VERSION" | cut -du -f2)"
-    ;;
-  *u??)
-    MAJOR="$(echo "$VERSION" | cut -du -f1)"
-    MINOR="$(echo "$VERSION" | cut -du -f2)"
-    ;;
-  *)
-    fail "Bad version identifier: \"$VERSION\""
-    ;;
-esac
-
-FULL_VERSION="1.${MAJOR}.0_${MINOR}"
+ARCHIVE_LINUX32="jdk-${VERSION}-linux-i586.tar.gz"
+ARCHIVE_LINUX64="jdk-${VERSION}-linux-x64.tar.gz"
+ARCHIVE_DARWIN="jdk${FULL_VERSION}.jdk.tar.gz"
+ARCHIVE_WINDOWS="jdk${FULL_VERSION}.tar.gz"
 
 
 ## main
@@ -106,6 +88,7 @@
 
 find "$DIR/x86_64-darwin" -name "._*" -exec rm -f {} ";"
 
+echo "Sharing ..."
 (
   cd "$DIR/x86-linux/jdk${FULL_VERSION}"
   for FILE in $(find . -type f)
@@ -126,4 +109,5 @@
 
 # create archive
 
-tar -cz -f "${DIR}.tar.gz" "$DIR"
+echo "Archiving ..."
+tar -c -z -f "${DIR}.tar.gz" "$DIR" && echo "${DIR}.tar.gz"
diff -r 2b21b4e2d7cb -r a9c1b1428e87 Admin/lib/Tools/makedist_bundles
--- a/Admin/lib/Tools/makedist_bundles	Mon Jan 14 18:30:36 2013 +0100
+++ b/Admin/lib/Tools/makedist_bundles	Mon Jan 14 22:33:53 2013 +0100
@@ -75,6 +75,7 @@
           \#* | "") ;;
           *)
             COMPONENT="$REPLY"
+            COMPONENT_DIR="$ISABELLE_TARGET/contrib/$COMPONENT"
             case "$COMPONENT" in
               jedit_build*) ;;
               *)
@@ -88,7 +89,10 @@
                 fi
 
                 tar -C "$ISABELLE_TARGET/contrib" -x -z -f "$CONTRIB"
-                echo "contrib/$COMPONENT" >> "$ISABELLE_TARGET/etc/components"
+                if [ -f "$COMPONENT_DIR/etc/settings" -o -f "$COMPONENT_DIR/etc/components" ]
+                then
+                  echo "contrib/$COMPONENT" >> "$ISABELLE_TARGET/etc/components"
+                fi
                 ;;
             esac
             ;;
@@ -123,6 +127,15 @@
     cp "$ISABELLE_HOME/Admin/Windows/Cygwin/Cygwin-Setup.bat" \
       "$ISABELLE_HOME/Admin/Windows/Cygwin/Cygwin-Terminal.bat" "$ISABELLE_TARGET"
 
+    for NAME in init.bat postinstall rebaseall
+    do
+      cp -a "$ISABELLE_HOME/Admin/Windows/Cygwin/isabelle/$NAME" \
+        "$ISABELLE_TARGET/contrib/cygwin/isabelle/."
+    done
+
+    perl -pi -e "s,/bin/rebaseall.*,/isabelle/rebaseall,g;" \
+      "$ISABELLE_TARGET/contrib/cygwin/etc/postinstall/autorebase.bat.done"
+
     for NAME in ANNOUNCE README NEWS COPYRIGHT CONTRIBUTORS contrib/README
     do
       FILE="$ISABELLE_TARGET/$NAME"
diff -r 2b21b4e2d7cb -r a9c1b1428e87 Admin/lib/Tools/makedist_cygwin
--- a/Admin/lib/Tools/makedist_cygwin	Mon Jan 14 18:30:36 2013 +0100
+++ b/Admin/lib/Tools/makedist_cygwin	Mon Jan 14 22:33:53 2013 +0100
@@ -63,7 +63,7 @@
 
 # patches
 
-for NAME in hosts protocols services networks
+for NAME in hosts protocols services networks passwd group
 do
   rm "$TARGET/etc/$NAME"
 done
@@ -72,8 +72,6 @@
 
 rm "$TARGET/Cygwin.bat"
 
-cp -a "$ISABELLE_HOME/Admin/Windows/Cygwin/isabelle/." "$TARGET/isabelle/."
-
 
 # archive
 
diff -r 2b21b4e2d7cb -r a9c1b1428e87 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Mon Jan 14 18:30:36 2013 +0100
+++ b/src/Pure/Isar/proof.ML	Mon Jan 14 22:33:53 2013 +0100
@@ -1030,8 +1030,8 @@
 local
 
 fun skipped_proof state =
-  Context_Position.if_visible (context_of state) Output.report
-    (Markup.markup Markup.bad "Skipped proof");
+  Context_Position.report_text (context_of state) (Position.thread_data ())
+    Markup.bad "Skipped proof";
 
 in
 
diff -r 2b21b4e2d7cb -r a9c1b1428e87 src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Mon Jan 14 18:30:36 2013 +0100
+++ b/src/Pure/System/isabelle_system.scala	Mon Jan 14 22:33:53 2013 +0100
@@ -210,6 +210,15 @@
   }
 
 
+  /* mkdirs */
+
+  def mkdirs(path: Path)
+  {
+    path.file.mkdirs
+    if (!path.is_dir) error("Cannot create directory: " + quote(platform_path(path)))
+  }
+
+
 
   /** external processes **/
 
diff -r 2b21b4e2d7cb -r a9c1b1428e87 src/Pure/System/options.scala
--- a/src/Pure/System/options.scala	Mon Jan 14 18:30:36 2013 +0100
+++ b/src/Pure/System/options.scala	Mon Jan 14 22:33:53 2013 +0100
@@ -348,7 +348,7 @@
       changed.sortBy(_._1)
         .map({ case (x, y, z) => x + " = " + Outer_Syntax.quote_string(y) + z + "\n" }).mkString
 
-    Options.PREFS_DIR.file.mkdirs()
+    Isabelle_System.mkdirs(Options.PREFS_DIR)
     Options.PREFS.file renameTo Options.PREFS_BACKUP.file
     File.write(Options.PREFS,
       "(* generated by Isabelle " + Calendar.getInstance.getTime + " *)\n\n" + prefs)
diff -r 2b21b4e2d7cb -r a9c1b1428e87 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Mon Jan 14 18:30:36 2013 +0100
+++ b/src/Pure/Tools/build.scala	Mon Jan 14 22:33:53 2013 +0100
@@ -424,7 +424,7 @@
     // global browser info dir
     if (info.options.bool("browser_info") && !(browser_info + Path.explode("index.html")).is_file)
     {
-      browser_info.file.mkdirs()
+      Isabelle_System.mkdirs(browser_info)
       File.copy(Path.explode("~~/lib/logo/isabelle.gif"),
         browser_info + Path.explode("isabelle.gif"))
       File.write(browser_info + Path.explode("index.html"),
@@ -614,7 +614,7 @@
       }
 
     // prepare log dir
-    (output_dir + LOG).file.mkdirs()
+    Isabelle_System.mkdirs(output_dir + LOG)
 
     // optional cleanup
     if (clean_build) {
diff -r 2b21b4e2d7cb -r a9c1b1428e87 src/Tools/jEdit/src/text_overview.scala
--- a/src/Tools/jEdit/src/text_overview.scala	Mon Jan 14 18:30:36 2013 +0100
+++ b/src/Tools/jEdit/src/text_overview.scala	Mon Jan 14 22:33:53 2013 +0100
@@ -91,9 +91,12 @@
               case None => Text.Range(0)
               case Some(visible_range) =>
                 val len = rendering.overview_limit max visible_range.length
-                val start = ((visible_range.start + visible_range.stop - len) / 2) max 0
-                val stop = (start + len) min char_count
-                Text.Range(start, stop)
+                val start = (visible_range.start + visible_range.stop - len) / 2
+                val stop = start + len
+
+                if (start < 0) Text.Range(0, len min char_count)
+                else if (stop > char_count) Text.Range((char_count - len) max 0, char_count)
+                else Text.Range(start, stop)
             }
 
           if (!(line_count == last_line_count && char_count == last_char_count &&