# HG changeset patch # User wenzelm # Date 1341519477 -7200 # Node ID 3155cee13c49e56ef003451e0102b8e7331acb15 # Parent 4b93fc861cfa7051cf4bc7e454f7a143bcbd76b1# Parent 4cae75fa29f2e0d39340f5971871bd465c21cd58 merged diff -r 4b93fc861cfa -r 3155cee13c49 Admin/Cygwin/Cygwin-Setup.bat --- 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" - diff -r 4b93fc861cfa -r 3155cee13c49 Admin/Cygwin/Cygwin-Terminal.bat --- 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 diff -r 4b93fc861cfa -r 3155cee13c49 Admin/Cygwin/README --- 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 diff -r 4b93fc861cfa -r 3155cee13c49 Admin/Cygwin/init.bat --- 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" diff -r 4b93fc861cfa -r 3155cee13c49 Admin/Cygwin/sfx.txt --- 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@! diff -r 4b93fc861cfa -r 3155cee13c49 Admin/Windows/Cygwin/Cygwin-Setup.bat --- /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" + diff -r 4b93fc861cfa -r 3155cee13c49 Admin/Windows/Cygwin/Cygwin-Terminal.bat --- /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 diff -r 4b93fc861cfa -r 3155cee13c49 Admin/Windows/Cygwin/README --- /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 diff -r 4b93fc861cfa -r 3155cee13c49 Admin/Windows/Cygwin/init.bat --- /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" diff -r 4b93fc861cfa -r 3155cee13c49 Admin/Windows/Cygwin/sfx.txt --- /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@! diff -r 4b93fc861cfa -r 3155cee13c49 Admin/Windows/exec_process/build --- /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 + + diff -r 4b93fc861cfa -r 3155cee13c49 Admin/Windows/exec_process/etc/settings --- /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" diff -r 4b93fc861cfa -r 3155cee13c49 Admin/Windows/exec_process/exec_process.c --- /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 +#include +#include +#include + + +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"); +} + diff -r 4b93fc861cfa -r 3155cee13c49 Admin/Windows/launch4j/Isabelle.exe Binary file Admin/Windows/launch4j/Isabelle.exe has changed diff -r 4b93fc861cfa -r 3155cee13c49 Admin/Windows/launch4j/README --- /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 diff -r 4b93fc861cfa -r 3155cee13c49 Admin/Windows/launch4j/isabelle.bmp Binary file Admin/Windows/launch4j/isabelle.bmp has changed diff -r 4b93fc861cfa -r 3155cee13c49 Admin/Windows/launch4j/isabelle.ico Binary file Admin/Windows/launch4j/isabelle.ico has changed diff -r 4b93fc861cfa -r 3155cee13c49 Admin/Windows/launch4j/isabelle.xml --- /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 @@ + + true + gui + + Isabelle.exe + + + + normal + + + false + true + + isabelle.ico + + isabelle.Main + %EXEDIR%\lib\classes\ext\Pure.jar + %EXEDIR%\lib\classes\ext\scala-library.jar + %EXEDIR%\lib\classes\ext\scala-swing.jar + + + %EXEDIR%\contrib\jdk-6u31_x86-cygwin\jdk1.6.0_31 + + + jdkOnly + -Disabelle.home="%EXEDIR%" -Dcygwin.root="%EXEDIR%\\contrib\\cygwin-1.7.9" + + + isabelle.bmp + false + 10 + false + + \ No newline at end of file diff -r 4b93fc861cfa -r 3155cee13c49 Admin/exec_process/build --- 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 - - diff -r 4b93fc861cfa -r 3155cee13c49 Admin/exec_process/etc/settings --- 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" diff -r 4b93fc861cfa -r 3155cee13c49 Admin/exec_process/exec_process.c --- 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 -#include -#include -#include - - -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"); -} - diff -r 4b93fc861cfa -r 3155cee13c49 Admin/launch4j/Isabelle.exe Binary file Admin/launch4j/Isabelle.exe has changed diff -r 4b93fc861cfa -r 3155cee13c49 Admin/launch4j/README --- 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 diff -r 4b93fc861cfa -r 3155cee13c49 Admin/launch4j/isabelle.bmp Binary file Admin/launch4j/isabelle.bmp has changed diff -r 4b93fc861cfa -r 3155cee13c49 Admin/launch4j/isabelle.ico Binary file Admin/launch4j/isabelle.ico has changed diff -r 4b93fc861cfa -r 3155cee13c49 Admin/launch4j/isabelle.xml --- 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 @@ - - true - gui - - Isabelle.exe - - - - normal - - - false - true - - isabelle.ico - - isabelle.Main - %EXEDIR%\lib\classes\ext\Pure.jar - %EXEDIR%\lib\classes\ext\scala-library.jar - %EXEDIR%\lib\classes\ext\scala-swing.jar - - - %EXEDIR%\contrib\jdk-6u31_x86-cygwin\jdk1.6.0_31 - - - jdkOnly - -Disabelle.home="%EXEDIR%" -Dcygwin.root="%EXEDIR%\\contrib\\cygwin-1.7.9" - - - isabelle.bmp - false - 10 - false - - \ No newline at end of file diff -r 4b93fc861cfa -r 3155cee13c49 Admin/psbooklet --- 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)' diff -r 4b93fc861cfa -r 3155cee13c49 src/HOL/HOL.thy --- 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*} diff -r 4b93fc861cfa -r 3155cee13c49 src/HOL/HOLCF/IOA/meta_theory/CompoTraces.thy --- 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) \ Finite tr" + +lemma finiteR_mksch': "\ Finite tr \ \ 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)) diff -r 4b93fc861cfa -r 3155cee13c49 src/HOL/HOLCF/IOA/meta_theory/Sequence.thy --- 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 "\ ?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: diff -r 4b93fc861cfa -r 3155cee13c49 src/HOL/Word/Word.thy --- 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')) \ (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 diff -r 4b93fc861cfa -r 3155cee13c49 src/Pure/Isar/outer_syntax.ML --- 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 diff -r 4b93fc861cfa -r 3155cee13c49 src/Pure/System/gui_setup.scala --- 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) } } } diff -r 4b93fc861cfa -r 3155cee13c49 src/Pure/System/isabelle_system.scala --- 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 = diff -r 4b93fc861cfa -r 3155cee13c49 src/Pure/System/main.scala --- 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) } }