--- a/Admin/Cygwin/Cygwin-Setup.bat Thu Jul 05 17:31:13 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,4 +0,0 @@
-@echo off
-
-"%CD%\contrib\cygwin-1.7.9\setup" --site http://isabelle.in.tum.de/cygwin --no-verify --only-site --local-package-dir "%TEMP%" --root "%CD%\contrib\cygwin-1.7.9"
-
--- a/Admin/Cygwin/Cygwin-Terminal.bat Thu Jul 05 17:31:13 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,9 +0,0 @@
-@echo off
-
-set HOME=%HOMEDRIVE%%HOMEPATH%
-set PATH=%CD%\bin;%PATH%
-set CHERE_INVOKING=true
-
-echo This is the GNU Bash interpreter of Cygwin.
-echo Use command "isabelle" to invoke Isabelle tools.
-"%CD%\contrib\cygwin-1.7.9\bin\bash" --login -i
--- a/Admin/Cygwin/README Thu Jul 05 17:31:13 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,23 +0,0 @@
-Notes on Cygwin
-===============
-
-* http://www.cygwin.com/
-
-* http://www.cygwin.com/cygwin-ug-net/ntsec.html
-
-* http://chinese-watercolor.com/LRP/printsrv/cygwin-sshd.html
-
-* Cygwin crash of Poly/ML 5.4.0, 5.4.1 with threads (and sockets?)
-http://cygwin.com/ml/cygwin/2012-04/msg00415.html
-http://cygwin.com/ml/cygwin/2012-04/msg00417.html
-
-* Mirror with many old versions (not setup.ini)
- http://ftp.eq.uc.pt/software/pc/prog/cygwin
-
-* Time machine for older versions:
- http://www.fruitbat.org/Cygwin/index.html#cygwincirca
-
- e.g. ftp://www.fruitbat.org/pub/cygwin/circa/2012/02/04/034515/setup.ini
- for last 1.7.9 version
-
-* 7zip self-extracting installer: http://www.7zsfx.info
--- a/Admin/Cygwin/init.bat Thu Jul 05 17:31:13 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,8 +0,0 @@
-@echo off
-
-cd "%~dp0"
-cd "..\.."
-
-echo Initializing ...
-"contrib\cygwin-1.7.9\bin\ash" /bin/rebaseall
-"contrib\cygwin-1.7.9\bin\bash" -c "PATH=/bin; chmod -wx $(find heaps -type f); mkpasswd -l >/etc/passwd; mkgroup -l >/etc/group"
--- a/Admin/Cygwin/sfx.txt Thu Jul 05 17:31:13 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,9 +0,0 @@
-;!@Install@!UTF-8!
-GUIFlags="64"
-InstallPath="%UserDesktop%"
-BeginPrompt="Unpack Isabelle2012?"
-ExtractPathText="Target directory"
-ExtractTitle="Unpacking Isabelle2012 ..."
-Shortcut="Du,{%%T\Isabelle2012\Isabelle.exe},{},{},{},{},{%%T\Isabelle2012}"
-RunProgram="\"%%T\Isabelle2012\contrib\cygwin-1.7.9\init.bat\""
-;!@InstallEnd@!
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/Windows/Cygwin/Cygwin-Setup.bat Thu Jul 05 22:17:57 2012 +0200
@@ -0,0 +1,4 @@
+@echo off
+
+"%CD%\contrib\cygwin-1.7.9\setup" --site http://isabelle.in.tum.de/cygwin --no-verify --only-site --local-package-dir "%TEMP%" --root "%CD%\contrib\cygwin-1.7.9"
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/Windows/Cygwin/Cygwin-Terminal.bat Thu Jul 05 22:17:57 2012 +0200
@@ -0,0 +1,9 @@
+@echo off
+
+set HOME=%HOMEDRIVE%%HOMEPATH%
+set PATH=%CD%\bin;%PATH%
+set CHERE_INVOKING=true
+
+echo This is the GNU Bash interpreter of Cygwin.
+echo Use command "isabelle" to invoke Isabelle tools.
+"%CD%\contrib\cygwin-1.7.9\bin\bash" --login -i
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/Windows/Cygwin/README Thu Jul 05 22:17:57 2012 +0200
@@ -0,0 +1,23 @@
+Notes on Cygwin
+===============
+
+* http://www.cygwin.com/
+
+* http://www.cygwin.com/cygwin-ug-net/ntsec.html
+
+* http://chinese-watercolor.com/LRP/printsrv/cygwin-sshd.html
+
+* Cygwin crash of Poly/ML 5.4.0, 5.4.1 with threads (and sockets?)
+http://cygwin.com/ml/cygwin/2012-04/msg00415.html
+http://cygwin.com/ml/cygwin/2012-04/msg00417.html
+
+* Mirror with many old versions (not setup.ini)
+ http://ftp.eq.uc.pt/software/pc/prog/cygwin
+
+* Time machine for older versions:
+ http://www.fruitbat.org/Cygwin/index.html#cygwincirca
+
+ e.g. ftp://www.fruitbat.org/pub/cygwin/circa/2012/02/04/034515/setup.ini
+ for last 1.7.9 version
+
+* 7zip self-extracting installer: http://www.7zsfx.info
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/Windows/Cygwin/init.bat Thu Jul 05 22:17:57 2012 +0200
@@ -0,0 +1,8 @@
+@echo off
+
+cd "%~dp0"
+cd "..\.."
+
+echo Initializing ...
+"contrib\cygwin-1.7.9\bin\ash" /bin/rebaseall
+"contrib\cygwin-1.7.9\bin\bash" -c "PATH=/bin; chmod -wx $(find heaps -type f); mkpasswd -l >/etc/passwd; mkgroup -l >/etc/group"
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/Windows/Cygwin/sfx.txt Thu Jul 05 22:17:57 2012 +0200
@@ -0,0 +1,9 @@
+;!@Install@!UTF-8!
+GUIFlags="64"
+InstallPath="%UserDesktop%"
+BeginPrompt="Unpack Isabelle2012?"
+ExtractPathText="Target directory"
+ExtractTitle="Unpacking Isabelle2012 ..."
+Shortcut="Du,{%%T\Isabelle2012\Isabelle.exe},{},{},{},{},{%%T\Isabelle2012}"
+RunProgram="\"%%T\Isabelle2012\contrib\cygwin-1.7.9\init.bat\""
+;!@InstallEnd@!
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/Windows/exec_process/build Thu Jul 05 22:17:57 2012 +0200
@@ -0,0 +1,53 @@
+#!/usr/bin/env bash
+#
+# Multi-platform build script
+
+THIS="$(cd "$(dirname "$0")"; pwd)"
+PRG="$(basename "$0")"
+
+
+# diagnostics
+
+function usage()
+{
+ echo
+ echo "Usage: $PRG TARGET"
+ echo
+ exit 1
+}
+
+function fail()
+{
+ echo "$1" >&2
+ exit 2
+}
+
+
+# command line args
+
+[ "$#" -eq 0 ] && usage
+TARGET="$1"; shift
+
+[ "$#" -eq 0 ] || usage
+
+
+# main
+
+mkdir -p "$TARGET"
+
+case "$TARGET" in
+ x86_64-linux | x86_64-darwin)
+ cc -m64 exec_process.c -o "$TARGET/exec_process"
+ ;;
+ x86-linux | x86-darwin)
+ cc -m32 exec_process.c -o "$TARGET/exec_process"
+ ;;
+ x86-cygwin)
+ cc exec_process.c -o "$TARGET/exec_process.exe"
+ ;;
+ *)
+ cc exec_process.c -o "$TARGET/exec_process"
+ ;;
+esac
+
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/Windows/exec_process/etc/settings Thu Jul 05 22:17:57 2012 +0200
@@ -0,0 +1,3 @@
+# -*- shell-script -*- :mode=shellscript:
+
+EXEC_PROCESS="$COMPONENT/${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM}/exec_process"
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/Windows/exec_process/exec_process.c Thu Jul 05 22:17:57 2012 +0200
@@ -0,0 +1,57 @@
+/* Author: Makarius
+
+Bash process group invocation.
+*/
+
+#include <stdlib.h>
+#include <stdio.h>
+#include <sys/types.h>
+#include <unistd.h>
+
+
+static void fail(const char *msg)
+{
+ fprintf(stderr, "%s\n", msg);
+ exit(2);
+}
+
+
+int main(int argc, char *argv[])
+{
+ /* args */
+
+ if (argc != 3) {
+ fprintf(stderr, "Bad arguments\n");
+ exit(1);
+ }
+ char *pid_name = argv[1];
+ char *script = argv[2];
+
+
+ /* report pid */
+
+ FILE *pid_file;
+ pid_file = fopen(pid_name, "w");
+ if (pid_file == NULL) fail("Cannot open pid file");
+ fprintf(pid_file, "%d", getpid());
+ fclose(pid_file);
+
+
+ /* setsid */
+
+ if (getgid() == getpid()) fail("Cannot set session id");
+ setsid();
+
+
+ /* exec */
+
+ char *cmd_line[4];
+ cmd_line[0] = "/bin/bash";
+ cmd_line[1] = "-c";
+ cmd_line[2] = script;
+ cmd_line[3] = NULL;
+
+ execv("/bin/bash", cmd_line);
+ fail("Cannot exec process");
+}
+
Binary file Admin/Windows/launch4j/Isabelle.exe has changed
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/Windows/launch4j/README Thu Jul 05 22:17:57 2012 +0200
@@ -0,0 +1,4 @@
+Java application wrapper for Windows
+====================================
+
+* http://launch4j.sourceforge.net
Binary file Admin/Windows/launch4j/isabelle.bmp has changed
Binary file Admin/Windows/launch4j/isabelle.ico has changed
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/Windows/launch4j/isabelle.xml Thu Jul 05 22:17:57 2012 +0200
@@ -0,0 +1,35 @@
+<launch4jConfig>
+ <dontWrapJar>true</dontWrapJar>
+ <headerType>gui</headerType>
+ <jar></jar>
+ <outfile>Isabelle.exe</outfile>
+ <errTitle></errTitle>
+ <cmdLine></cmdLine>
+ <chdir></chdir>
+ <priority>normal</priority>
+ <downloadUrl></downloadUrl>
+ <supportUrl></supportUrl>
+ <customProcName>false</customProcName>
+ <stayAlive>true</stayAlive>
+ <manifest></manifest>
+ <icon>isabelle.ico</icon>
+ <classPath>
+ <mainClass>isabelle.Main</mainClass>
+ <cp>%EXEDIR%\lib\classes\ext\Pure.jar</cp>
+ <cp>%EXEDIR%\lib\classes\ext\scala-library.jar</cp>
+ <cp>%EXEDIR%\lib\classes\ext\scala-swing.jar</cp>
+ </classPath>
+ <jre>
+ <path>%EXEDIR%\contrib\jdk-6u31_x86-cygwin\jdk1.6.0_31</path>
+ <minVersion></minVersion>
+ <maxVersion></maxVersion>
+ <jdkPreference>jdkOnly</jdkPreference>
+ <opt>-Disabelle.home="%EXEDIR%" -Dcygwin.root="%EXEDIR%\\contrib\\cygwin-1.7.9"</opt>
+ </jre>
+ <splash>
+ <file>isabelle.bmp</file>
+ <waitForWindow>false</waitForWindow>
+ <timeout>10</timeout>
+ <timeoutErr>false</timeoutErr>
+ </splash>
+</launch4jConfig>
\ No newline at end of file
--- a/Admin/exec_process/build Thu Jul 05 17:31:13 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,53 +0,0 @@
-#!/usr/bin/env bash
-#
-# Multi-platform build script
-
-THIS="$(cd "$(dirname "$0")"; pwd)"
-PRG="$(basename "$0")"
-
-
-# diagnostics
-
-function usage()
-{
- echo
- echo "Usage: $PRG TARGET"
- echo
- exit 1
-}
-
-function fail()
-{
- echo "$1" >&2
- exit 2
-}
-
-
-# command line args
-
-[ "$#" -eq 0 ] && usage
-TARGET="$1"; shift
-
-[ "$#" -eq 0 ] || usage
-
-
-# main
-
-mkdir -p "$TARGET"
-
-case "$TARGET" in
- x86_64-linux | x86_64-darwin)
- cc -m64 exec_process.c -o "$TARGET/exec_process"
- ;;
- x86-linux | x86-darwin)
- cc -m32 exec_process.c -o "$TARGET/exec_process"
- ;;
- x86-cygwin)
- cc exec_process.c -o "$TARGET/exec_process.exe"
- ;;
- *)
- cc exec_process.c -o "$TARGET/exec_process"
- ;;
-esac
-
-
--- a/Admin/exec_process/etc/settings Thu Jul 05 17:31:13 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,3 +0,0 @@
-# -*- shell-script -*- :mode=shellscript:
-
-EXEC_PROCESS="$COMPONENT/${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM}/exec_process"
--- a/Admin/exec_process/exec_process.c Thu Jul 05 17:31:13 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,57 +0,0 @@
-/* Author: Makarius
-
-Bash process group invocation.
-*/
-
-#include <stdlib.h>
-#include <stdio.h>
-#include <sys/types.h>
-#include <unistd.h>
-
-
-static void fail(const char *msg)
-{
- fprintf(stderr, "%s\n", msg);
- exit(2);
-}
-
-
-int main(int argc, char *argv[])
-{
- /* args */
-
- if (argc != 3) {
- fprintf(stderr, "Bad arguments\n");
- exit(1);
- }
- char *pid_name = argv[1];
- char *script = argv[2];
-
-
- /* report pid */
-
- FILE *pid_file;
- pid_file = fopen(pid_name, "w");
- if (pid_file == NULL) fail("Cannot open pid file");
- fprintf(pid_file, "%d", getpid());
- fclose(pid_file);
-
-
- /* setsid */
-
- if (getgid() == getpid()) fail("Cannot set session id");
- setsid();
-
-
- /* exec */
-
- char *cmd_line[4];
- cmd_line[0] = "/bin/bash";
- cmd_line[1] = "-c";
- cmd_line[2] = script;
- cmd_line[3] = NULL;
-
- execv("/bin/bash", cmd_line);
- fail("Cannot exec process");
-}
-
Binary file Admin/launch4j/Isabelle.exe has changed
--- a/Admin/launch4j/README Thu Jul 05 17:31:13 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,4 +0,0 @@
-Java application wrapper for Windows
-====================================
-
-* http://launch4j.sourceforge.net
Binary file Admin/launch4j/isabelle.bmp has changed
Binary file Admin/launch4j/isabelle.ico has changed
--- a/Admin/launch4j/isabelle.xml Thu Jul 05 17:31:13 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,35 +0,0 @@
-<launch4jConfig>
- <dontWrapJar>true</dontWrapJar>
- <headerType>gui</headerType>
- <jar></jar>
- <outfile>Isabelle.exe</outfile>
- <errTitle></errTitle>
- <cmdLine></cmdLine>
- <chdir></chdir>
- <priority>normal</priority>
- <downloadUrl></downloadUrl>
- <supportUrl></supportUrl>
- <customProcName>false</customProcName>
- <stayAlive>true</stayAlive>
- <manifest></manifest>
- <icon>isabelle.ico</icon>
- <classPath>
- <mainClass>isabelle.Main</mainClass>
- <cp>%EXEDIR%\lib\classes\ext\Pure.jar</cp>
- <cp>%EXEDIR%\lib\classes\ext\scala-library.jar</cp>
- <cp>%EXEDIR%\lib\classes\ext\scala-swing.jar</cp>
- </classPath>
- <jre>
- <path>%EXEDIR%\contrib\jdk-6u31_x86-cygwin\jdk1.6.0_31</path>
- <minVersion></minVersion>
- <maxVersion></maxVersion>
- <jdkPreference>jdkOnly</jdkPreference>
- <opt>-Disabelle.home="%EXEDIR%" -Dcygwin.root="%EXEDIR%\\contrib\\cygwin-1.7.9"</opt>
- </jre>
- <splash>
- <file>isabelle.bmp</file>
- <waitForWindow>false</waitForWindow>
- <timeout>10</timeout>
- <timeoutErr>false</timeoutErr>
- </splash>
-</launch4jConfig>
\ No newline at end of file
--- a/Admin/psbooklet Thu Jul 05 17:31:13 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,6 +0,0 @@
-#!/usr/bin/env bash
-#
-# psbooklet - rearrange pages of ps file to be printed as booklet (duplex)
-
-psbook "$@" | \
- pstops '4:0L@.7(21cm,0cm)+1L@.7(21cm,14.85cm),3R@.7(0cm,14.85cm)+2R@.7(0cm,29.7cm)'
--- a/src/HOL/HOL.thy Thu Jul 05 17:31:13 2012 +0200
+++ b/src/HOL/HOL.thy Thu Jul 05 22:17:57 2012 +0200
@@ -404,14 +404,6 @@
lemma eq_neq_eq_imp_neq: "[| x = a ; a ~= b; b = y |] ==> x ~= y"
by (erule subst, erule ssubst, assumption)
-(*still used in HOLCF*)
-lemma rev_contrapos:
- assumes pq: "P ==> Q"
- and nq: "~Q"
- shows "~P"
-apply (rule nq [THEN contrapos_nn])
-apply (erule pq)
-done
subsubsection {*Existential quantifier*}
--- a/src/HOL/HOLCF/IOA/meta_theory/CompoTraces.thy Thu Jul 05 17:31:13 2012 +0200
+++ b/src/HOL/HOLCF/IOA/meta_theory/CompoTraces.thy Thu Jul 05 22:17:57 2012 +0200
@@ -64,7 +64,10 @@
axiomatization where
finiteR_mksch:
- "Finite (mksch A B$tr$x$y) --> Finite tr"
+ "Finite (mksch A B$tr$x$y) \<Longrightarrow> Finite tr"
+
+lemma finiteR_mksch': "\<not> Finite tr \<Longrightarrow> \<not> Finite (mksch A B$tr$x$y)"
+ by (blast intro: finiteR_mksch)
declaration {* fn _ => Simplifier.map_ss (Simplifier.set_mksym (K (K NONE))) *}
@@ -507,7 +510,7 @@
apply (subgoal_tac "schA=UU")
apply (simp (no_asm_simp))
(* first side: mksch = UU *)
-apply (auto intro!: ForallQFilterPUU finiteR_mksch [THEN mp, COMP rev_contrapos] ForallBnAmksch)[1]
+apply (auto intro!: ForallQFilterPUU finiteR_mksch' ForallBnAmksch)[1]
(* schA = UU *)
apply (erule_tac A = "A" in LastActExtimplUU)
apply (simp (no_asm_simp))
@@ -726,7 +729,7 @@
apply (subgoal_tac "schB=UU")
apply (simp (no_asm_simp))
(* first side: mksch = UU *)
-apply (force intro!: ForallQFilterPUU finiteR_mksch [THEN mp, COMP rev_contrapos] ForallAnBmksch)
+apply (force intro!: ForallQFilterPUU finiteR_mksch' ForallAnBmksch)
(* schA = UU *)
apply (erule_tac A = "B" in LastActExtimplUU)
apply (simp (no_asm_simp))
--- a/src/HOL/HOLCF/IOA/meta_theory/Sequence.thy Thu Jul 05 17:31:13 2012 +0200
+++ b/src/HOL/HOLCF/IOA/meta_theory/Sequence.thy Thu Jul 05 22:17:57 2012 +0200
@@ -651,7 +651,7 @@
(* inverse of ForallnPFilterPnil *)
-lemma FilternPnilForallP1: "!! ys . Filter P$ys = nil -->
+lemma FilternPnilForallP [rule_format]: "Filter P$ys = nil -->
(Forall (%x. ~P x) ys & Finite ys)"
apply (rule_tac x="ys" in Seq_induct)
(* adm *)
@@ -663,27 +663,32 @@
apply simp
done
-lemmas FilternPnilForallP = FilternPnilForallP1 [THEN mp]
-(* inverse of ForallnPFilterPUU. proved apply 2 lemmas because of adm problems *)
-
-lemma FilterUU_nFinite_lemma1: "Finite ys ==> Filter P$ys ~= UU"
-apply (erule Seq_Finite_ind, simp_all)
-done
-
-lemma FilterUU_nFinite_lemma2: "~ Forall (%x. ~P x) ys --> Filter P$ys ~= UU"
-apply (rule_tac x="ys" in Seq_induct)
-apply (simp add: Forall_def sforall_def)
-apply simp_all
-done
+(* inverse of ForallnPFilterPUU *)
lemma FilternPUUForallP:
- "Filter P$ys = UU ==> (Forall (%x. ~P x) ys & ~Finite ys)"
-apply (rule conjI)
-apply (cut_tac FilterUU_nFinite_lemma2 [THEN mp, COMP rev_contrapos])
-apply auto
-apply (blast dest!: FilterUU_nFinite_lemma1)
-done
+ assumes "Filter P$ys = UU"
+ shows "Forall (%x. ~P x) ys & ~Finite ys"
+proof
+ show "Forall (%x. ~P x) ys"
+ proof (rule classical)
+ assume "\<not> ?thesis"
+ then have "Filter P$ys ~= UU"
+ apply (rule rev_mp)
+ apply (induct ys rule: Seq_induct)
+ apply (simp add: Forall_def sforall_def)
+ apply simp_all
+ done
+ with assms show ?thesis by contradiction
+ qed
+ show "~ Finite ys"
+ proof
+ assume "Finite ys"
+ then have "Filter P$ys ~= UU"
+ by (rule Seq_Finite_ind) simp_all
+ with assms show False by contradiction
+ qed
+qed
lemma ForallQFilterPnil:
--- a/src/HOL/Word/Word.thy Thu Jul 05 17:31:13 2012 +0200
+++ b/src/HOL/Word/Word.thy Thu Jul 05 22:17:57 2012 +0200
@@ -2344,7 +2344,10 @@
fixes x' :: "'a::len0 word"
shows "(w' = (x' AND y')) \<Longrightarrow> (x' = (x' OR w'))" by auto
-lemmas word_ao_equiv = leao [COMP leoa [COMP iffI]]
+lemma word_ao_equiv:
+ fixes w w' :: "'a::len0 word"
+ shows "(w = w OR w') = (w' = w AND w')"
+ by (auto intro: leoa leao)
lemma le_word_or2: "x <= x OR (y::'a::len0 word)"
unfolding word_le_def uint_or
--- a/src/Pure/Isar/outer_syntax.ML Thu Jul 05 17:31:13 2012 +0200
+++ b/src/Pure/Isar/outer_syntax.ML Thu Jul 05 22:17:57 2012 +0200
@@ -69,7 +69,9 @@
(case cmd name of
SOME (Command {int_only, parse, ...}) =>
Parse.!!! (Scan.prompt (name ^ "# ") (Parse.tags |-- parse >> pair int_only))
- | NONE => raise Fail ("No parser for outer syntax command " ^ quote name));
+ | NONE =>
+ Scan.succeed (false, Toplevel.imperative (fn () =>
+ error ("Bad parser for outer syntax command " ^ quote name))));
in
--- a/src/Pure/System/gui_setup.scala Thu Jul 05 17:31:13 2012 +0200
+++ b/src/Pure/System/gui_setup.scala Thu Jul 05 22:17:57 2012 +0200
@@ -62,7 +62,7 @@
// reactions
listenTo(ok)
reactions += {
- case ButtonClicked(`ok`) => System.exit(0)
+ case ButtonClicked(`ok`) => sys.exit(0)
}
}
}
--- a/src/Pure/System/isabelle_system.scala Thu Jul 05 17:31:13 2012 +0200
+++ b/src/Pure/System/isabelle_system.scala Thu Jul 05 22:17:57 2012 +0200
@@ -50,8 +50,7 @@
val standard_system = new Standard_System
val settings =
{
- val env0 = Map(System.getenv.toList: _*) +
- ("ISABELLE_JDK_HOME" -> standard_system.this_jdk_home())
+ val env0 = sys.env + ("ISABELLE_JDK_HOME" -> standard_system.this_jdk_home())
val user_home = System.getProperty("user.home")
val env =
--- a/src/Pure/System/main.scala Thu Jul 05 17:31:13 2012 +0200
+++ b/src/Pure/System/main.scala Thu Jul 05 22:17:57 2012 +0200
@@ -25,7 +25,7 @@
Library.dialog(null, "Isabelle", "Isabelle output",
Library.scrollable_text(out + "\nReturn code: " + rc))
- System.exit(rc)
+ sys.exit(rc)
}
}
