1.1 --- a/Admin/Windows/Cygwin/isabelle/init.bat Mon Jan 14 18:30:36 2013 +0100
1.2 +++ b/Admin/Windows/Cygwin/isabelle/init.bat Mon Jan 14 22:33:53 2013 +0100
1.3 @@ -1,11 +1,11 @@
1.4 @echo off
1.5
1.6 cd "%~dp0"
1.7 -cd "..\.."
1.8 +cd ".."
1.9
1.10 set CYGWIN=nodosfilewarning
1.11
1.12 echo Initializing Cygwin ...
1.13 -"contrib\cygwin\bin\dash" /isabelle/rebaseall contrib/polyml-5.5.0
1.14 -"contrib\cygwin\bin\bash" /isabelle/postinstall
1.15 +"bin\dash" /isabelle/rebaseall
1.16 +"bin\bash" /isabelle/postinstall
1.17
2.1 --- a/Admin/Windows/Cygwin/isabelle/rebaseall Mon Jan 14 18:30:36 2013 +0100
2.2 +++ b/Admin/Windows/Cygwin/isabelle/rebaseall Mon Jan 14 22:33:53 2013 +0100
2.3 @@ -4,7 +4,9 @@
2.4
2.5 FILE_LIST="$(mktemp)"
2.6
2.7 -for DIR in "$@"
2.8 +CONTRIB="$(cygpath -u "$(cygpath -w /)\..")"
2.9 +
2.10 +for DIR in "$CONTRIB/polyml-5.5.0"
2.11 do
2.12 find "$DIR" -name "*.dll" >> "$FILE_LIST"
2.13 done
3.1 --- a/Admin/components/bundled-windows Mon Jan 14 18:30:36 2013 +0100
3.2 +++ b/Admin/components/bundled-windows Mon Jan 14 22:33:53 2013 +0100
3.3 @@ -1,3 +1,3 @@
3.4 #additional components to be bundled for release
3.5 -cygwin-20130110
3.6 +cygwin-20130114
3.7
4.1 --- a/Admin/components/components.sha1 Mon Jan 14 18:30:36 2013 +0100
4.2 +++ b/Admin/components/components.sha1 Mon Jan 14 22:33:53 2013 +0100
4.3 @@ -1,5 +1,6 @@
4.4 2f6417b8e96a0e4e8354fe0f1a253c18fb55d9a7 cvc3-2.4.1.tar.gz
4.5 842d9526f37b928cf9e22f141884365129990d63 cygwin-20130110.tar.gz
4.6 +cb3b0706d208f104b800267697204f6d82f7b48a cygwin-20130114.tar.gz
4.7 0fe549949a025d65d52d6deca30554de8fca3b6e e-1.5.tar.gz
4.8 b98a98025d1f7e560ca6864a53296137dae736b4 e-1.6.tar.gz
4.9 6d34b18ca0aa1e10bab6413045d079188c0e2dfb exec_process-1.0.1.tar.gz
4.10 @@ -8,6 +9,7 @@
4.11 ae7ee5becb26512f18c609e83b34612918bae5f0 exec_process-1.0.tar.gz
4.12 683acd94761ef460cca1a628f650355370de5afb hol-light-bundle-0.5-126.tar.gz
4.13 8d83e433c1419e0c0cc5fd1762903d11b4a5752c jdk-6u31.tar.gz
4.14 +38d2d2a91c66714c18430e136e7e5191af3996e6 jdk-7u11.tar.gz
4.15 ec740ee9ffd43551ddf1e5b91641405116af6291 jdk-7u6.tar.gz
4.16 7d5b152ac70f720bb9e783fa45ecadcf95069584 jdk-7u9.tar.gz
4.17 44775a22f42a9d665696bfb49e53c79371c394b0 jedit_build-20111217.tar.gz
5.1 --- a/Admin/components/main Mon Jan 14 18:30:36 2013 +0100
5.2 +++ b/Admin/components/main Mon Jan 14 22:33:53 2013 +0100
5.3 @@ -2,7 +2,7 @@
5.4 cvc3-2.4.1
5.5 e-1.6
5.6 exec_process-1.0.3
5.7 -jdk-7u9
5.8 +jdk-7u11
5.9 jedit_build-20130104
5.10 jfreechart-1.0.14
5.11 kodkodi-1.5.2
6.1 --- a/Admin/java/build Mon Jan 14 18:30:36 2013 +0100
6.2 +++ b/Admin/java/build Mon Jan 14 22:33:53 2013 +0100
6.3 @@ -11,31 +11,13 @@
6.4
6.5 ## parameters
6.6
6.7 -ARCHIVE_LINUX32="jdk-7u9-linux-i586.tar.gz"
6.8 -ARCHIVE_LINUX64="jdk-7u9-linux-x64.tar.gz"
6.9 -ARCHIVE_DARWIN="jdk1.7.0_09.jdk.tar.gz"
6.10 -ARCHIVE_WINDOWS="jdk1.7.0_09.tar.gz"
6.11 +VERSION="7u11"
6.12 +FULL_VERSION="1.7.0_11"
6.13
6.14 -VERSION="7u9"
6.15 -
6.16 -
6.17 -## variations on version
6.18 -
6.19 -case "$VERSION" in
6.20 - *u?)
6.21 - MAJOR="$(echo "$VERSION" | cut -du -f1)"
6.22 - MINOR="0$(echo "$VERSION" | cut -du -f2)"
6.23 - ;;
6.24 - *u??)
6.25 - MAJOR="$(echo "$VERSION" | cut -du -f1)"
6.26 - MINOR="$(echo "$VERSION" | cut -du -f2)"
6.27 - ;;
6.28 - *)
6.29 - fail "Bad version identifier: \"$VERSION\""
6.30 - ;;
6.31 -esac
6.32 -
6.33 -FULL_VERSION="1.${MAJOR}.0_${MINOR}"
6.34 +ARCHIVE_LINUX32="jdk-${VERSION}-linux-i586.tar.gz"
6.35 +ARCHIVE_LINUX64="jdk-${VERSION}-linux-x64.tar.gz"
6.36 +ARCHIVE_DARWIN="jdk${FULL_VERSION}.jdk.tar.gz"
6.37 +ARCHIVE_WINDOWS="jdk${FULL_VERSION}.tar.gz"
6.38
6.39
6.40 ## main
6.41 @@ -106,6 +88,7 @@
6.42
6.43 find "$DIR/x86_64-darwin" -name "._*" -exec rm -f {} ";"
6.44
6.45 +echo "Sharing ..."
6.46 (
6.47 cd "$DIR/x86-linux/jdk${FULL_VERSION}"
6.48 for FILE in $(find . -type f)
6.49 @@ -126,4 +109,5 @@
6.50
6.51 # create archive
6.52
6.53 -tar -cz -f "${DIR}.tar.gz" "$DIR"
6.54 +echo "Archiving ..."
6.55 +tar -c -z -f "${DIR}.tar.gz" "$DIR" && echo "${DIR}.tar.gz"
7.1 --- a/Admin/lib/Tools/makedist_bundles Mon Jan 14 18:30:36 2013 +0100
7.2 +++ b/Admin/lib/Tools/makedist_bundles Mon Jan 14 22:33:53 2013 +0100
7.3 @@ -75,6 +75,7 @@
7.4 \#* | "") ;;
7.5 *)
7.6 COMPONENT="$REPLY"
7.7 + COMPONENT_DIR="$ISABELLE_TARGET/contrib/$COMPONENT"
7.8 case "$COMPONENT" in
7.9 jedit_build*) ;;
7.10 *)
7.11 @@ -88,7 +89,10 @@
7.12 fi
7.13
7.14 tar -C "$ISABELLE_TARGET/contrib" -x -z -f "$CONTRIB"
7.15 - echo "contrib/$COMPONENT" >> "$ISABELLE_TARGET/etc/components"
7.16 + if [ -f "$COMPONENT_DIR/etc/settings" -o -f "$COMPONENT_DIR/etc/components" ]
7.17 + then
7.18 + echo "contrib/$COMPONENT" >> "$ISABELLE_TARGET/etc/components"
7.19 + fi
7.20 ;;
7.21 esac
7.22 ;;
7.23 @@ -123,6 +127,15 @@
7.24 cp "$ISABELLE_HOME/Admin/Windows/Cygwin/Cygwin-Setup.bat" \
7.25 "$ISABELLE_HOME/Admin/Windows/Cygwin/Cygwin-Terminal.bat" "$ISABELLE_TARGET"
7.26
7.27 + for NAME in init.bat postinstall rebaseall
7.28 + do
7.29 + cp -a "$ISABELLE_HOME/Admin/Windows/Cygwin/isabelle/$NAME" \
7.30 + "$ISABELLE_TARGET/contrib/cygwin/isabelle/."
7.31 + done
7.32 +
7.33 + perl -pi -e "s,/bin/rebaseall.*,/isabelle/rebaseall,g;" \
7.34 + "$ISABELLE_TARGET/contrib/cygwin/etc/postinstall/autorebase.bat.done"
7.35 +
7.36 for NAME in ANNOUNCE README NEWS COPYRIGHT CONTRIBUTORS contrib/README
7.37 do
7.38 FILE="$ISABELLE_TARGET/$NAME"
8.1 --- a/Admin/lib/Tools/makedist_cygwin Mon Jan 14 18:30:36 2013 +0100
8.2 +++ b/Admin/lib/Tools/makedist_cygwin Mon Jan 14 22:33:53 2013 +0100
8.3 @@ -63,7 +63,7 @@
8.4
8.5 # patches
8.6
8.7 -for NAME in hosts protocols services networks
8.8 +for NAME in hosts protocols services networks passwd group
8.9 do
8.10 rm "$TARGET/etc/$NAME"
8.11 done
8.12 @@ -72,8 +72,6 @@
8.13
8.14 rm "$TARGET/Cygwin.bat"
8.15
8.16 -cp -a "$ISABELLE_HOME/Admin/Windows/Cygwin/isabelle/." "$TARGET/isabelle/."
8.17 -
8.18
8.19 # archive
8.20
9.1 --- a/src/Pure/Isar/proof.ML Mon Jan 14 18:30:36 2013 +0100
9.2 +++ b/src/Pure/Isar/proof.ML Mon Jan 14 22:33:53 2013 +0100
9.3 @@ -1030,8 +1030,8 @@
9.4 local
9.5
9.6 fun skipped_proof state =
9.7 - Context_Position.if_visible (context_of state) Output.report
9.8 - (Markup.markup Markup.bad "Skipped proof");
9.9 + Context_Position.report_text (context_of state) (Position.thread_data ())
9.10 + Markup.bad "Skipped proof";
9.11
9.12 in
9.13
10.1 --- a/src/Pure/System/isabelle_system.scala Mon Jan 14 18:30:36 2013 +0100
10.2 +++ b/src/Pure/System/isabelle_system.scala Mon Jan 14 22:33:53 2013 +0100
10.3 @@ -210,6 +210,15 @@
10.4 }
10.5
10.6
10.7 + /* mkdirs */
10.8 +
10.9 + def mkdirs(path: Path)
10.10 + {
10.11 + path.file.mkdirs
10.12 + if (!path.is_dir) error("Cannot create directory: " + quote(platform_path(path)))
10.13 + }
10.14 +
10.15 +
10.16
10.17 /** external processes **/
10.18
11.1 --- a/src/Pure/System/options.scala Mon Jan 14 18:30:36 2013 +0100
11.2 +++ b/src/Pure/System/options.scala Mon Jan 14 22:33:53 2013 +0100
11.3 @@ -348,7 +348,7 @@
11.4 changed.sortBy(_._1)
11.5 .map({ case (x, y, z) => x + " = " + Outer_Syntax.quote_string(y) + z + "\n" }).mkString
11.6
11.7 - Options.PREFS_DIR.file.mkdirs()
11.8 + Isabelle_System.mkdirs(Options.PREFS_DIR)
11.9 Options.PREFS.file renameTo Options.PREFS_BACKUP.file
11.10 File.write(Options.PREFS,
11.11 "(* generated by Isabelle " + Calendar.getInstance.getTime + " *)\n\n" + prefs)
12.1 --- a/src/Pure/Tools/build.scala Mon Jan 14 18:30:36 2013 +0100
12.2 +++ b/src/Pure/Tools/build.scala Mon Jan 14 22:33:53 2013 +0100
12.3 @@ -424,7 +424,7 @@
12.4 // global browser info dir
12.5 if (info.options.bool("browser_info") && !(browser_info + Path.explode("index.html")).is_file)
12.6 {
12.7 - browser_info.file.mkdirs()
12.8 + Isabelle_System.mkdirs(browser_info)
12.9 File.copy(Path.explode("~~/lib/logo/isabelle.gif"),
12.10 browser_info + Path.explode("isabelle.gif"))
12.11 File.write(browser_info + Path.explode("index.html"),
12.12 @@ -614,7 +614,7 @@
12.13 }
12.14
12.15 // prepare log dir
12.16 - (output_dir + LOG).file.mkdirs()
12.17 + Isabelle_System.mkdirs(output_dir + LOG)
12.18
12.19 // optional cleanup
12.20 if (clean_build) {
13.1 --- a/src/Tools/jEdit/src/text_overview.scala Mon Jan 14 18:30:36 2013 +0100
13.2 +++ b/src/Tools/jEdit/src/text_overview.scala Mon Jan 14 22:33:53 2013 +0100
13.3 @@ -91,9 +91,12 @@
13.4 case None => Text.Range(0)
13.5 case Some(visible_range) =>
13.6 val len = rendering.overview_limit max visible_range.length
13.7 - val start = ((visible_range.start + visible_range.stop - len) / 2) max 0
13.8 - val stop = (start + len) min char_count
13.9 - Text.Range(start, stop)
13.10 + val start = (visible_range.start + visible_range.stop - len) / 2
13.11 + val stop = start + len
13.12 +
13.13 + if (start < 0) Text.Range(0, len min char_count)
13.14 + else if (stop > char_count) Text.Range((char_count - len) max 0, char_count)
13.15 + else Text.Range(start, stop)
13.16 }
13.17
13.18 if (!(line_count == last_line_count && char_count == last_char_count &&