--- 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>
--- 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"
-
--- 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
--- 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
-
--- 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
+
--- 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)"
--- 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@!
Binary file Admin/Windows/launch4j/Isabelle.exe has changed
--- 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>
--- /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
--- 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
--- 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
--- 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"
--- 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 -- "$@"
--- 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}).
--- 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.
*}
--- 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.
--- 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
--- 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 .
--- 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]
--- 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,
--- 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,
--- 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,
--- 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 */
--- /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))
+ }
+}
+
--- 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);
--- 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)
- }
-}
-
--- /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")
+ }
+}
+
--- 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)
--- 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)
+ }
}
}
--- 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
--- 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 */