# HG changeset patch # User huffman # Date 1243832456 25200 # Node ID f20a61cec3d409a2c793d7da4439b58cee1b3fb2 # Parent 2261c8781f7387073f8f84728f870ce42f1c7757# Parent 526e149999cc547361a5ff18ff293d5831480439 merged diff -r 2261c8781f73 -r f20a61cec3d4 Admin/CHECKLIST --- a/Admin/CHECKLIST Sun May 31 21:59:33 2009 -0700 +++ b/Admin/CHECKLIST Sun May 31 22:00:56 2009 -0700 @@ -1,8 +1,9 @@ Checklist for official releases =============================== -- test mosml, polyml-5.2, polyml-5.1, polyml-5.0, polyml-4.1.3, polyml-4.1.4, polyml-4.2.0, - sparc-solaris, x86-solaris; +- test mosml, polyml-5.2, polyml-5.1, polyml-5.0; + +- test sparc-solaris, x86-solaris; - test ProofGeneral; diff -r 2261c8781f73 -r f20a61cec3d4 Admin/isatest/isatest-settings --- a/Admin/isatest/isatest-settings Sun May 31 21:59:33 2009 -0700 +++ b/Admin/isatest/isatest-settings Sun May 31 22:00:56 2009 -0700 @@ -1,4 +1,4 @@ -# -*- shell-script -*- +# -*- shell-script -*- :mode=shellscript: # $Id$ # Author: Gerwin Klein, NICTA # diff -r 2261c8781f73 -r f20a61cec3d4 Admin/isatest/settings/annomaly --- a/Admin/isatest/settings/annomaly Sun May 31 21:59:33 2009 -0700 +++ b/Admin/isatest/settings/annomaly Sun May 31 22:00:56 2009 -0700 @@ -1,3 +1,5 @@ +# -*- shell-script -*- :mode=shellscript: + ML_SYSTEM=annomaly ML_HOME="$SMLNJ_HOME/bin" ML_OPTIONS="-m $SMLNJ_HOME/annomaly/annomaly.cm @SMLdebug=/dev/null" diff -r 2261c8781f73 -r f20a61cec3d4 Admin/isatest/settings/at-mac-poly-5.1-para --- a/Admin/isatest/settings/at-mac-poly-5.1-para Sun May 31 21:59:33 2009 -0700 +++ b/Admin/isatest/settings/at-mac-poly-5.1-para Sun May 31 22:00:56 2009 -0700 @@ -1,7 +1,7 @@ -# -*- shell-script -*- +# -*- shell-script -*- :mode=shellscript: - POLYML_HOME="/home/polyml/polyml-5.2.1" - ML_SYSTEM="polyml-5.2.1" + POLYML_HOME="/home/polyml/polyml-svn" + ML_SYSTEM="polyml-experimental" ML_PLATFORM="x86-darwin" ML_HOME="$POLYML_HOME/$ML_PLATFORM" ML_OPTIONS="--mutable 800 --immutable 2000" diff -r 2261c8781f73 -r f20a61cec3d4 Admin/isatest/settings/at-poly --- a/Admin/isatest/settings/at-poly Sun May 31 21:59:33 2009 -0700 +++ b/Admin/isatest/settings/at-poly Sun May 31 22:00:56 2009 -0700 @@ -1,4 +1,4 @@ -# -*- shell-script -*- +# -*- shell-script -*- :mode=shellscript: POLYML_HOME="/home/polyml/polyml-5.2" ML_SYSTEM="polyml-5.2" diff -r 2261c8781f73 -r f20a61cec3d4 Admin/isatest/settings/at-poly-4.1.3 --- a/Admin/isatest/settings/at-poly-4.1.3 Sun May 31 21:59:33 2009 -0700 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,27 +0,0 @@ -# -*- shell-script -*- - - POLYML_HOME="/home/polyml/polyml-4.1.3" - ML_SYSTEM="polyml-4.1.3" - ML_PLATFORM="x86-linux" - ML_HOME="$POLYML_HOME/$ML_PLATFORM" - ML_OPTIONS="-h 30000" - -ISABELLE_HOME_USER=~/isabelle-at-poly-4.1.3 - -# Where to look for isabelle tools (multiple dirs separated by ':'). -ISABELLE_TOOLS="$ISABELLE_HOME/lib/Tools" - -# Location for temporary files (should be on a local file system). -ISABELLE_TMP_PREFIX="/tmp/isabelle-$USER" - - -# Heap input locations. ML system identifier is included in lookup. -ISABELLE_PATH="$ISABELLE_HOME_USER/heaps:$ISABELLE_HOME/heaps" - -# Heap output location. ML system identifier is appended automatically later on. -ISABELLE_OUTPUT="$ISABELLE_HOME_USER/heaps" -ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info" - -ISABELLE_USEDIR_OPTIONS="-i true -d pdf -v true" - -HOL_USEDIR_OPTIONS="-p 2" diff -r 2261c8781f73 -r f20a61cec3d4 Admin/isatest/settings/at-poly-5.1-para-e --- a/Admin/isatest/settings/at-poly-5.1-para-e Sun May 31 21:59:33 2009 -0700 +++ b/Admin/isatest/settings/at-poly-5.1-para-e Sun May 31 22:00:56 2009 -0700 @@ -1,4 +1,4 @@ -# -*- shell-script -*- +# -*- shell-script -*- :mode=shellscript: POLYML_HOME="/home/polyml/polyml-5.2.1" ML_SYSTEM="polyml-5.2.1" diff -r 2261c8781f73 -r f20a61cec3d4 Admin/isatest/settings/at-poly-dev-e --- a/Admin/isatest/settings/at-poly-dev-e Sun May 31 21:59:33 2009 -0700 +++ b/Admin/isatest/settings/at-poly-dev-e Sun May 31 22:00:56 2009 -0700 @@ -1,4 +1,4 @@ -# -*- shell-script -*- +# -*- shell-script -*- :mode=shellscript: POLYML_HOME="/home/polyml/polyml-5.2" ML_SYSTEM="polyml-5.2" diff -r 2261c8781f73 -r f20a61cec3d4 Admin/isatest/settings/at-poly-e --- a/Admin/isatest/settings/at-poly-e Sun May 31 21:59:33 2009 -0700 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,27 +0,0 @@ -# -*- shell-script -*- - - POLYML_HOME="/home/polyml/polyml-4.2.0" - ML_SYSTEM="polyml-4.2.0" - ML_PLATFORM="x86-linux" - ML_HOME="$POLYML_HOME/$ML_PLATFORM" - ML_OPTIONS="-h 30000" - -ISABELLE_HOME_USER=~/isabelle-at-poly-e - -# Where to look for isabelle tools (multiple dirs separated by ':'). -ISABELLE_TOOLS="$ISABELLE_HOME/lib/Tools" - -# Location for temporary files (should be on a local file system). -ISABELLE_TMP_PREFIX="/tmp/isabelle-$USER" - - -# Heap input locations. ML system identifier is included in lookup. -ISABELLE_PATH="$ISABELLE_HOME_USER/heaps:$ISABELLE_HOME/heaps" - -# Heap output location. ML system identifier is appended automatically later on. -ISABELLE_OUTPUT="$ISABELLE_HOME_USER/heaps" -ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info" - -ISABELLE_USEDIR_OPTIONS="-i true -d pdf -v true" - -HOL_USEDIR_OPTIONS="-p 2" diff -r 2261c8781f73 -r f20a61cec3d4 Admin/isatest/settings/at-sml --- a/Admin/isatest/settings/at-sml Sun May 31 21:59:33 2009 -0700 +++ b/Admin/isatest/settings/at-sml Sun May 31 22:00:56 2009 -0700 @@ -1,4 +1,4 @@ -# -*- shell-script -*- +# -*- shell-script -*- :mode=shellscript: # Standard ML of New Jersey 110 or later ML_SYSTEM=smlnj-110.0.7 diff -r 2261c8781f73 -r f20a61cec3d4 Admin/isatest/settings/at-sml-dev-e --- a/Admin/isatest/settings/at-sml-dev-e Sun May 31 21:59:33 2009 -0700 +++ b/Admin/isatest/settings/at-sml-dev-e Sun May 31 22:00:56 2009 -0700 @@ -1,4 +1,4 @@ -# -*- shell-script -*- +# -*- shell-script -*- :mode=shellscript: # Standard ML of New Jersey 110 or later ML_SYSTEM=smlnj diff -r 2261c8781f73 -r f20a61cec3d4 Admin/isatest/settings/at-sml-dev-p --- a/Admin/isatest/settings/at-sml-dev-p Sun May 31 21:59:33 2009 -0700 +++ b/Admin/isatest/settings/at-sml-dev-p Sun May 31 22:00:56 2009 -0700 @@ -1,4 +1,4 @@ -# -*- shell-script -*- +# -*- shell-script -*- :mode=shellscript: # Standard ML of New Jersey 110 or later ML_SYSTEM=smlnj diff -r 2261c8781f73 -r f20a61cec3d4 Admin/isatest/settings/at64-poly --- a/Admin/isatest/settings/at64-poly Sun May 31 21:59:33 2009 -0700 +++ b/Admin/isatest/settings/at64-poly Sun May 31 22:00:56 2009 -0700 @@ -1,4 +1,4 @@ -# -*- shell-script -*- +# -*- shell-script -*- :mode=shellscript: POLYML_HOME="/home/polyml/polyml-5.2" ML_SYSTEM="polyml-5.2" diff -r 2261c8781f73 -r f20a61cec3d4 Admin/isatest/settings/at64-poly-5.1-para --- a/Admin/isatest/settings/at64-poly-5.1-para Sun May 31 21:59:33 2009 -0700 +++ b/Admin/isatest/settings/at64-poly-5.1-para Sun May 31 22:00:56 2009 -0700 @@ -1,4 +1,4 @@ -# -*- shell-script -*- +# -*- shell-script -*- :mode=shellscript: POLYML_HOME="/home/polyml/polyml-5.2.1" ML_SYSTEM="polyml-5.2.1" diff -r 2261c8781f73 -r f20a61cec3d4 Admin/isatest/settings/at64-sml-dev --- a/Admin/isatest/settings/at64-sml-dev Sun May 31 21:59:33 2009 -0700 +++ b/Admin/isatest/settings/at64-sml-dev Sun May 31 22:00:56 2009 -0700 @@ -1,4 +1,4 @@ -# -*- shell-script -*- +# -*- shell-script -*- :mode=shellscript: # Standard ML of New Jersey 110 or later ML_SYSTEM=smlnj diff -r 2261c8781f73 -r f20a61cec3d4 Admin/isatest/settings/mac-poly --- a/Admin/isatest/settings/mac-poly Sun May 31 21:59:33 2009 -0700 +++ b/Admin/isatest/settings/mac-poly Sun May 31 22:00:56 2009 -0700 @@ -1,4 +1,4 @@ -# -*- shell-script -*- +# -*- shell-script -*- :mode=shellscript: POLYML_HOME="/home/polyml/polyml-5.2" ML_SYSTEM="polyml-5.2" diff -r 2261c8781f73 -r f20a61cec3d4 Admin/isatest/settings/mac-sml-dev --- a/Admin/isatest/settings/mac-sml-dev Sun May 31 21:59:33 2009 -0700 +++ b/Admin/isatest/settings/mac-sml-dev Sun May 31 22:00:56 2009 -0700 @@ -1,4 +1,4 @@ -# -*- shell-script -*- +# -*- shell-script -*- :mode=shellscript: # Standard ML of New Jersey 110 or later ML_SYSTEM=smlnj diff -r 2261c8781f73 -r f20a61cec3d4 Admin/isatest/settings/sun-poly --- a/Admin/isatest/settings/sun-poly Sun May 31 21:59:33 2009 -0700 +++ b/Admin/isatest/settings/sun-poly Sun May 31 22:00:56 2009 -0700 @@ -1,4 +1,4 @@ -# -*- shell-script -*- +# -*- shell-script -*- :mode=shellscript: POLYML_HOME="/home/polyml/polyml-5.1" ML_SYSTEM="polyml-5.1" diff -r 2261c8781f73 -r f20a61cec3d4 Admin/isatest/settings/sun-sml --- a/Admin/isatest/settings/sun-sml Sun May 31 21:59:33 2009 -0700 +++ b/Admin/isatest/settings/sun-sml Sun May 31 22:00:56 2009 -0700 @@ -1,4 +1,4 @@ -# -*- shell-script -*- +# -*- shell-script -*- :mode=shellscript: # Standard ML of New Jersey 110.0.7 (stable version) ML_SYSTEM=smlnj-110.0.7 diff -r 2261c8781f73 -r f20a61cec3d4 Admin/isatest/settings/sun-sml-dev --- a/Admin/isatest/settings/sun-sml-dev Sun May 31 21:59:33 2009 -0700 +++ b/Admin/isatest/settings/sun-sml-dev Sun May 31 22:00:56 2009 -0700 @@ -1,4 +1,4 @@ -# -*- shell-script -*- +# -*- shell-script -*- :mode=shellscript: # Standard ML of New Jersey 110 or later ML_SYSTEM=smlnj-110 diff -r 2261c8781f73 -r f20a61cec3d4 NEWS --- a/NEWS Sun May 31 21:59:33 2009 -0700 +++ b/NEWS Sun May 31 22:00:56 2009 -0700 @@ -26,6 +26,22 @@ by the code generator; see Predicate.thy for an example. +*** ML *** + +* Eliminated old Attrib.add_attributes, Method.add_methods and related +cominators for "args". INCOMPATIBILITY, need to use simplified +Attrib/Method.setup introduced in Isabelle2009. + + +*** System *** + +* Discontinued support for Poly/ML 4.x versions. + +* Removed "compress" option from isabelle-process and isabelle usedir; +this is always enabled. + + + New in Isabelle2009 (April 2009) -------------------------------- diff -r 2261c8781f73 -r f20a61cec3d4 bin/isabelle-process --- a/bin/isabelle-process Sun May 31 21:59:33 2009 -0700 +++ b/bin/isabelle-process Sun May 31 22:00:56 2009 -0700 @@ -26,13 +26,11 @@ echo "Usage: $PRG [OPTIONS] [INPUT] [OUTPUT]" echo echo " Options are:" - echo " -C tell ML system to copy output image" echo " -I startup Isar interaction mode" echo " -P startup Proof General interaction mode" echo " -S secure mode -- disallow critical operations" echo " -X startup PGIP interaction mode" echo " -W OUTPUT startup process wrapper, with messages going to OUTPUT stream" - echo " -c tell ML system to compress output image" echo " -e MLTEXT pass MLTEXT to the ML session" echo " -f pass 'Session.finish();' to the ML session" echo " -m MODE add print mode for output" @@ -60,25 +58,20 @@ # options -COPYDB="" ISAR=false PROOFGENERAL="" SECURE="" WRAPPER_OUTPUT="" PGIP="" -COMPRESS="" MLTEXT="" MODES="" TERMINATE="" READONLY="" NOWRITE="" -while getopts "CIPSW:Xce:fm:qruw" OPT +while getopts "IPSW:Xe:fm:qruw" OPT do case "$OPT" in - C) - COPYDB=true - ;; I) ISAR=true ;; @@ -94,9 +87,6 @@ X) PGIP=true ;; - c) - COMPRESS=true - ;; e) MLTEXT="$MLTEXT $OPTARG" ;; @@ -235,8 +225,7 @@ NICE="" fi -export INFILE OUTFILE COPYDB COMPRESS MLTEXT TERMINATE NOWRITE \ - ISABELLE_PID ISABELLE_TMP +export INFILE OUTFILE MLTEXT TERMINATE NOWRITE ISABELLE_PID ISABELLE_TMP if [ -f "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM" ]; then $NICE "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM" diff -r 2261c8781f73 -r f20a61cec3d4 doc-src/System/Thy/Basics.thy --- a/doc-src/System/Thy/Basics.thy Sun May 31 21:59:33 2009 -0700 +++ b/doc-src/System/Thy/Basics.thy Sun May 31 22:00:56 2009 -0700 @@ -266,13 +266,11 @@ Usage: isabelle-process [OPTIONS] [INPUT] [OUTPUT] Options are: - -C tell ML system to copy output image -I startup Isar interaction mode -P startup Proof General interaction mode -S secure mode -- disallow critical operations -W OUTPUT startup process wrapper, with messages going to OUTPUT stream -X startup PGIP interaction mode - -c tell ML system to compress output image -e MLTEXT pass MLTEXT to the ML session -f pass 'Session.finish();' to the ML session -m MODE add print mode for output @@ -320,16 +318,6 @@ read-only after terminating. Thus subsequent invocations cause the logic image to be read-only automatically. - \medskip The @{verbatim "-c"} option tells the underlying ML system - to compress the output heap (fully transparently). On Poly/ML for - example, the image is garbage collected and all stored values are - maximally shared, resulting in up to @{text "50%"} less disk space - consumption. - - \medskip The @{verbatim "-C"} option tells the ML system to produce - a completely self-contained output image, probably including a copy - of the ML runtime system itself. - \medskip Using the @{verbatim "-e"} option, arbitrary ML code may be passed to the Isabelle session from the command line. Multiple @{verbatim "-e"}'s are evaluated in the given order. Strange things diff -r 2261c8781f73 -r f20a61cec3d4 doc-src/System/Thy/Presentation.thy --- a/doc-src/System/Thy/Presentation.thy Sun May 31 21:59:33 2009 -0700 +++ b/doc-src/System/Thy/Presentation.thy Sun May 31 22:00:56 2009 -0700 @@ -446,7 +446,6 @@ -T LEVEL multithreading: trace level (default 0) -V VERSION declare alternative document VERSION -b build mode (output heap image, using current dir) - -c BOOL tell ML system to compress output image (default true) -d FORMAT build document as FORMAT (default false) -f NAME use ML file NAME (default ROOT.ML) -g BOOL generate session graph image for document (default false) diff -r 2261c8781f73 -r f20a61cec3d4 doc-src/System/Thy/document/Basics.tex --- a/doc-src/System/Thy/document/Basics.tex Sun May 31 21:59:33 2009 -0700 +++ b/doc-src/System/Thy/document/Basics.tex Sun May 31 22:00:56 2009 -0700 @@ -275,13 +275,11 @@ Usage: isabelle-process [OPTIONS] [INPUT] [OUTPUT] Options are: - -C tell ML system to copy output image -I startup Isar interaction mode -P startup Proof General interaction mode -S secure mode -- disallow critical operations -W OUTPUT startup process wrapper, with messages going to OUTPUT stream -X startup PGIP interaction mode - -c tell ML system to compress output image -e MLTEXT pass MLTEXT to the ML session -f pass 'Session.finish();' to the ML session -m MODE add print mode for output @@ -331,16 +329,6 @@ read-only after terminating. Thus subsequent invocations cause the logic image to be read-only automatically. - \medskip The \verb|-c| option tells the underlying ML system - to compress the output heap (fully transparently). On Poly/ML for - example, the image is garbage collected and all stored values are - maximally shared, resulting in up to \isa{{\isachardoublequote}{\isadigit{5}}{\isadigit{0}}{\isacharpercent}{\isachardoublequote}} less disk space - consumption. - - \medskip The \verb|-C| option tells the ML system to produce - a completely self-contained output image, probably including a copy - of the ML runtime system itself. - \medskip Using the \verb|-e| option, arbitrary ML code may be passed to the Isabelle session from the command line. Multiple \verb|-e|'s are evaluated in the given order. Strange things diff -r 2261c8781f73 -r f20a61cec3d4 doc-src/System/Thy/document/Presentation.tex --- a/doc-src/System/Thy/document/Presentation.tex Sun May 31 21:59:33 2009 -0700 +++ b/doc-src/System/Thy/document/Presentation.tex Sun May 31 22:00:56 2009 -0700 @@ -472,7 +472,6 @@ -T LEVEL multithreading: trace level (default 0) -V VERSION declare alternative document VERSION -b build mode (output heap image, using current dir) - -c BOOL tell ML system to compress output image (default true) -d FORMAT build document as FORMAT (default false) -f NAME use ML file NAME (default ROOT.ML) -g BOOL generate session graph image for document (default false) diff -r 2261c8781f73 -r f20a61cec3d4 doc-src/antiquote_setup.ML --- a/doc-src/antiquote_setup.ML Sun May 31 21:59:33 2009 -0700 +++ b/doc-src/antiquote_setup.ML Sun May 31 22:00:56 2009 -0700 @@ -159,9 +159,9 @@ end); fun entity_antiqs check markup kind = - [(entity check markup kind NONE), - (entity check markup kind (SOME true)), - (entity check markup kind (SOME false))]; + ((entity check markup kind NONE); + (entity check markup kind (SOME true)); + (entity check markup kind (SOME false))); in diff -r 2261c8781f73 -r f20a61cec3d4 etc/settings --- a/etc/settings Sun May 31 21:59:33 2009 -0700 +++ b/etc/settings Sun May 31 22:00:56 2009 -0700 @@ -15,7 +15,7 @@ # not invent new ML system names unless you know what you are doing. # Only one of the sections below should be activated. -# Poly/ML 4.x/5.x (automated settings) +# Poly/ML 5.x (automated settings) POLY_HOME="$(type -p poly)"; [ -n "$POLY_HOME" ] && POLY_HOME="$(dirname "$POLY_HOME")" ML_PLATFORM=$("$ISABELLE_HOME/lib/scripts/polyml-platform") ML_HOME=$(choosefrom \ @@ -29,24 +29,18 @@ ML_OPTIONS="-H 200" ML_DBASE="" -# Poly/ML 5.1 +# Poly/ML 5.2.1 #ML_PLATFORM=x86-linux #ML_HOME=/usr/local/polyml/x86-linux -#ML_SYSTEM=polyml-5.1 +#ML_SYSTEM=polyml-5.2.1 #ML_OPTIONS="-H 500" -# Poly/ML 5.1 (64 bit) +# Poly/ML 5.2.1 (64 bit) #ML_PLATFORM=x86_64-linux #ML_HOME=/usr/local/polyml/x86_64-linux -#ML_SYSTEM=polyml-5.1 +#ML_SYSTEM=polyml-5.2.1 #ML_OPTIONS="-H 1000" -# Poly/ML 4.2.0 -#ML_PLATFORM=x86-linux -#ML_HOME=/usr/local/polyml/x86-linux -#ML_SYSTEM=polyml-4.2.0 -#ML_OPTIONS="-H 80" - # Standard ML of New Jersey (slow!) #ML_SYSTEM=smlnj-110 #ML_HOME="/usr/local/smlnj/bin" diff -r 2261c8781f73 -r f20a61cec3d4 etc/user-settings.sample --- a/etc/user-settings.sample Sun May 31 21:59:33 2009 -0700 +++ b/etc/user-settings.sample Sun May 31 22:00:56 2009 -0700 @@ -1,4 +1,4 @@ -# -*- shell-script -*- +# -*- shell-script -*- :mode=shellscript: # # Isabelle user settings sample -- for use in ~/.isabelle/etc/settings diff -r 2261c8781f73 -r f20a61cec3d4 lib/Tools/usedir --- a/lib/Tools/usedir Sun May 31 21:59:33 2009 -0700 +++ b/lib/Tools/usedir Sun May 31 22:00:56 2009 -0700 @@ -23,7 +23,6 @@ echo " -T LEVEL multithreading: trace level (default 0)" echo " -V VERSION declare alternative document VERSION" echo " -b build mode (output heap image, using current dir)" - echo " -c BOOL tell ML system to compress output image (default true)" echo " -d FORMAT build document as FORMAT (default false)" echo " -f NAME use ML file NAME (default ROOT.ML)" echo " -g BOOL generate session graph image for document (default false)" @@ -77,7 +76,6 @@ TRACETHREADS="0" DOCUMENT_VERSIONS="" BUILD="" -COMPRESS=true DOCUMENT=false ROOT_FILE="ROOT.ML" DOCUMENT_GRAPH=false @@ -91,7 +89,7 @@ function getoptions() { OPTIND=1 - while getopts "C:D:M:P:Q:T:V:bc:d:f:g:i:m:p:rs:v:" OPT + while getopts "C:D:M:P:Q:T:V:bd:f:g:i:m:p:rs:v:" OPT do case "$OPT" in C) @@ -129,10 +127,6 @@ b) BUILD=true ;; - c) - check_bool "$OPTARG" - COMPRESS="$OPTARG" - ;; d) DOCUMENT="$OPTARG" ;; @@ -175,7 +169,8 @@ done } -getoptions $ISABELLE_USEDIR_OPTIONS +eval "OPTIONS=($ISABELLE_USEDIR_OPTIONS)" +getoptions "${OPTIONS[@]}" getoptions "$@" shift $(($OPTIND - 1)) @@ -233,12 +228,9 @@ echo "Building $ITEM ..." >&2 LOG="$LOGDIR/$ITEM" - OPT_C="" - [ "$COMPRESS" = true ] && OPT_C="-c" - "$ISABELLE_PROCESS" \ -e "Session.use_dir \"$ROOT_FILE\" true [$MODES] $RESET $INFO \"$DOC\" $DOCUMENT_GRAPH [$DOCUMENT_VERSIONS] \"$PARENT\" \"$SESSION\" ($COPY_DUMP, \"$DUMP\") \"$RPATH\" $PROOFS $VERBOSE $MAXTHREADS $TRACETHREADS $PARALLEL_PROOFS;" \ - $OPT_C -q -w $LOGIC $NAME > "$LOG" + -q -w $LOGIC $NAME > "$LOG" RC="$?" else ITEM=$(basename "$LOGIC")-"$SESSION" diff -r 2261c8781f73 -r f20a61cec3d4 lib/scripts/run-mosml --- a/lib/scripts/run-mosml Sun May 31 21:59:33 2009 -0700 +++ b/lib/scripts/run-mosml Sun May 31 22:00:56 2009 -0700 @@ -4,7 +4,7 @@ # # Moscow ML 2.00 startup script -export -n INFILE OUTFILE COPYDB COMPRESS MLTEXT TERMINATE NOWRITE +export -n INFILE OUTFILE MLTEXT TERMINATE NOWRITE ## diagnostics diff -r 2261c8781f73 -r f20a61cec3d4 lib/scripts/run-polyml --- a/lib/scripts/run-polyml Sun May 31 21:59:33 2009 -0700 +++ b/lib/scripts/run-polyml Sun May 31 22:00:56 2009 -0700 @@ -4,7 +4,7 @@ # # Poly/ML 5.1/5.2 startup script. -export -n INFILE OUTFILE COPYDB COMPRESS MLTEXT TERMINATE NOWRITE +export -n INFILE OUTFILE MLTEXT TERMINATE NOWRITE ## diagnostics @@ -54,11 +54,7 @@ if [ -z "$OUTFILE" ]; then COMMIT='fun commit () = (TextIO.output (TextIO.stdErr, "Error - Database is not opened for writing.\n"); false);' else - if [ -z "$COMPRESS" ]; then - COMMIT="fun commit () = (TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\"); PolyML.SaveState.saveState \"$OUTFILE\"; true);" - else - COMMIT="fun commit () = (PolyML.shareCommonData PolyML.rootFunction; TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\"); PolyML.SaveState.saveState \"$OUTFILE\"; true);" - fi + COMMIT="fun commit () = (PolyML.shareCommonData PolyML.rootFunction; TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\"); PolyML.SaveState.saveState \"$OUTFILE\"; true);" [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; } fi diff -r 2261c8781f73 -r f20a61cec3d4 lib/scripts/run-polyml-4.1.3 --- a/lib/scripts/run-polyml-4.1.3 Sun May 31 21:59:33 2009 -0700 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,106 +0,0 @@ -#!/usr/bin/env bash -# -# Author: Markus Wenzel, TU Muenchen -# -# Poly/ML 4.x startup script. - -export -n INFILE OUTFILE COPYDB COMPRESS MLTEXT TERMINATE NOWRITE - - -## diagnostics - -function fail_out() -{ - echo "Unable to create output heap file: \"$OUTFILE\"" >&2 - exit 2 -} - -function check_file() -{ - if [ ! -f "$1" ]; then - echo "Unable to locate $1" >&2 - echo "Please check your ML system settings!" >&2 - exit 2 - fi -} - - -## Poly/ML executable and database - -ML_DBASE_PREFIX="" - -POLY="$ML_HOME/poly" -check_file "$POLY" - -if [ -z "$ML_DBASE" ]; then - if [ ! -e "$ML_HOME/ML_dbase" -a "$(basename "$ML_HOME")" = bin ]; then - ML_DBASE_HOME="$(cd "$ML_HOME"; cd "$(pwd -P)"; cd ../lib/poly; pwd)" - else - ML_DBASE_HOME="$ML_HOME" - fi - if [ -z "$COPYDB" ]; then - ML_DBASE_PREFIX="$ML_DBASE_HOME/" - ML_DBASE="ML_dbase" - else - ML_DBASE="$ML_DBASE_HOME/ML_dbase" - fi - export POLYPATH="$ML_DBASE_HOME" -else - export POLYPATH="$(dirname "$ML_DBASE")" -fi - -DISCGARB_OPTIONS="-d -c" - -EXIT="fun exit 0 = (OS.Process.exit OS.Process.success): unit | exit _ = OS.Process.exit OS.Process.failure;" - - -## prepare databases - -if [ -z "$INFILE" ]; then - check_file "$ML_DBASE_PREFIX$ML_DBASE" - INFILE="$ML_DBASE" - MLTEXT="val use = PolyML.use; $EXIT $MLTEXT" - DISCGARB_OPTIONS="$DISCGARB_OPTIONS -S max" -else - COPYDB=true -fi - -if [ -z "$OUTFILE" ]; then - DB="$INFILE" - ML_OPTIONS="-r $ML_OPTIONS" -elif [ "$INFILE" -ef "$OUTFILE" ]; then - DB="$INFILE" -elif [ -n "$COPYDB" ]; then - [ -f "$OUTFILE" ] && { rm -f "$OUTFILE" || fail_out; } - cp "$INFILE" "$OUTFILE" || fail_out - chmod +w "$OUTFILE" || fail_out - DB="$OUTFILE" -else - [ -f "$OUTFILE" ] && { rm -f "$OUTFILE" || fail_out; } - echo "PolyML.make_database \"$OUTFILE\"; PolyML.quit();" | "$POLY" -r "$INFILE" - [ -f "$OUTFILE" ] || fail_out - DB="$OUTFILE" -fi - - -## run it! - -if [ -z "$TERMINATE" ]; then - FEEDER_OPTS="" -else - FEEDER_OPTS="-q" -fi - -DB_INFO="$(ls -l "$DB" 2>/dev/null)" - -"$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" $FEEDER_OPTS | { - read FPID; "$POLY" $ML_OPTIONS "$DB"; - RC="$?"; kill -HUP "$FPID"; exit "$RC"; } -RC="$?" - -NEW_DB_INFO="$(ls -l "$DB" 2>/dev/null)" -[ -n "$OUTFILE" -a -n "$COMPRESS" -a "$DB_INFO" != "$NEW_DB_INFO" ] && \ - "$POLY" $DISCGARB_OPTIONS "$OUTFILE" -[ -n "$OUTFILE" -a -f "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE" - -exit "$RC" diff -r 2261c8781f73 -r f20a61cec3d4 lib/scripts/run-polyml-4.1.4 --- a/lib/scripts/run-polyml-4.1.4 Sun May 31 21:59:33 2009 -0700 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,106 +0,0 @@ -#!/usr/bin/env bash -# -# Author: Markus Wenzel, TU Muenchen -# -# Poly/ML 4.x startup script. - -export -n INFILE OUTFILE COPYDB COMPRESS MLTEXT TERMINATE NOWRITE - - -## diagnostics - -function fail_out() -{ - echo "Unable to create output heap file: \"$OUTFILE\"" >&2 - exit 2 -} - -function check_file() -{ - if [ ! -f "$1" ]; then - echo "Unable to locate $1" >&2 - echo "Please check your ML system settings!" >&2 - exit 2 - fi -} - - -## Poly/ML executable and database - -ML_DBASE_PREFIX="" - -POLY="$ML_HOME/poly" -check_file "$POLY" - -if [ -z "$ML_DBASE" ]; then - if [ ! -e "$ML_HOME/ML_dbase" -a "$(basename "$ML_HOME")" = bin ]; then - ML_DBASE_HOME="$(cd "$ML_HOME"; cd "$(pwd -P)"; cd ../lib/poly; pwd)" - else - ML_DBASE_HOME="$ML_HOME" - fi - if [ -z "$COPYDB" ]; then - ML_DBASE_PREFIX="$ML_DBASE_HOME/" - ML_DBASE="ML_dbase" - else - ML_DBASE="$ML_DBASE_HOME/ML_dbase" - fi - export POLYPATH="$ML_DBASE_HOME" -else - export POLYPATH="$(dirname "$ML_DBASE")" -fi - -DISCGARB_OPTIONS="-d -c" - -EXIT="fun exit 0 = (OS.Process.exit OS.Process.success): unit | exit _ = OS.Process.exit OS.Process.failure;" - - -## prepare databases - -if [ -z "$INFILE" ]; then - check_file "$ML_DBASE_PREFIX$ML_DBASE" - INFILE="$ML_DBASE" - MLTEXT="val use = PolyML.use; $EXIT $MLTEXT" - DISCGARB_OPTIONS="$DISCGARB_OPTIONS -S max" -else - COPYDB=true -fi - -if [ -z "$OUTFILE" ]; then - DB="$INFILE" - ML_OPTIONS="-r $ML_OPTIONS" -elif [ "$INFILE" -ef "$OUTFILE" ]; then - DB="$INFILE" -elif [ -n "$COPYDB" ]; then - [ -f "$OUTFILE" ] && { rm -f "$OUTFILE" || fail_out; } - cp "$INFILE" "$OUTFILE" || fail_out - chmod +w "$OUTFILE" || fail_out - DB="$OUTFILE" -else - [ -f "$OUTFILE" ] && { rm -f "$OUTFILE" || fail_out; } - echo "PolyML.make_database \"$OUTFILE\"; PolyML.quit();" | "$POLY" -r "$INFILE" - [ -f "$OUTFILE" ] || fail_out - DB="$OUTFILE" -fi - - -## run it! - -if [ -z "$TERMINATE" ]; then - FEEDER_OPTS="" -else - FEEDER_OPTS="-q" -fi - -DB_INFO="$(ls -l "$DB" 2>/dev/null)" - -"$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" $FEEDER_OPTS | { - read FPID; "$POLY" $ML_OPTIONS "$DB"; - RC="$?"; kill -HUP "$FPID"; exit "$RC"; } -RC="$?" - -NEW_DB_INFO="$(ls -l "$DB" 2>/dev/null)" -[ -n "$OUTFILE" -a -n "$COMPRESS" -a "$DB_INFO" != "$NEW_DB_INFO" ] && \ - "$POLY" $DISCGARB_OPTIONS "$OUTFILE" -[ -n "$OUTFILE" -a -f "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE" - -exit "$RC" diff -r 2261c8781f73 -r f20a61cec3d4 lib/scripts/run-polyml-4.2.0 --- a/lib/scripts/run-polyml-4.2.0 Sun May 31 21:59:33 2009 -0700 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,106 +0,0 @@ -#!/usr/bin/env bash -# -# Author: Markus Wenzel, TU Muenchen -# -# Poly/ML 4.x startup script. - -export -n INFILE OUTFILE COPYDB COMPRESS MLTEXT TERMINATE NOWRITE - - -## diagnostics - -function fail_out() -{ - echo "Unable to create output heap file: \"$OUTFILE\"" >&2 - exit 2 -} - -function check_file() -{ - if [ ! -f "$1" ]; then - echo "Unable to locate $1" >&2 - echo "Please check your ML system settings!" >&2 - exit 2 - fi -} - - -## Poly/ML executable and database - -ML_DBASE_PREFIX="" - -POLY="$ML_HOME/poly" -check_file "$POLY" - -if [ -z "$ML_DBASE" ]; then - if [ ! -e "$ML_HOME/ML_dbase" -a "$(basename "$ML_HOME")" = bin ]; then - ML_DBASE_HOME="$(cd "$ML_HOME"; cd "$(pwd -P)"; cd ../lib/poly; pwd)" - else - ML_DBASE_HOME="$ML_HOME" - fi - if [ -z "$COPYDB" ]; then - ML_DBASE_PREFIX="$ML_DBASE_HOME/" - ML_DBASE="ML_dbase" - else - ML_DBASE="$ML_DBASE_HOME/ML_dbase" - fi - export POLYPATH="$ML_DBASE_HOME" -else - export POLYPATH="$(dirname "$ML_DBASE")" -fi - -DISCGARB_OPTIONS="-d -c" - -EXIT="fun exit 0 = (OS.Process.exit OS.Process.success): unit | exit _ = OS.Process.exit OS.Process.failure;" - - -## prepare databases - -if [ -z "$INFILE" ]; then - check_file "$ML_DBASE_PREFIX$ML_DBASE" - INFILE="$ML_DBASE" - MLTEXT="val use = PolyML.use; $EXIT $MLTEXT" - DISCGARB_OPTIONS="$DISCGARB_OPTIONS -S max" -else - COPYDB=true -fi - -if [ -z "$OUTFILE" ]; then - DB="$INFILE" - ML_OPTIONS="-r $ML_OPTIONS" -elif [ "$INFILE" -ef "$OUTFILE" ]; then - DB="$INFILE" -elif [ -n "$COPYDB" ]; then - [ -f "$OUTFILE" ] && { rm -f "$OUTFILE" || fail_out; } - cp "$INFILE" "$OUTFILE" || fail_out - chmod +w "$OUTFILE" || fail_out - DB="$OUTFILE" -else - [ -f "$OUTFILE" ] && { rm -f "$OUTFILE" || fail_out; } - echo "PolyML.make_database \"$OUTFILE\"; PolyML.quit();" | "$POLY" -r "$INFILE" - [ -f "$OUTFILE" ] || fail_out - DB="$OUTFILE" -fi - - -## run it! - -if [ -z "$TERMINATE" ]; then - FEEDER_OPTS="" -else - FEEDER_OPTS="-q" -fi - -DB_INFO="$(ls -l "$DB" 2>/dev/null)" - -"$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" $FEEDER_OPTS | { - read FPID; "$POLY" $ML_OPTIONS "$DB"; - RC="$?"; kill -HUP "$FPID"; exit "$RC"; } -RC="$?" - -NEW_DB_INFO="$(ls -l "$DB" 2>/dev/null)" -[ -n "$OUTFILE" -a -n "$COMPRESS" -a "$DB_INFO" != "$NEW_DB_INFO" ] && \ - "$POLY" $DISCGARB_OPTIONS "$OUTFILE" -[ -n "$OUTFILE" -a -f "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE" - -exit "$RC" diff -r 2261c8781f73 -r f20a61cec3d4 lib/scripts/run-polyml-5.0 --- a/lib/scripts/run-polyml-5.0 Sun May 31 21:59:33 2009 -0700 +++ b/lib/scripts/run-polyml-5.0 Sun May 31 22:00:56 2009 -0700 @@ -4,7 +4,7 @@ # # Poly/ML 5.0 startup script. -export -n INFILE OUTFILE COPYDB COMPRESS MLTEXT TERMINATE NOWRITE +export -n INFILE OUTFILE MLTEXT TERMINATE NOWRITE ## diagnostics @@ -54,11 +54,7 @@ if [ -z "$OUTFILE" ]; then COMMIT='fun commit () = (TextIO.output (TextIO.stdErr, "Error - Database is not opened for writing.\n"); false);' else - if [ -z "$COMPRESS" ]; then - COMMIT="fun commit () = (TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\"); PolyML.export (\"$OUTFILE\", PolyML.rootFunction); true);" - else - COMMIT="fun commit () = (PolyML.shareCommonData PolyML.rootFunction; TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\"); PolyML.export (\"$OUTFILE\", PolyML.rootFunction); true);" - fi + COMMIT="fun commit () = (PolyML.shareCommonData PolyML.rootFunction; TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\"); PolyML.export (\"$OUTFILE\", PolyML.rootFunction); true);" [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; } rm -f "${OUTFILE}.o" || fail_out fi diff -r 2261c8781f73 -r f20a61cec3d4 lib/scripts/run-smlnj --- a/lib/scripts/run-smlnj Sun May 31 21:59:33 2009 -0700 +++ b/lib/scripts/run-smlnj Sun May 31 22:00:56 2009 -0700 @@ -4,7 +4,7 @@ # # SML/NJ startup script (for 110 or later). -export -n INFILE OUTFILE COPYDB COMPRESS MLTEXT TERMINATE NOWRITE +export -n INFILE OUTFILE MLTEXT TERMINATE NOWRITE ## diagnostics diff -r 2261c8781f73 -r f20a61cec3d4 lib/scripts/timestart.bash --- a/lib/scripts/timestart.bash Sun May 31 21:59:33 2009 -0700 +++ b/lib/scripts/timestart.bash Sun May 31 22:00:56 2009 -0700 @@ -1,4 +1,4 @@ -# -*- shell-script -*- +# -*- shell-script -*- :mode=shellscript: # # Author: Makarius # diff -r 2261c8781f73 -r f20a61cec3d4 lib/scripts/timestop.bash --- a/lib/scripts/timestop.bash Sun May 31 21:59:33 2009 -0700 +++ b/lib/scripts/timestop.bash Sun May 31 22:00:56 2009 -0700 @@ -1,4 +1,4 @@ -# -*- shell-script -*- +# -*- shell-script -*- :mode=shellscript: # # Author: Makarius # diff -r 2261c8781f73 -r f20a61cec3d4 src/FOL/IFOL.thy --- a/src/FOL/IFOL.thy Sun May 31 21:59:33 2009 -0700 +++ b/src/FOL/IFOL.thy Sun May 31 22:00:56 2009 -0700 @@ -610,7 +610,7 @@ subsection {* Intuitionistic Reasoning *} -setup {* Intuitionistic.method_setup "iprover" *} +setup {* Intuitionistic.method_setup @{binding iprover} *} lemma impE': assumes 1: "P --> Q" diff -r 2261c8781f73 -r f20a61cec3d4 src/HOL/Decision_Procs/ferrack_tac.ML --- a/src/HOL/Decision_Procs/ferrack_tac.ML Sun May 31 21:59:33 2009 -0700 +++ b/src/HOL/Decision_Procs/ferrack_tac.ML Sun May 31 22:00:56 2009 -0700 @@ -2,6 +2,13 @@ Author: Amine Chaieb, TU Muenchen *) +signature FERRACK_TAC = +sig + val trace: bool ref + val linr_tac: Proof.context -> bool -> int -> tactic + val setup: theory -> theory +end + structure Ferrack_Tac = struct @@ -98,12 +105,10 @@ THEN tac) st end handle Subscript => no_tac st); -fun linr_meth src = - Method.syntax (Args.mode "no_quantify") src - #> (fn (q, ctxt) => SIMPLE_METHOD' (linr_tac ctxt (not q))); - val setup = - Method.add_method ("rferrack", linr_meth, - "decision procedure for linear real arithmetic"); + Method.setup @{binding rferrack} + (Args.mode "no_quantify" >> (fn q => fn ctxt => + SIMPLE_METHOD' (linr_tac ctxt (not q)))) + "decision procedure for linear real arithmetic"; end diff -r 2261c8781f73 -r f20a61cec3d4 src/HOL/HOL.thy --- a/src/HOL/HOL.thy Sun May 31 21:59:33 2009 -0700 +++ b/src/HOL/HOL.thy Sun May 31 22:00:56 2009 -0700 @@ -31,7 +31,7 @@ ("Tools/recfun_codegen.ML") begin -setup {* Intuitionistic.method_setup "iprover" *} +setup {* Intuitionistic.method_setup @{binding iprover} *} subsection {* Primitive logic *} diff -r 2261c8781f73 -r f20a61cec3d4 src/HOL/Library/Efficient_Nat.thy --- a/src/HOL/Library/Efficient_Nat.thy Sun May 31 21:59:33 2009 -0700 +++ b/src/HOL/Library/Efficient_Nat.thy Sun May 31 22:00:56 2009 -0700 @@ -317,7 +317,7 @@ setup {* fold (Numeral.add_code @{const_name number_nat_inst.number_of_nat} - true false) ["SML", "OCaml", "Haskell"] + false true) ["SML", "OCaml", "Haskell"] *} text {* diff -r 2261c8781f73 -r f20a61cec3d4 src/HOL/Relation_Power.thy --- a/src/HOL/Relation_Power.thy Sun May 31 21:59:33 2009 -0700 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,154 +0,0 @@ -(* Title: HOL/Relation_Power.thy - Author: Tobias Nipkow - Copyright 1996 TU Muenchen -*) - -header{*Powers of Relations and Functions*} - -theory Relation_Power -imports Power Transitive_Closure Plain -begin - -consts funpower :: "('a \ 'b) \ nat \ 'a \ 'b" (infixr "^^" 80) - -overloading - relpow \ "funpower \ ('a \ 'a) set \ nat \ ('a \ 'a) set" -begin - -text {* @{text "R ^^ n = R O ... O R"}, the n-fold composition of @{text R} *} - -primrec relpow where - "(R \ ('a \ 'a) set) ^^ 0 = Id" - | "(R \ ('a \ 'a) set) ^^ Suc n = R O (R ^^ n)" - -end - -overloading - funpow \ "funpower \ ('a \ 'a) \ nat \ 'a \ 'a" -begin - -text {* @{text "f ^^ n = f o ... o f"}, the n-fold composition of @{text f} *} - -primrec funpow where - "(f \ 'a \ 'a) ^^ 0 = id" - | "(f \ 'a \ 'a) ^^ Suc n = f o (f ^^ n)" - -end - -primrec fun_pow :: "nat \ ('a \ 'a) \ 'a \ 'a" where - "fun_pow 0 f = id" - | "fun_pow (Suc n) f = f o fun_pow n f" - -lemma funpow_fun_pow [code unfold]: - "f ^^ n = fun_pow n f" - unfolding funpow_def fun_pow_def .. - -lemma funpow_add: - "f ^^ (m + n) = f ^^ m o f ^^ n" - by (induct m) simp_all - -lemma funpow_swap1: - "f ((f ^^ n) x) = (f ^^ n) (f x)" -proof - - have "f ((f ^^ n) x) = (f ^^ (n+1)) x" unfolding One_nat_def by simp - also have "\ = (f ^^ n o f ^^ 1) x" by (simp only: funpow_add) - also have "\ = (f ^^ n) (f x)" unfolding One_nat_def by simp - finally show ?thesis . -qed - -lemma rel_pow_1 [simp]: - fixes R :: "('a * 'a) set" - shows "R ^^ 1 = R" - by simp - -lemma rel_pow_0_I: - "(x, x) \ R ^^ 0" - by simp - -lemma rel_pow_Suc_I: - "(x, y) \ R ^^ n \ (y, z) \ R \ (x, z) \ R ^^ Suc n" - by auto - -lemma rel_pow_Suc_I2: - "(x, y) \ R \ (y, z) \ R ^^ n \ (x, z) \ R ^^ Suc n" - by (induct n arbitrary: z) (simp, fastsimp) - -lemma rel_pow_0_E: - "(x, y) \ R ^^ 0 \ (x = y \ P) \ P" - by simp - -lemma rel_pow_Suc_E: - "(x, z) \ R ^^ Suc n \ (\y. (x, y) \ R ^^ n \ (y, z) \ R \ P) \ P" - by auto - -lemma rel_pow_E: - "(x, z) \ R ^^ n \ (n = 0 \ x = z \ P) - \ (\y m. n = Suc m \ (x, y) \ R ^^ m \ (y, z) \ R \ P) - \ P" - by (cases n) auto - -lemma rel_pow_Suc_D2: - "(x, z) \ R ^^ Suc n \ (\y. (x, y) \ R \ (y, z) \ R ^^ n)" - apply (induct n arbitrary: x z) - apply (blast intro: rel_pow_0_I elim: rel_pow_0_E rel_pow_Suc_E) - apply (blast intro: rel_pow_Suc_I elim: rel_pow_0_E rel_pow_Suc_E) - done - -lemma rel_pow_Suc_D2': - "\x y z. (x, y) \ R ^^ n \ (y, z) \ R \ (\w. (x, w) \ R \ (w, z) \ R ^^ n)" - by (induct n) (simp_all, blast) - -lemma rel_pow_E2: - "(x, z) \ R ^^ n \ (n = 0 \ x = z \ P) - \ (\y m. n = Suc m \ (x, y) \ R \ (y, z) \ R ^^ m \ P) - \ P" - apply (cases n, simp) - apply (cut_tac n=nat and R=R in rel_pow_Suc_D2', simp, blast) - done - -lemma rtrancl_imp_UN_rel_pow: - "p \ R^* \ p \ (\n. R ^^ n)" - apply (cases p) apply (simp only:) - apply (erule rtrancl_induct) - apply (blast intro: rel_pow_0_I rel_pow_Suc_I)+ - done - -lemma rel_pow_imp_rtrancl: - "p \ R ^^ n \ p \ R^*" - apply (induct n arbitrary: p) - apply (simp_all only: split_tupled_all) - apply (blast intro: rtrancl_refl elim: rel_pow_0_E) - apply (blast elim: rel_pow_Suc_E intro: rtrancl_into_rtrancl) - done - -lemma rtrancl_is_UN_rel_pow: - "R^* = (UN n. R ^^ n)" - by (blast intro: rtrancl_imp_UN_rel_pow rel_pow_imp_rtrancl) - -lemma trancl_power: - "x \ r^+ = (\n > 0. x \ r ^^ n)" - apply (cases x) - apply simp - apply (rule iffI) - apply (drule tranclD2) - apply (clarsimp simp: rtrancl_is_UN_rel_pow) - apply (rule_tac x="Suc x" in exI) - apply (clarsimp simp: rel_comp_def) - apply fastsimp - apply clarsimp - apply (case_tac n, simp) - apply clarsimp - apply (drule rel_pow_imp_rtrancl) - apply fastsimp - done - -lemma single_valued_rel_pow: - fixes R :: "('a * 'a) set" - shows "single_valued R \ single_valued (R ^^ n)" - apply (induct n arbitrary: R) - apply simp_all - apply (rule single_valuedI) - apply (fast dest: single_valuedD elim: rel_pow_Suc_E) - done - -end diff -r 2261c8781f73 -r f20a61cec3d4 src/HOL/Tools/primrec_package.ML --- a/src/HOL/Tools/primrec_package.ML Sun May 31 21:59:33 2009 -0700 +++ b/src/HOL/Tools/primrec_package.ML Sun May 31 22:00:56 2009 -0700 @@ -268,7 +268,7 @@ val (fixes, spec) = fst (prep_spec raw_fixes raw_spec lthy); fun attr_bindings prefix = map (fn ((b, attrs), _) => (Binding.qualify false prefix b, Code.add_default_eqn_attrib :: attrs)) spec; - fun simp_attr_binding prefix = (Binding.qualify false prefix (Binding.name "simps"), + fun simp_attr_binding prefix = (Binding.qualify true prefix (Binding.name "simps"), map (Attrib.internal o K) [Simplifier.simp_add, Nitpick_Const_Simp_Thms.add, Quickcheck_RecFun_Simp_Thms.add]); in diff -r 2261c8781f73 -r f20a61cec3d4 src/HOL/ex/predicate_compile.ML --- a/src/HOL/ex/predicate_compile.ML Sun May 31 21:59:33 2009 -0700 +++ b/src/HOL/ex/predicate_compile.ML Sun May 31 22:00:56 2009 -0700 @@ -31,6 +31,8 @@ (* debug stuff *) +fun makestring _ = "?"; (* FIXME dummy *) + fun tracing s = (if ! Toplevel.debug then Output.tracing s else ()); fun print_tac s = (if ! Toplevel.debug then Tactical.print_tac s else Seq.single); diff -r 2261c8781f73 -r f20a61cec3d4 src/Pure/IsaMakefile --- a/src/Pure/IsaMakefile Sun May 31 21:59:33 2009 -0700 +++ b/src/Pure/IsaMakefile Sun May 31 22:00:56 2009 -0700 @@ -19,16 +19,15 @@ ## Pure -BOOTSTRAP_FILES = ML-Systems/exn.ML ML-Systems/ml_name_space.ML \ +BOOTSTRAP_FILES = ML-Systems/compiler_polyml-5.0.ML \ + ML-Systems/compiler_polyml-5.2.ML ML-Systems/compiler_polyml-5.3.ML \ + ML-Systems/exn.ML ML-Systems/ml_name_space.ML \ ML-Systems/ml_pretty.ML ML-Systems/mosml.ML \ ML-Systems/multithreading.ML ML-Systems/multithreading_polyml.ML \ - ML-Systems/overloading_smlnj.ML ML-Systems/polyml-4.1.3.ML \ - ML-Systems/polyml-4.1.4.ML ML-Systems/polyml-4.2.0.ML \ - ML-Systems/polyml-5.0.ML ML-Systems/polyml-5.1.ML \ - ML-Systems/polyml-experimental.ML ML-Systems/polyml.ML \ - ML-Systems/polyml_common.ML ML-Systems/polyml_old_compiler4.ML \ - ML-Systems/polyml_old_compiler5.ML ML-Systems/polyml_pp.ML \ - ML-Systems/proper_int.ML ML-Systems/smlnj.ML \ + ML-Systems/overloading_smlnj.ML ML-Systems/polyml-5.0.ML \ + ML-Systems/polyml-5.1.ML ML-Systems/polyml-experimental.ML \ + ML-Systems/polyml.ML ML-Systems/polyml_common.ML \ + ML-Systems/pp_polyml.ML ML-Systems/proper_int.ML ML-Systems/smlnj.ML \ ML-Systems/system_shell.ML ML-Systems/thread_dummy.ML \ ML-Systems/time_limit.ML ML-Systems/universal.ML diff -r 2261c8781f73 -r f20a61cec3d4 src/Pure/Isar/attrib.ML --- a/src/Pure/Isar/attrib.ML Sun May 31 21:59:33 2009 -0700 +++ b/src/Pure/Isar/attrib.ML Sun May 31 22:00:56 2009 -0700 @@ -26,14 +26,10 @@ (('c * 'a list) * ('b * 'a list) list) list -> (('c * 'att list) * ('fact * 'att list) list) list val crude_closure: Proof.context -> src -> src - val add_attributes: (bstring * (src -> attribute) * string) list -> theory -> theory - val syntax: attribute context_parser -> src -> attribute val setup: Binding.binding -> attribute context_parser -> string -> theory -> theory val attribute_setup: bstring * Position.T -> Symbol_Pos.text * Position.T -> string -> theory -> theory - val no_args: attribute -> src -> attribute val add_del: attribute -> attribute -> attribute context_parser - val add_del_args: attribute -> attribute -> src -> attribute val thm_sel: Facts.interval list parser val thm: thm context_parser val thms: thm list context_parser @@ -89,6 +85,10 @@ |> Pretty.chunks |> Pretty.writeln end; +fun add_attribute name att comment thy = thy |> Attributes.map (fn atts => + #2 (NameSpace.define (Sign.naming_of thy) (name, ((att, comment), stamp ())) atts) + handle Symtab.DUP dup => error ("Duplicate declaration of attribute " ^ quote dup)); + (* name space *) @@ -149,24 +149,13 @@ Args.closure src); -(* add_attributes *) - -fun add_attributes raw_attrs thy = - let - val new_attrs = - raw_attrs |> map (fn (name, att, comment) => (Binding.name name, ((att, comment), stamp ()))); - fun add attrs = fold (snd oo NameSpace.define (Sign.naming_of thy)) new_attrs attrs - handle Symtab.DUP dup => error ("Duplicate declaration of attributes " ^ quote dup); - in Attributes.map add thy end; - - (* attribute setup *) -fun syntax scan src (context, th) = - let val (f: attribute, context') = Args.syntax "attribute" scan src context - in f (context', th) end; +fun syntax scan = Args.syntax "attribute" scan; -fun setup name scan comment = add_attributes [(Binding.name_of name, syntax scan, comment)]; +fun setup name scan = + add_attribute name + (fn src => fn (ctxt, th) => let val (a, ctxt') = syntax scan src ctxt in a (ctxt', th) end); fun attribute_setup name (txt, pos) cmt = Context.theory_map (ML_Context.expression pos @@ -175,12 +164,9 @@ ("(" ^ ML_Syntax.make_binding name ^ ", " ^ txt ^ ", " ^ ML_Syntax.print_string cmt ^ ")")); -(* basic syntax *) +(* add/del syntax *) -fun no_args x = syntax (Scan.succeed x); - -fun add_del add del = (Scan.lift (Args.add >> K add || Args.del >> K del || Scan.succeed add)); -fun add_del_args add del = syntax (add_del add del); +fun add_del add del = Scan.lift (Args.add >> K add || Args.del >> K del || Scan.succeed add); @@ -237,113 +223,99 @@ fun internal att = Args.src (("Pure.attribute", [T.mk_attribute att]), Position.none); -val internal_att = - syntax (Scan.lift Args.internal_attribute >> Morphism.form); - - -(* tags *) - -val tagged = syntax (Scan.lift (Args.name -- Args.name) >> Thm.tag); -val untagged = syntax (Scan.lift Args.name >> Thm.untag); - -val kind = syntax (Scan.lift Args.name >> Thm.kind); - (* rule composition *) val COMP_att = - syntax (Scan.lift (Scan.optional (Args.bracks P.nat) 1) -- thm - >> (fn (i, B) => Thm.rule_attribute (fn _ => fn A => Drule.compose_single (A, i, B)))); + Scan.lift (Scan.optional (Args.bracks P.nat) 1) -- thm + >> (fn (i, B) => Thm.rule_attribute (fn _ => fn A => Drule.compose_single (A, i, B))); val THEN_att = - syntax (Scan.lift (Scan.optional (Args.bracks P.nat) 1) -- thm - >> (fn (i, B) => Thm.rule_attribute (fn _ => fn A => A RSN (i, B)))); + Scan.lift (Scan.optional (Args.bracks P.nat) 1) -- thm + >> (fn (i, B) => Thm.rule_attribute (fn _ => fn A => A RSN (i, B))); val OF_att = - syntax (thms >> (fn Bs => Thm.rule_attribute (fn _ => fn A => Bs MRS A))); + thms >> (fn Bs => Thm.rule_attribute (fn _ => fn A => Bs MRS A)); (* rename_abs *) -val rename_abs = syntax - (Scan.lift (Scan.repeat (Args.maybe Args.name) >> (apsnd o Drule.rename_bvars'))); +val rename_abs = Scan.repeat (Args.maybe Args.name) >> (apsnd o Drule.rename_bvars'); (* unfold / fold definitions *) fun unfolded_syntax rule = - syntax (thms >> - (fn ths => Thm.rule_attribute (fn context => rule (Context.proof_of context) ths))); + thms >> (fn ths => Thm.rule_attribute (fn context => rule (Context.proof_of context) ths)); val unfolded = unfolded_syntax LocalDefs.unfold; val folded = unfolded_syntax LocalDefs.fold; -(* rule cases *) - -val consumes = syntax (Scan.lift (Scan.optional P.nat 1) >> RuleCases.consumes); -val case_names = syntax (Scan.lift (Scan.repeat1 Args.name) >> RuleCases.case_names); -val case_conclusion = - syntax (Scan.lift (Args.name -- Scan.repeat Args.name) >> RuleCases.case_conclusion); -val params = syntax (Scan.lift (P.and_list1 (Scan.repeat Args.name)) >> RuleCases.params); - - (* rule format *) -val rule_format = syntax (Args.mode "no_asm" - >> (fn true => ObjectLogic.rule_format_no_asm | false => ObjectLogic.rule_format)); +val rule_format = Args.mode "no_asm" + >> (fn true => ObjectLogic.rule_format_no_asm | false => ObjectLogic.rule_format); -val elim_format = no_args (Thm.rule_attribute (K Tactic.make_elim)); +val elim_format = Thm.rule_attribute (K Tactic.make_elim); (* misc rules *) -val standard = no_args (Thm.rule_attribute (K Drule.standard)); - -val no_vars = no_args (Thm.rule_attribute (fn context => fn th => +val no_vars = Thm.rule_attribute (fn context => fn th => let val ctxt = Variable.set_body false (Context.proof_of context); val ((_, [th']), _) = Variable.import_thms true [th] ctxt; - in th' end)); + in th' end); val eta_long = - no_args (Thm.rule_attribute (K (Conv.fconv_rule Drule.eta_long_conversion))); + Thm.rule_attribute (K (Conv.fconv_rule Drule.eta_long_conversion)); -val rotated = syntax - (Scan.lift (Scan.optional P.int 1) >> (fn n => Thm.rule_attribute (K (rotate_prems n)))); - -val abs_def = no_args (Thm.rule_attribute (K Drule.abs_def)); +val rotated = Scan.optional P.int 1 >> (fn n => Thm.rule_attribute (K (rotate_prems n))); (* theory setup *) val _ = Context.>> (Context.map_theory - (add_attributes - [("attribute", internal_att, "internal attribute"), - ("tagged", tagged, "tagged theorem"), - ("untagged", untagged, "untagged theorem"), - ("kind", kind, "theorem kind"), - ("COMP", COMP_att, "direct composition with rules (no lifting)"), - ("THEN", THEN_att, "resolution with rule"), - ("OF", OF_att, "rule applied to facts"), - ("rename_abs", rename_abs, "rename bound variables in abstractions"), - ("unfolded", unfolded, "unfolded definitions"), - ("folded", folded, "folded definitions"), - ("standard", standard, "result put into standard form"), - ("elim_format", elim_format, "destruct rule turned into elimination rule format"), - ("no_vars", no_vars, "frozen schematic vars"), - ("eta_long", eta_long, "put theorem into eta long beta normal form"), - ("consumes", consumes, "number of consumed facts"), - ("case_names", case_names, "named rule cases"), - ("case_conclusion", case_conclusion, "named conclusion of rule cases"), - ("params", params, "named rule parameters"), - ("atomize", no_args ObjectLogic.declare_atomize, "declaration of atomize rule"), - ("rulify", no_args ObjectLogic.declare_rulify, "declaration of rulify rule"), - ("rule_format", rule_format, "result put into standard rule format"), - ("rotated", rotated, "rotated theorem premises"), - ("defn", add_del_args LocalDefs.defn_add LocalDefs.defn_del, - "declaration of definitional transformations"), - ("abs_def", abs_def, "abstract over free variables of a definition")])); + (setup (Binding.name "attribute") (Scan.lift Args.internal_attribute >> Morphism.form) + "internal attribute" #> + setup (Binding.name "tagged") (Scan.lift (Args.name -- Args.name) >> Thm.tag) "tagged theorem" #> + setup (Binding.name "untagged") (Scan.lift Args.name >> Thm.untag) "untagged theorem" #> + setup (Binding.name "kind") (Scan.lift Args.name >> Thm.kind) "theorem kind" #> + setup (Binding.name "COMP") COMP_att "direct composition with rules (no lifting)" #> + setup (Binding.name "THEN") THEN_att "resolution with rule" #> + setup (Binding.name "OF") OF_att "rule applied to facts" #> + setup (Binding.name "rename_abs") (Scan.lift rename_abs) + "rename bound variables in abstractions" #> + setup (Binding.name "unfolded") unfolded "unfolded definitions" #> + setup (Binding.name "folded") folded "folded definitions" #> + setup (Binding.name "consumes") (Scan.lift (Scan.optional P.nat 1) >> RuleCases.consumes) + "number of consumed facts" #> + setup (Binding.name "case_names") (Scan.lift (Scan.repeat1 Args.name) >> RuleCases.case_names) + "named rule cases" #> + setup (Binding.name "case_conclusion") + (Scan.lift (Args.name -- Scan.repeat Args.name) >> RuleCases.case_conclusion) + "named conclusion of rule cases" #> + setup (Binding.name "params") + (Scan.lift (P.and_list1 (Scan.repeat Args.name)) >> RuleCases.params) + "named rule parameters" #> + setup (Binding.name "standard") (Scan.succeed (Thm.rule_attribute (K Drule.standard))) + "result put into standard form (legacy)" #> + setup (Binding.name "rule_format") rule_format "result put into canonical rule format" #> + setup (Binding.name "elim_format") (Scan.succeed elim_format) + "destruct rule turned into elimination rule format" #> + setup (Binding.name "no_vars") (Scan.succeed no_vars) "frozen schematic vars" #> + setup (Binding.name "eta_long") (Scan.succeed eta_long) + "put theorem into eta long beta normal form" #> + setup (Binding.name "atomize") (Scan.succeed ObjectLogic.declare_atomize) + "declaration of atomize rule" #> + setup (Binding.name "rulify") (Scan.succeed ObjectLogic.declare_rulify) + "declaration of rulify rule" #> + setup (Binding.name "rotated") (Scan.lift rotated) "rotated theorem premises" #> + setup (Binding.name "defn") (add_del LocalDefs.defn_add LocalDefs.defn_del) + "declaration of definitional transformations" #> + setup (Binding.name "abs_def") (Scan.succeed (Thm.rule_attribute (K Drule.abs_def))) + "abstract over free variables of a definition")); @@ -397,8 +369,8 @@ val name = Sign.full_bname thy bname; in thy - |> add_attributes [(bname, syntax (Scan.lift (scan_config thy config) >> Morphism.form), - "configuration option")] + |> setup (Binding.name bname) (Scan.lift (scan_config thy config) >> Morphism.form) + "configuration option" |> Configs.map (Symtab.update (name, config)) end; diff -r 2261c8781f73 -r f20a61cec3d4 src/Pure/Isar/method.ML --- a/src/Pure/Isar/method.ML Sun May 31 21:59:33 2009 -0700 +++ b/src/Pure/Isar/method.ML Sun May 31 22:00:56 2009 -0700 @@ -75,30 +75,13 @@ val defined: theory -> string -> bool val method: theory -> src -> Proof.context -> method val method_i: theory -> src -> Proof.context -> method - val add_methods: (bstring * (src -> Proof.context -> method) * string) list - -> theory -> theory - val add_method: bstring * (src -> Proof.context -> method) * string - -> theory -> theory val syntax: 'a context_parser -> src -> Proof.context -> 'a * Proof.context val setup: binding -> (Proof.context -> method) context_parser -> string -> theory -> theory val method_setup: bstring * Position.T -> Symbol_Pos.text * Position.T -> string -> theory -> theory - val simple_args: 'a parser -> ('a -> Proof.context -> method) -> src -> Proof.context -> method - val ctxt_args: (Proof.context -> method) -> src -> Proof.context -> method type modifier = (Proof.context -> Proof.context) * attribute val section: modifier parser list -> thm list context_parser val sections: modifier parser list -> thm list list context_parser - val sectioned_args: 'a context_parser -> modifier parser list -> - ('a -> Proof.context -> 'b) -> src -> Proof.context -> 'b - val bang_sectioned_args: modifier parser list -> - (thm list -> Proof.context -> 'a) -> src -> Proof.context -> 'a - val bang_sectioned_args': modifier parser list -> 'a context_parser -> - ('a -> thm list -> Proof.context -> 'b) -> src -> Proof.context -> 'b - val only_sectioned_args: modifier parser list -> (Proof.context -> 'a) -> src -> - Proof.context -> 'a - val thms_ctxt_args: (thm list -> Proof.context -> 'a) -> src -> Proof.context -> 'a - val thms_args: (thm list -> 'a) -> src -> Proof.context -> 'a - val thm_args: (thm -> 'a) -> src -> Proof.context -> 'a val parse: text parser end; @@ -356,6 +339,10 @@ |> Pretty.chunks |> Pretty.writeln end; +fun add_method name meth comment thy = thy |> Methods.map (fn meths => + #2 (NameSpace.define (Sign.naming_of thy) (name, ((meth, comment), stamp ())) meths) + handle Symtab.DUP dup => error ("Duplicate declaration of method " ^ quote dup)); + (* get methods *) @@ -376,27 +363,13 @@ fun method thy = method_i thy o Args.map_name (NameSpace.intern (#1 (Methods.get thy))); -(* add method *) - -fun add_methods raw_meths thy = - let - val new_meths = raw_meths |> map (fn (name, f, comment) => - (Binding.name name, ((f, comment), stamp ()))); - - fun add meths = fold (snd oo NameSpace.define (Sign.naming_of thy)) new_meths meths - handle Symtab.DUP dup => error ("Duplicate declaration of method " ^ quote dup); - in Methods.map add thy end; - -val add_method = add_methods o Library.single; - - (* method setup *) fun syntax scan = Args.context_syntax "method" scan; -fun setup name scan comment = - add_methods [(Binding.name_of name, - fn src => fn ctxt => let val (m, ctxt') = syntax scan src ctxt in m ctxt' end, comment)]; +fun setup name scan = + add_method name + (fn src => fn ctxt => let val (m, ctxt') = syntax scan src ctxt in m ctxt' end); fun method_setup name (txt, pos) cmt = Context.theory_map (ML_Context.expression pos @@ -411,15 +384,6 @@ structure P = OuterParse; -(* basic *) - -fun simple_args scan f src ctxt : method = - fst (syntax (Scan.lift (scan >> (fn x => f x ctxt))) src ctxt); - -fun ctxt_args (f: Proof.context -> method) src ctxt = - fst (syntax (Scan.succeed (f ctxt)) src ctxt); - - (* sections *) type modifier = (Proof.context -> Proof.context) * attribute; @@ -436,19 +400,6 @@ fun sections ss = Scan.repeat (section ss); -fun sectioned_args args ss f src ctxt = - let val ((x, _), ctxt') = syntax (args -- sections ss) src ctxt - in f x ctxt' end; - -fun bang_sectioned_args ss f = sectioned_args Args.bang_facts ss f; -fun bang_sectioned_args' ss scan f = - sectioned_args (Args.bang_facts -- scan >> swap) ss (uncurry f); -fun only_sectioned_args ss f = sectioned_args (Scan.succeed ()) ss (fn () => f); - -fun thms_ctxt_args f = sectioned_args (thms []) [] f; -fun thms_args f = thms_ctxt_args (K o f); -fun thm_args f = thms_args (fn [thm] => f thm | _ => error "Single theorem expected"); - end; diff -r 2261c8781f73 -r f20a61cec3d4 src/Pure/ML-Systems/compiler_polyml-5.0.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/ML-Systems/compiler_polyml-5.0.ML Sun May 31 22:00:56 2009 -0700 @@ -0,0 +1,32 @@ +(* Title: Pure/ML-Systems/compiler_polyml-5.0.ML + +Runtime compilation -- for PolyML.compilerEx in version 5.0 and 5.1. +*) + +fun use_text ({tune_source, print, error, ...}: use_context) (line, name) verbose txt = + let + val in_buffer = ref (explode (tune_source txt)); + val out_buffer = ref ([]: string list); + fun output () = implode (rev (case ! out_buffer of "\n" :: cs => cs | cs => cs)); + + val current_line = ref line; + fun get () = + (case ! in_buffer of + [] => "" + | c :: cs => (in_buffer := cs; if c = "\n" then current_line := ! current_line + 1 else (); c)); + fun put s = out_buffer := s :: ! out_buffer; + + fun exec () = + (case ! in_buffer of + [] => () + | _ => (PolyML.compilerEx (get, put, fn () => ! current_line, name) (); exec ())); + in + exec () handle exn => (error (output ()); raise exn); + if verbose then print (output ()) else () + end; + +fun use_file context verbose name = + let + val instream = TextIO.openIn name; + val txt = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream); + in use_text context (1, name) verbose txt end; diff -r 2261c8781f73 -r f20a61cec3d4 src/Pure/ML-Systems/compiler_polyml-5.2.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/ML-Systems/compiler_polyml-5.2.ML Sun May 31 22:00:56 2009 -0700 @@ -0,0 +1,51 @@ +(* Title: Pure/ML-Systems/compiler_polyml-5.2.ML + +Runtime compilation for Poly/ML 5.2 and 5.2.1. +*) + +local + +fun drop_newline s = + if String.isSuffix "\n" s then String.substring (s, 0, size s - 1) + else s; + +in + +fun use_text ({tune_source, name_space, str_of_pos, print, error, ...}: use_context) + (start_line, name) verbose txt = + let + val current_line = ref start_line; + val in_buffer = ref (String.explode (tune_source txt)); + val out_buffer = ref ([]: string list); + fun output () = drop_newline (implode (rev (! out_buffer))); + + fun get () = + (case ! in_buffer of + [] => NONE + | c :: cs => + (in_buffer := cs; if c = #"\n" then current_line := ! current_line + 1 else (); SOME c)); + fun put s = out_buffer := s :: ! out_buffer; + fun message (msg, is_err, line) = + (if is_err then "Error: " else "Warning: ") ^ drop_newline msg ^ str_of_pos line name ^ "\n"; + + val parameters = + [PolyML.Compiler.CPOutStream put, + PolyML.Compiler.CPLineNo (fn () => ! current_line), + PolyML.Compiler.CPErrorMessageProc (put o message), + PolyML.Compiler.CPNameSpace name_space]; + val _ = + (while not (List.null (! in_buffer)) do + PolyML.compiler (get, parameters) ()) + handle exn => + (put ("Exception- " ^ General.exnMessage exn ^ " raised"); + error (output ()); raise exn); + in if verbose then print (output ()) else () end; + +fun use_file context verbose name = + let + val instream = TextIO.openIn name; + val txt = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream); + in use_text context (1, name) verbose txt end; + +end; + diff -r 2261c8781f73 -r f20a61cec3d4 src/Pure/ML-Systems/compiler_polyml-5.3.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/ML-Systems/compiler_polyml-5.3.ML Sun May 31 22:00:56 2009 -0700 @@ -0,0 +1,55 @@ +(* Title: Pure/ML-Systems/compiler_polyml-5.3.ML + +Runtime compilation for Poly/ML 5.3 (SVN experimental). +*) + +local + +fun drop_newline s = + if String.isSuffix "\n" s then String.substring (s, 0, size s - 1) + else s; + +in + +fun use_text ({tune_source, name_space, str_of_pos, print, error, ...}: use_context) + (start_line, name) verbose txt = + let + val current_line = ref start_line; + val in_buffer = ref (String.explode (tune_source txt)); + val out_buffer = ref ([]: string list); + fun output () = drop_newline (implode (rev (! out_buffer))); + + fun get () = + (case ! in_buffer of + [] => NONE + | c :: cs => + (in_buffer := cs; if c = #"\n" then current_line := ! current_line + 1 else (); SOME c)); + fun put s = out_buffer := s :: ! out_buffer; + fun put_message {message = msg1, hard, location = {startLine = line, ...}, context} = + (put (if hard then "Error: " else "Warning: "); + PolyML.prettyPrint (put, 76) msg1; + (case context of NONE => () | SOME msg2 => PolyML.prettyPrint (put, 76) msg2); + put ("At" ^ str_of_pos line name ^ "\n")); + + val parameters = + [PolyML.Compiler.CPOutStream put, + PolyML.Compiler.CPLineNo (fn () => ! current_line), + PolyML.Compiler.CPErrorMessageProc put_message, + PolyML.Compiler.CPNameSpace name_space, + PolyML.Compiler.CPPrintInAlphabeticalOrder false]; + val _ = + (while not (List.null (! in_buffer)) do + PolyML.compiler (get, parameters) ()) + handle exn => + (put ("Exception- " ^ General.exnMessage exn ^ " raised"); + error (output ()); raise exn); + in if verbose then print (output ()) else () end; + +fun use_file context verbose name = + let + val instream = TextIO.openIn name; + val txt = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream); + in use_text context (1, name) verbose txt end; + +end; + diff -r 2261c8781f73 -r f20a61cec3d4 src/Pure/ML-Systems/install_pp_polyml-experimental.ML --- a/src/Pure/ML-Systems/install_pp_polyml-experimental.ML Sun May 31 21:59:33 2009 -0700 +++ b/src/Pure/ML-Systems/install_pp_polyml-experimental.ML Sun May 31 22:00:56 2009 -0700 @@ -1,18 +1,17 @@ (* Title: Pure/ML-Systems/install_pp_polyml-experimental.ML -Extra toplevel pretty-printing for Poly/ML; experimental version for -Poly/ML 5.3. +Extra toplevel pretty-printing for Poly/ML 5.3 (SVN experimental). *) -addPrettyPrinter (fn depth => fn pretty => fn x => +PolyML.addPrettyPrinter (fn depth => fn pretty => fn x => (case Future.peek x of - NONE => PrettyString "" - | SOME (Exn.Exn _) => PrettyString "" + NONE => PolyML.PrettyString "" + | SOME (Exn.Exn _) => PolyML.PrettyString "" | SOME (Exn.Result y) => pretty (y, depth))); -addPrettyPrinter (fn depth => fn pretty => fn x => +PolyML.addPrettyPrinter (fn depth => fn pretty => fn x => (case Lazy.peek x of - NONE => PrettyString "" - | SOME (Exn.Exn _) => PrettyString "" + NONE => PolyML.PrettyString "" + | SOME (Exn.Exn _) => PolyML.PrettyString "" | SOME (Exn.Result y) => pretty (y, depth))); diff -r 2261c8781f73 -r f20a61cec3d4 src/Pure/ML-Systems/install_pp_polyml.ML --- a/src/Pure/ML-Systems/install_pp_polyml.ML Sun May 31 21:59:33 2009 -0700 +++ b/src/Pure/ML-Systems/install_pp_polyml.ML Sun May 31 22:00:56 2009 -0700 @@ -3,15 +3,17 @@ Extra toplevel pretty-printing for Poly/ML. *) -install_pp (fn (str, _, _, _) => fn depth => fn (print: 'a * int -> unit) => fn (x: 'a future) => - (case Future.peek x of - NONE => str "" - | SOME (Exn.Exn _) => str "" - | SOME (Exn.Result y) => print (y, depth))); +PolyML.install_pp + (fn (str, _, _, _) => fn depth => fn (print: 'a * int -> unit) => fn (x: 'a future) => + (case Future.peek x of + NONE => str "" + | SOME (Exn.Exn _) => str "" + | SOME (Exn.Result y) => print (y, depth))); -install_pp (fn (str, _, _, _) => fn depth => fn (print: 'a * int -> unit) => fn (x: 'a lazy) => - (case Lazy.peek x of - NONE => str "" - | SOME (Exn.Exn _) => str "" - | SOME (Exn.Result y) => print (y, depth))); +PolyML.install_pp + (fn (str, _, _, _) => fn depth => fn (print: 'a * int -> unit) => fn (x: 'a lazy) => + (case Lazy.peek x of + NONE => str "" + | SOME (Exn.Exn _) => str "" + | SOME (Exn.Result y) => print (y, depth))); diff -r 2261c8781f73 -r f20a61cec3d4 src/Pure/ML-Systems/mosml.ML --- a/src/Pure/ML-Systems/mosml.ML Sun May 31 21:59:33 2009 -0700 +++ b/src/Pure/ML-Systems/mosml.ML Sun May 31 22:00:56 2009 -0700 @@ -132,8 +132,6 @@ (*dummy implementation*) fun exception_trace f = f (); -(*dummy implementation*) -fun print x = x; (** Compiler-independent timing functions **) diff -r 2261c8781f73 -r f20a61cec3d4 src/Pure/ML-Systems/multithreading_polyml.ML --- a/src/Pure/ML-Systems/multithreading_polyml.ML Sun May 31 21:59:33 2009 -0700 +++ b/src/Pure/ML-Systems/multithreading_polyml.ML Sun May 31 22:00:56 2009 -0700 @@ -1,7 +1,7 @@ (* Title: Pure/ML-Systems/multithreading_polyml.ML Author: Makarius -Multithreading in Poly/ML 5.2 or later (cf. polyml/basis/Thread.sml). +Multithreading in Poly/ML 5.2.1 or later (cf. polyml/basis/Thread.sml). *) signature MULTITHREADING_POLYML = diff -r 2261c8781f73 -r f20a61cec3d4 src/Pure/ML-Systems/polyml-4.1.3.ML --- a/src/Pure/ML-Systems/polyml-4.1.3.ML Sun May 31 21:59:33 2009 -0700 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,15 +0,0 @@ -(* Title: Pure/ML-Systems/polyml-4.1.3.ML - -Compatibility wrapper for Poly/ML 4.1.3. -*) - -use "ML-Systems/polyml_old_basis.ML"; -use "ML-Systems/universal.ML"; -use "ML-Systems/thread_dummy.ML"; -use "ML-Systems/ml_name_space.ML"; -use "ML-Systems/polyml_common.ML"; -use "ML-Systems/polyml_old_compiler4.ML"; -use "ML-Systems/polyml_pp.ML"; - -val pointer_eq = Address.wordEq; - diff -r 2261c8781f73 -r f20a61cec3d4 src/Pure/ML-Systems/polyml-4.1.4.ML --- a/src/Pure/ML-Systems/polyml-4.1.4.ML Sun May 31 21:59:33 2009 -0700 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,15 +0,0 @@ -(* Title: Pure/ML-Systems/polyml-4.1.4.ML - -Compatibility wrapper for Poly/ML 4.1.4. -*) - -use "ML-Systems/polyml_old_basis.ML"; -use "ML-Systems/universal.ML"; -use "ML-Systems/thread_dummy.ML"; -use "ML-Systems/ml_name_space.ML"; -use "ML-Systems/polyml_common.ML"; -use "ML-Systems/polyml_old_compiler4.ML"; -use "ML-Systems/polyml_pp.ML"; - -val pointer_eq = Address.wordEq; - diff -r 2261c8781f73 -r f20a61cec3d4 src/Pure/ML-Systems/polyml-4.2.0.ML --- a/src/Pure/ML-Systems/polyml-4.2.0.ML Sun May 31 21:59:33 2009 -0700 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,14 +0,0 @@ -(* Title: Pure/ML-Systems/polyml-4.2.0.ML - -Compatibility wrapper for Poly/ML 4.2.0. -*) - -use "ML-Systems/universal.ML"; -use "ML-Systems/thread_dummy.ML"; -use "ML-Systems/ml_name_space.ML"; -use "ML-Systems/polyml_common.ML"; -use "ML-Systems/polyml_old_compiler4.ML"; -use "ML-Systems/polyml_pp.ML"; - -val pointer_eq = Address.wordEq; - diff -r 2261c8781f73 -r f20a61cec3d4 src/Pure/ML-Systems/polyml-5.0.ML --- a/src/Pure/ML-Systems/polyml-5.0.ML Sun May 31 21:59:33 2009 -0700 +++ b/src/Pure/ML-Systems/polyml-5.0.ML Sun May 31 22:00:56 2009 -0700 @@ -7,8 +7,8 @@ use "ML-Systems/thread_dummy.ML"; use "ML-Systems/ml_name_space.ML"; use "ML-Systems/polyml_common.ML"; -use "ML-Systems/polyml_old_compiler5.ML"; -use "ML-Systems/polyml_pp.ML"; +use "ML-Systems/compiler_polyml-5.0.ML"; +use "ML-Systems/pp_polyml.ML"; val pointer_eq = PolyML.pointerEq; diff -r 2261c8781f73 -r f20a61cec3d4 src/Pure/ML-Systems/polyml-5.1.ML --- a/src/Pure/ML-Systems/polyml-5.1.ML Sun May 31 21:59:33 2009 -0700 +++ b/src/Pure/ML-Systems/polyml-5.1.ML Sun May 31 22:00:56 2009 -0700 @@ -6,8 +6,8 @@ use "ML-Systems/thread_dummy.ML"; use "ML-Systems/ml_name_space.ML"; use "ML-Systems/polyml_common.ML"; -use "ML-Systems/polyml_old_compiler5.ML"; -use "ML-Systems/polyml_pp.ML"; +use "ML-Systems/compiler_polyml-5.0.ML"; +use "ML-Systems/pp_polyml.ML"; val pointer_eq = PolyML.pointerEq; diff -r 2261c8781f73 -r f20a61cec3d4 src/Pure/ML-Systems/polyml-experimental.ML --- a/src/Pure/ML-Systems/polyml-experimental.ML Sun May 31 21:59:33 2009 -0700 +++ b/src/Pure/ML-Systems/polyml-experimental.ML Sun May 31 22:00:56 2009 -0700 @@ -1,6 +1,6 @@ -(* Title: Pure/ML-Systems/polyml.ML +(* Title: Pure/ML-Systems/polyml-experimental.ML -Compatibility wrapper for experimental versions of Poly/ML after 5.2.1. +Compatibility wrapper for Poly/ML 5.3 (SVN experimental). *) open Thread; @@ -19,92 +19,42 @@ fun share_common_data () = PolyML.shareCommonData PolyML.rootFunction; - -(* runtime compilation *) - -local - -fun drop_newline s = - if String.isSuffix "\n" s then String.substring (s, 0, size s - 1) - else s; - -in - -fun use_text ({tune_source, name_space, str_of_pos, print, error, ...}: use_context) - (start_line, name) verbose txt = - let - val current_line = ref start_line; - val in_buffer = ref (String.explode (tune_source txt)); - val out_buffer = ref ([]: string list); - fun output () = drop_newline (implode (rev (! out_buffer))); - - fun get () = - (case ! in_buffer of - [] => NONE - | c :: cs => - (in_buffer := cs; if c = #"\n" then current_line := ! current_line + 1 else (); SOME c)); - fun put s = out_buffer := s :: ! out_buffer; - fun put_message {message = msg1, hard, location = {startLine = line, ...}, context} = - (put (if hard then "Error: " else "Warning: "); - PolyML.prettyPrint (put, 76) msg1; - (case context of NONE => () | SOME msg2 => PolyML.prettyPrint (put, 76) msg2); - put ("At" ^ str_of_pos line name ^ "\n")); - - val parameters = - [PolyML.Compiler.CPOutStream put, - PolyML.Compiler.CPLineNo (fn () => ! current_line), - PolyML.Compiler.CPErrorMessageProc put_message, - PolyML.Compiler.CPNameSpace name_space, - PolyML.Compiler.CPPrintInAlphabeticalOrder false]; - val _ = - (while not (List.null (! in_buffer)) do - PolyML.compiler (get, parameters) ()) - handle exn => - (put ("Exception- " ^ General.exnMessage exn ^ " raised"); - error (output ()); raise exn); - in if verbose then print (output ()) else () end; - -fun use_file context verbose name = - let - val instream = TextIO.openIn name; - val txt = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream); - in use_text context (1, name) verbose txt end; - -end; +use "ML-Systems/compiler_polyml-5.3.ML"; (* toplevel pretty printing *) val pretty_ml = let - fun convert len (PrettyBlock (ind, _, context, prts)) = + fun convert len (PolyML.PrettyBlock (ind, _, context, prts)) = let fun property name default = - (case List.find (fn ContextProperty (a, _) => name = a | _ => false) context of - SOME (ContextProperty (_, b)) => b + (case List.find (fn PolyML.ContextProperty (a, _) => name = a | _ => false) context of + SOME (PolyML.ContextProperty (_, b)) => b | NONE => default); val bg = property "begin" ""; val en = property "end" ""; val len' = property "length" len; in ML_Pretty.Block ((bg, en), map (convert len') prts, ind) end - | convert len (PrettyString s) = + | convert len (PolyML.PrettyString s) = ML_Pretty.String (s, case Int.fromString len of SOME i => i | NONE => size s) - | convert _ (PrettyBreak (wd, _)) = + | convert _ (PolyML.PrettyBreak (wd, _)) = ML_Pretty.Break (if wd < 99999 then (false, wd) else (true, 2)); in convert "" end; fun ml_pretty (ML_Pretty.Block ((bg, en), prts, ind)) = let val context = - (if bg = "" then [] else [ContextProperty ("begin", bg)]) @ - (if en = "" then [] else [ContextProperty ("end", en)]) - in PrettyBlock (ind, false, context, map ml_pretty prts) end + (if bg = "" then [] else [PolyML.ContextProperty ("begin", bg)]) @ + (if en = "" then [] else [PolyML.ContextProperty ("end", en)]) + in PolyML.PrettyBlock (ind, false, context, map ml_pretty prts) end | ml_pretty (ML_Pretty.String (s, len)) = - if len = size s then PrettyString s - else PrettyBlock (0, false, [ContextProperty ("length", Int.toString len)], [PrettyString s]) - | ml_pretty (ML_Pretty.Break (false, wd)) = PrettyBreak (wd, 0) - | ml_pretty (ML_Pretty.Break (true, _)) = PrettyBreak (99999, 0); + if len = size s then PolyML.PrettyString s + else PolyML.PrettyBlock + (0, false, [PolyML.ContextProperty ("length", Int.toString len)], [PolyML.PrettyString s]) + | ml_pretty (ML_Pretty.Break (false, wd)) = PolyML.PrettyBreak (wd, 0) + | ml_pretty (ML_Pretty.Break (true, _)) = PolyML.PrettyBreak (99999, 0); fun toplevel_pp context (_: string list) pp = use_text context (1, "pp") false - ("addPrettyPrinter (fn _ => fn _ => ml_pretty o Pretty.to_ML o (" ^ pp ^ "))"); + ("PolyML.addPrettyPrinter (fn _ => fn _ => ml_pretty o Pretty.to_ML o (" ^ pp ^ "))"); diff -r 2261c8781f73 -r f20a61cec3d4 src/Pure/ML-Systems/polyml.ML --- a/src/Pure/ML-Systems/polyml.ML Sun May 31 21:59:33 2009 -0700 +++ b/src/Pure/ML-Systems/polyml.ML Sun May 31 22:00:56 2009 -0700 @@ -1,6 +1,6 @@ (* Title: Pure/ML-Systems/polyml.ML -Compatibility wrapper for Poly/ML 5.2 or later. +Compatibility wrapper for Poly/ML 5.2 and 5.2.1. *) open Thread; @@ -22,54 +22,6 @@ fun share_common_data () = PolyML.shareCommonData PolyML.rootFunction; - -(* runtime compilation *) - -local - -fun drop_newline s = - if String.isSuffix "\n" s then String.substring (s, 0, size s - 1) - else s; - -in - -fun use_text ({tune_source, name_space, str_of_pos, print, error, ...}: use_context) - (start_line, name) verbose txt = - let - val current_line = ref start_line; - val in_buffer = ref (String.explode (tune_source txt)); - val out_buffer = ref ([]: string list); - fun output () = drop_newline (implode (rev (! out_buffer))); +use "ML-Systems/compiler_polyml-5.2.ML"; +use "ML-Systems/pp_polyml.ML"; - fun get () = - (case ! in_buffer of - [] => NONE - | c :: cs => - (in_buffer := cs; if c = #"\n" then current_line := ! current_line + 1 else (); SOME c)); - fun put s = out_buffer := s :: ! out_buffer; - fun message (msg, is_err, line) = - (if is_err then "Error: " else "Warning: ") ^ drop_newline msg ^ str_of_pos line name ^ "\n"; - - val parameters = - [PolyML.Compiler.CPOutStream put, - PolyML.Compiler.CPLineNo (fn () => ! current_line), - PolyML.Compiler.CPErrorMessageProc (put o message), - PolyML.Compiler.CPNameSpace name_space]; - val _ = - (while not (List.null (! in_buffer)) do - PolyML.compiler (get, parameters) ()) - handle exn => - (put ("Exception- " ^ General.exnMessage exn ^ " raised"); - error (output ()); raise exn); - in if verbose then print (output ()) else () end; - -fun use_file context verbose name = - let - val instream = TextIO.openIn name; - val txt = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream); - in use_text context (1, name) verbose txt end; - -end; - -use "ML-Systems/polyml_pp.ML"; - diff -r 2261c8781f73 -r f20a61cec3d4 src/Pure/ML-Systems/polyml_common.ML --- a/src/Pure/ML-Systems/polyml_common.ML Sun May 31 21:59:33 2009 -0700 +++ b/src/Pure/ML-Systems/polyml_common.ML Sun May 31 22:00:56 2009 -0700 @@ -1,6 +1,6 @@ (* Title: Pure/ML-Systems/polyml_common.ML -Compatibility file for Poly/ML -- common part for 4.x and 5.x. +Compatibility file for Poly/ML -- common part for 5.x. *) exception Interrupt = SML90.Interrupt; @@ -28,13 +28,7 @@ (* old Poly/ML emulation *) -local - val orig_exit = exit; -in - open PolyML; - val exit = orig_exit; - fun quit () = exit 0; -end; +fun quit () = exit 0; (* restore old-style character / string functions *) @@ -83,6 +77,8 @@ fun print_depth n = (depth := n; PolyML.print_depth n); end; +val error_depth = PolyML.error_depth; + (** interrupts **) @@ -134,7 +130,12 @@ | SOME txt => txt); -(* profile execution *) + +(** Runtime system **) + +val exception_trace = PolyML.exception_trace; +val timing = PolyML.timing; +val profiling = PolyML.profiling; fun profile 0 f x = f x | profile n f x = diff -r 2261c8781f73 -r f20a61cec3d4 src/Pure/ML-Systems/polyml_old_basis.ML --- a/src/Pure/ML-Systems/polyml_old_basis.ML Sun May 31 21:59:33 2009 -0700 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,29 +0,0 @@ -(* Title: Pure/ML-Systems/polyml_old_basis.ML - -Fixes for the old SML basis library (before Poly/ML 4.2.0). -*) - -structure String = -struct - fun isSuffix s1 s2 = - let val n1 = size s1 and n2 = size s2 - in if n1 = n2 then s1 = s2 else n1 <= n2 andalso String.substring (s2, n2 - n1, n1) = s1 end; - fun isSubstring s1 s2 = - String.isPrefix s1 s2 orelse - size s1 < size s2 andalso isSubstring s1 (String.extract (s2, 1, NONE)); - open String; -end; - -structure Substring = -struct - open Substring; - val full = all; -end; - -structure TextIO = -struct - open TextIO; - fun inputLine is = - let val s = TextIO.inputLine is - in if s = "" then NONE else SOME s end; -end; diff -r 2261c8781f73 -r f20a61cec3d4 src/Pure/ML-Systems/polyml_old_compiler4.ML --- a/src/Pure/ML-Systems/polyml_old_compiler4.ML Sun May 31 21:59:33 2009 -0700 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,32 +0,0 @@ -(* Title: Pure/ML-Systems/polyml_old_compiler4.ML - -Runtime compilation -- for old PolyML.compiler (version 4.x). -*) - -fun use_text ({tune_source, print, error, ...}: use_context) (line: int, name) verbose txt = - let - val in_buffer = ref (explode (tune_source txt)); - val out_buffer = ref ([]: string list); - fun output () = implode (rev (case ! out_buffer of "\n" :: cs => cs | cs => cs)); - - fun get () = - (case ! in_buffer of - [] => "" - | c :: cs => (in_buffer := cs; c)); - fun put s = out_buffer := s :: ! out_buffer; - - fun exec () = - (case ! in_buffer of - [] => () - | _ => (PolyML.compiler (get, put) (); exec ())); - in - exec () handle exn => - (error ((if name = "" then "" else "Error in " ^ name ^ "\n") ^ output ()); raise exn); - if verbose then print (output ()) else () - end; - -fun use_file context verbose name = - let - val instream = TextIO.openIn name; - val txt = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream); - in use_text context (1, name) verbose txt end; diff -r 2261c8781f73 -r f20a61cec3d4 src/Pure/ML-Systems/polyml_old_compiler5.ML --- a/src/Pure/ML-Systems/polyml_old_compiler5.ML Sun May 31 21:59:33 2009 -0700 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,32 +0,0 @@ -(* Title: Pure/ML-Systems/polyml_old_compiler5.ML - -Runtime compilation -- for old PolyML.compilerEx (version 5.0, 5.1). -*) - -fun use_text ({tune_source, print, error, ...}: use_context) (line, name) verbose txt = - let - val in_buffer = ref (explode (tune_source txt)); - val out_buffer = ref ([]: string list); - fun output () = implode (rev (case ! out_buffer of "\n" :: cs => cs | cs => cs)); - - val current_line = ref line; - fun get () = - (case ! in_buffer of - [] => "" - | c :: cs => (in_buffer := cs; if c = "\n" then current_line := ! current_line + 1 else (); c)); - fun put s = out_buffer := s :: ! out_buffer; - - fun exec () = - (case ! in_buffer of - [] => () - | _ => (PolyML.compilerEx (get, put, fn () => ! current_line, name) (); exec ())); - in - exec () handle exn => (error (output ()); raise exn); - if verbose then print (output ()) else () - end; - -fun use_file context verbose name = - let - val instream = TextIO.openIn name; - val txt = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream); - in use_text context (1, name) verbose txt end; diff -r 2261c8781f73 -r f20a61cec3d4 src/Pure/ML-Systems/polyml_pp.ML --- a/src/Pure/ML-Systems/polyml_pp.ML Sun May 31 21:59:33 2009 -0700 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,20 +0,0 @@ -(* Title: Pure/ML-Systems/polyml_pp.ML - -Toplevel pretty printing for Poly/ML before 5.3. -*) - -fun ml_pprint (print, begin_blk, brk, end_blk) = - let - fun str "" = () - | str s = print s; - fun pprint (ML_Pretty.Block ((bg, en), prts, ind)) = - (str bg; begin_blk (ind, false); List.app pprint prts; end_blk (); str en) - | pprint (ML_Pretty.String (s, _)) = str s - | pprint (ML_Pretty.Break (false, wd)) = brk (wd, 0) - | pprint (ML_Pretty.Break (true, _)) = brk (99999, 0); - in pprint end; - -fun toplevel_pp context (_: string list) pp = - use_text context (1, "pp") false - ("install_pp (fn args => fn _ => fn _ => ml_pprint args o Pretty.to_ML o (" ^ pp ^ "))"); - diff -r 2261c8781f73 -r f20a61cec3d4 src/Pure/ML-Systems/pp_polyml.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/ML-Systems/pp_polyml.ML Sun May 31 22:00:56 2009 -0700 @@ -0,0 +1,20 @@ +(* Title: Pure/ML-Systems/pp_polyml.ML + +Toplevel pretty printing for Poly/ML before 5.3. +*) + +fun ml_pprint (print, begin_blk, brk, end_blk) = + let + fun str "" = () + | str s = print s; + fun pprint (ML_Pretty.Block ((bg, en), prts, ind)) = + (str bg; begin_blk (ind, false); List.app pprint prts; end_blk (); str en) + | pprint (ML_Pretty.String (s, _)) = str s + | pprint (ML_Pretty.Break (false, wd)) = brk (wd, 0) + | pprint (ML_Pretty.Break (true, _)) = brk (99999, 0); + in pprint end; + +fun toplevel_pp context (_: string list) pp = + use_text context (1, "pp") false + ("PolyML.install_pp (fn args => fn _ => fn _ => ml_pprint args o Pretty.to_ML o (" ^ pp ^ "))"); + diff -r 2261c8781f73 -r f20a61cec3d4 src/Pure/ML-Systems/smlnj.ML --- a/src/Pure/ML-Systems/smlnj.ML Sun May 31 21:59:33 2009 -0700 +++ b/src/Pure/ML-Systems/smlnj.ML Sun May 31 22:00:56 2009 -0700 @@ -92,12 +92,6 @@ (*dummy implementation*) fun exception_trace f = f (); -(*dummy implementation*) -fun print x = x; - -(*dummy implementation*) -fun makestring x = "dummy string for SML New Jersey"; - (* ML command execution *) diff -r 2261c8781f73 -r f20a61cec3d4 src/Pure/ML/ml_test.ML --- a/src/Pure/ML/ml_test.ML Sun May 31 21:59:33 2009 -0700 +++ b/src/Pure/ML/ml_test.ML Sun May 31 22:00:56 2009 -0700 @@ -35,7 +35,7 @@ in (regs, context') end; fun position_of ctxt - ({file, startLine = line, startPosition = i, endPosition = j, ...}: location) = + ({file, startLine = line, startPosition = i, endPosition = j, ...}: PolyML.location) = (case pairself (Inttab.lookup (Extra_Env.get (Context.Proof ctxt))) (i, j) of (SOME pos1, SOME pos2) => Position.encode_range (pos1, pos2) | (SOME pos, NONE) => pos @@ -47,15 +47,15 @@ fun report_parse_tree context depth space = let val pos_of = position_of (Context.proof_of context); - fun report loc (PTtype types) = + fun report loc (PolyML.PTtype types) = PolyML.NameSpace.displayTypeExpression (types, depth, space) |> pretty_ml |> Pretty.from_ML |> Pretty.string_of |> Position.report_text Markup.ML_typing (pos_of loc) - | report loc (PTdeclaredAt decl) = + | report loc (PolyML.PTdeclaredAt decl) = Markup.markup (Markup.properties (Position.properties_of (pos_of decl)) Markup.ML_def) "" |> Position.report_text Markup.ML_ref (pos_of loc) - | report _ (PTnextSibling tree) = report_tree (tree ()) - | report _ (PTfirstChild tree) = report_tree (tree ()) + | report _ (PolyML.PTnextSibling tree) = report_tree (tree ()) + | report _ (PolyML.PTfirstChild tree) = report_tree (tree ()) | report _ _ = () and report_tree (loc, props) = List.app (report loc) props; in report_tree end; diff -r 2261c8781f73 -r f20a61cec3d4 src/Pure/meta_simplifier.ML --- a/src/Pure/meta_simplifier.ML Sun May 31 21:59:33 2009 -0700 +++ b/src/Pure/meta_simplifier.ML Sun May 31 22:00:56 2009 -0700 @@ -158,11 +158,6 @@ Thm.eq_thm_prop (thm1, thm2); -(* congruences *) - -val eq_cong = Thm.eq_thm_prop - - (* simplification sets, procedures, and solvers *) (*A simpset contains data required during conversion: @@ -785,7 +780,7 @@ val prems' = merge Thm.eq_thm_prop (prems1, prems2); val bounds' = if #1 bounds1 < #1 bounds2 then bounds2 else bounds1; val depth' = if #1 depth1 < #1 depth2 then depth2 else depth1; - val congs' = merge (eq_cong o pairself #2) (congs1, congs2); + val congs' = merge (Thm.eq_thm_prop o pairself #2) (congs1, congs2); val weak' = merge (op =) (weak1, weak2); val procs' = Net.merge eq_proc (procs1, procs2); val loop_tacs' = AList.merge (op =) (K true) (loop_tacs1, loop_tacs2); diff -r 2261c8781f73 -r f20a61cec3d4 src/Pure/mk --- a/src/Pure/mk Sun May 31 21:59:33 2009 -0700 +++ b/src/Pure/mk Sun May 31 22:00:56 2009 -0700 @@ -114,7 +114,7 @@ -e "val ml_platform = \"$ML_PLATFORM\";" \ -e "(use\"$COMPAT\"; use\"ROOT.ML\") handle _ => exit 1;" \ -e "ml_prompts \"ML> \" \"ML# \";" \ - -f -c -q -w RAW_ML_SYSTEM Pure > "$LOG" 2>&1 + -f -q -w RAW_ML_SYSTEM Pure > "$LOG" 2>&1 RC="$?" fi diff -r 2261c8781f73 -r f20a61cec3d4 src/Pure/simplifier.ML --- a/src/Pure/simplifier.ML Sun May 31 21:59:33 2009 -0700 +++ b/src/Pure/simplifier.ML Sun May 31 22:00:56 2009 -0700 @@ -348,16 +348,7 @@ -(** proof methods **) - -(* simplification *) - -val simp_options = - (Args.parens (Args.$$$ no_asmN) >> K simp_tac || - Args.parens (Args.$$$ no_asm_simpN) >> K asm_simp_tac || - Args.parens (Args.$$$ no_asm_useN) >> K full_simp_tac || - Args.parens (Args.$$$ asm_lrN) >> K asm_lr_simp_tac || - Scan.succeed asm_full_simp_tac); +(** method syntax **) val cong_modifiers = [Args.$$$ congN -- Args.colon >> K ((I, cong_add): Method.modifier), @@ -379,25 +370,33 @@ >> K (Context.proof_map (map_ss MetaSimplifier.clear_ss), simp_add)] @ cong_modifiers; -fun simp_args more_mods = - Method.sectioned_args (Args.bang_facts -- Scan.lift simp_options) - (more_mods @ simp_modifiers'); +val simp_options = + (Args.parens (Args.$$$ no_asmN) >> K simp_tac || + Args.parens (Args.$$$ no_asm_simpN) >> K asm_simp_tac || + Args.parens (Args.$$$ no_asm_useN) >> K full_simp_tac || + Args.parens (Args.$$$ asm_lrN) >> K asm_lr_simp_tac || + Scan.succeed asm_full_simp_tac); -fun simp_method (prems, tac) ctxt = METHOD (fn facts => - ALLGOALS (Method.insert_tac (prems @ facts)) THEN - (CHANGED_PROP o ALLGOALS o tac) (local_simpset_of ctxt)); - -fun simp_method' (prems, tac) ctxt = METHOD (fn facts => - HEADGOAL (Method.insert_tac (prems @ facts) THEN' - ((CHANGED_PROP) oo tac) (local_simpset_of ctxt))); +fun simp_method more_mods meth = + Args.bang_facts -- Scan.lift simp_options --| + Method.sections (more_mods @ simp_modifiers') >> + (fn (prems, tac) => fn ctxt => METHOD (fn facts => meth ctxt tac (prems @ facts))); (** setup **) -fun method_setup more_mods = Method.add_methods - [(simpN, simp_args more_mods simp_method', "simplification"), - ("simp_all", simp_args more_mods simp_method, "simplification (all goals)")]; +fun method_setup more_mods = + Method.setup (Binding.name simpN) + (simp_method more_mods (fn ctxt => fn tac => fn facts => + HEADGOAL (Method.insert_tac facts THEN' + (CHANGED_PROP oo tac) (local_simpset_of ctxt)))) + "simplification" #> + Method.setup (Binding.name "simp_all") + (simp_method more_mods (fn ctxt => fn tac => fn facts => + ALLGOALS (Method.insert_tac facts) THEN + (CHANGED_PROP o ALLGOALS o tac) (local_simpset_of ctxt))) + "simplification (all goals)"; fun easy_setup reflect trivs = method_setup [] #> Context.theory_map (map_ss (fn _ => let diff -r 2261c8781f73 -r f20a61cec3d4 src/Tools/Compute_Oracle/am_sml.ML --- a/src/Tools/Compute_Oracle/am_sml.ML Sun May 31 21:59:33 2009 -0700 +++ b/src/Tools/Compute_Oracle/am_sml.ML Sun May 31 22:00:56 2009 -0700 @@ -320,7 +320,7 @@ val strict_args = (case toplevel_arity_of c of NONE => the (arity_of c) | SOME sa => sa) val xs = map (fn n => if n < strict_args then "x"^(str n) else "x"^(str n)^"()") rightargs val right = (indexed "C" c)^" "^(string_of_tuple xs) - val message = "(\"unresolved lazy call: "^(string_of_int c)^", \"^(makestring x"^(string_of_int (strict_args - 1))^"))" + val message = "(\"unresolved lazy call: " ^ string_of_int c ^ "\")" val right = if strict_args < the (arity_of c) then "raise AM_SML.Run "^message else right in (indexed "c" c)^(if gnum > 0 then "_"^(str gnum) else "")^leftargs^" = "^right diff -r 2261c8781f73 -r f20a61cec3d4 src/Tools/Compute_Oracle/compute.ML --- a/src/Tools/Compute_Oracle/compute.ML Sun May 31 21:59:33 2009 -0700 +++ b/src/Tools/Compute_Oracle/compute.ML Sun May 31 22:00:56 2009 -0700 @@ -379,7 +379,11 @@ fun has_witness s = not (null (Sign.witness_sorts thy [] [s])) val shyptab = fold Sorttab.delete (filter has_witness (Sorttab.keys (shyptab))) shyptab val shyps = if Sorttab.is_empty shyptab then [] else Sorttab.keys (fold delete_term (prop::hyps) shyptab) - val _ = if not (null shyps) then raise Compute ("dangling sort hypotheses: "^(makestring shyps)) else () + val _ = + if not (null shyps) then + raise Compute ("dangling sort hypotheses: " ^ + commas (map (Syntax.string_of_sort_global thy) shyps)) + else () in Thm.cterm_of thy (fold_rev (fn hyp => fn p => Logic.mk_implies (hyp, p)) hyps prop) end))); @@ -610,7 +614,8 @@ case match_aterms varsubst b' a' of NONE => let - fun mk s = makestring (infer_types (naming_of computer) (encoding_of computer) ty s) + fun mk s = Syntax.string_of_term_global Pure.thy + (infer_types (naming_of computer) (encoding_of computer) ty s) val left = "computed left side: "^(mk a') val right = "computed right side: "^(mk b') in diff -r 2261c8781f73 -r f20a61cec3d4 src/Tools/eqsubst.ML --- a/src/Tools/eqsubst.ML Sun May 31 21:59:33 2009 -0700 +++ b/src/Tools/eqsubst.ML Sun May 31 22:00:56 2009 -0700 @@ -20,25 +20,25 @@ * Zipper.T (* focusterm to search under *) exception eqsubst_occL_exp of - string * int list * Thm.thm list * int * Thm.thm + string * int list * thm list * int * thm (* low level substitution functions *) val apply_subst_in_asm : int -> - Thm.thm -> - Thm.thm -> - (Thm.cterm list * int * 'a * Thm.thm) * match -> Thm.thm Seq.seq + thm -> + thm -> + (cterm list * int * 'a * thm) * match -> thm Seq.seq val apply_subst_in_concl : int -> - Thm.thm -> - Thm.cterm list * Thm.thm -> - Thm.thm -> match -> Thm.thm Seq.seq + thm -> + cterm list * thm -> + thm -> match -> thm Seq.seq (* matching/unification within zippers *) val clean_match_z : - Context.theory -> Term.term -> Zipper.T -> match option + theory -> term -> Zipper.T -> match option val clean_unify_z : - Context.theory -> int -> Term.term -> Zipper.T -> match Seq.seq + theory -> int -> term -> Zipper.T -> match Seq.seq (* skipping things in seq seq's *) @@ -57,65 +57,64 @@ (* tactics *) val eqsubst_asm_tac : Proof.context -> - int list -> Thm.thm list -> int -> Thm.thm -> Thm.thm Seq.seq + int list -> thm list -> int -> tactic val eqsubst_asm_tac' : Proof.context -> - (searchinfo -> int -> Term.term -> match skipseq) -> - int -> Thm.thm -> int -> Thm.thm -> Thm.thm Seq.seq + (searchinfo -> int -> term -> match skipseq) -> + int -> thm -> int -> tactic val eqsubst_tac : Proof.context -> int list -> (* list of occurences to rewrite, use [0] for any *) - Thm.thm list -> int -> Thm.thm -> Thm.thm Seq.seq + thm list -> int -> tactic val eqsubst_tac' : Proof.context -> (* proof context *) - (searchinfo -> Term.term -> match Seq.seq) (* search function *) - -> Thm.thm (* equation theorem to rewrite with *) + (searchinfo -> term -> match Seq.seq) (* search function *) + -> thm (* equation theorem to rewrite with *) -> int (* subgoal number in goal theorem *) - -> Thm.thm (* goal theorem *) - -> Thm.thm Seq.seq (* rewritten goal theorem *) + -> thm (* goal theorem *) + -> thm Seq.seq (* rewritten goal theorem *) val fakefree_badbounds : - (string * Term.typ) list -> - Term.term -> - (string * Term.typ) list * (string * Term.typ) list * Term.term + (string * typ) list -> + term -> + (string * typ) list * (string * typ) list * term val mk_foo_match : - (Term.term -> Term.term) -> - ('a * Term.typ) list -> Term.term -> Term.term + (term -> term) -> + ('a * typ) list -> term -> term (* preparing substitution *) - val prep_meta_eq : Proof.context -> Thm.thm -> Thm.thm list + val prep_meta_eq : Proof.context -> thm -> thm list val prep_concl_subst : - int -> Thm.thm -> (Thm.cterm list * Thm.thm) * searchinfo + int -> thm -> (cterm list * thm) * searchinfo val prep_subst_in_asm : - int -> Thm.thm -> int -> - (Thm.cterm list * int * int * Thm.thm) * searchinfo + int -> thm -> int -> + (cterm list * int * int * thm) * searchinfo val prep_subst_in_asms : - int -> Thm.thm -> - ((Thm.cterm list * int * int * Thm.thm) * searchinfo) list + int -> thm -> + ((cterm list * int * int * thm) * searchinfo) list val prep_zipper_match : - Zipper.T -> Term.term * ((string * Term.typ) list * (string * Term.typ) list * Term.term) + Zipper.T -> term * ((string * typ) list * (string * typ) list * term) (* search for substitutions *) val valid_match_start : Zipper.T -> bool val search_lr_all : Zipper.T -> Zipper.T Seq.seq val search_lr_valid : (Zipper.T -> bool) -> Zipper.T -> Zipper.T Seq.seq val searchf_lr_unify_all : - searchinfo -> Term.term -> match Seq.seq Seq.seq + searchinfo -> term -> match Seq.seq Seq.seq val searchf_lr_unify_valid : - searchinfo -> Term.term -> match Seq.seq Seq.seq + searchinfo -> term -> match Seq.seq Seq.seq val searchf_bt_unify_valid : - searchinfo -> Term.term -> match Seq.seq Seq.seq + searchinfo -> term -> match Seq.seq Seq.seq (* syntax tools *) val ith_syntax : int list parser val options_syntax : bool parser (* Isar level hooks *) - val eqsubst_asm_meth : Proof.context -> int list -> Thm.thm list -> Proof.method - val eqsubst_meth : Proof.context -> int list -> Thm.thm list -> Proof.method - val subst_meth : Method.src -> Proof.context -> Proof.method + val eqsubst_asm_meth : Proof.context -> int list -> thm list -> Proof.method + val eqsubst_meth : Proof.context -> int list -> thm list -> Proof.method val setup : theory -> theory end; @@ -560,15 +559,13 @@ Scan.optional (Args.parens (Scan.repeat OuterParse.nat)) [0]; (* combination method that takes a flag (true indicates that subst -should be done to an assumption, false = apply to the conclusion of -the goal) as well as the theorems to use *) -fun subst_meth src = - Method.syntax ((Scan.lift options_syntax) -- (Scan.lift ith_syntax) -- Attrib.thms) src - #> (fn (((asmflag, occL), inthms), ctxt) => - (if asmflag then eqsubst_asm_meth else eqsubst_meth) ctxt occL inthms); - - + should be done to an assumption, false = apply to the conclusion of + the goal) as well as the theorems to use *) val setup = - Method.add_method ("subst", subst_meth, "single-step substitution"); + Method.setup @{binding subst} + (Scan.lift (options_syntax -- ith_syntax) -- Attrib.thms >> + (fn ((asmflag, occL), inthms) => fn ctxt => + (if asmflag then eqsubst_asm_meth else eqsubst_meth) ctxt occL inthms)) + "single-step substitution"; end; diff -r 2261c8781f73 -r f20a61cec3d4 src/Tools/intuitionistic.ML --- a/src/Tools/intuitionistic.ML Sun May 31 21:59:33 2009 -0700 +++ b/src/Tools/intuitionistic.ML Sun May 31 22:00:56 2009 -0700 @@ -7,7 +7,7 @@ signature INTUITIONISTIC = sig val prover_tac: Proof.context -> int option -> int -> tactic - val method_setup: bstring -> theory -> theory + val method_setup: binding -> theory -> theory end; structure Intuitionistic: INTUITIONISTIC = @@ -84,15 +84,16 @@ modifier introN Args.colon (Scan.succeed ()) ContextRules.intro, Args.del -- Args.colon >> K (I, ContextRules.rule_del)]; -val method = - Method.bang_sectioned_args' modifiers (Scan.lift (Scan.option OuterParse.nat)) - (fn n => fn prems => fn ctxt => METHOD (fn facts => - HEADGOAL (Method.insert_tac (prems @ facts) THEN' - ObjectLogic.atomize_prems_tac THEN' prover_tac ctxt n))); - in -fun method_setup name = Method.add_method (name, method, "intuitionistic proof search"); +fun method_setup name = + Method.setup name + (Args.bang_facts -- Scan.lift (Scan.option OuterParse.nat) --| + Method.sections modifiers >> + (fn (prems, n) => fn ctxt => METHOD (fn facts => + HEADGOAL (Method.insert_tac (prems @ facts) THEN' + ObjectLogic.atomize_prems_tac THEN' prover_tac ctxt n)))) + "intuitionistic proof search"; end;