--- a/Admin/Release/CHECKLIST Sun Feb 28 21:19:58 2016 +0100
+++ b/Admin/Release/CHECKLIST Sun Feb 28 21:20:11 2016 +0100
@@ -12,7 +12,7 @@
- test "#!/usr/bin/env isabelle_scala_script";
- check sources:
- isabelle java isabelle.Check_Source '~~' '$AFP_BASE'
+ isabelle check_sources '~~' '$AFP_BASE'
- check ANNOUNCE, README, NEWS, COPYRIGHT, CONTRIBUTORS;
--- a/Admin/isatest/isatest-makedist Sun Feb 28 21:19:58 2016 +0100
+++ b/Admin/isatest/isatest-makedist Sun Feb 28 21:20:11 2016 +0100
@@ -102,10 +102,7 @@
$SSH lxbroy10 "$MAKEALL -x HOL-Proofs $HOME/settings/at64-poly"
sleep 15
-$SSH lxbroy4 "
- $MAKEALL -l HOL-Library $HOME/settings/at-poly;
- $MAKEALL -l HOL-Library $HOME/settings/at-poly-e;
- $MAKEALL $HOME/settings/at-poly-test"
+$SSH lxbroy4 "$MAKEALL -l HOL-Library $HOME/settings/at-poly"
sleep 15
$SSH macbroy2 "
$MAKEALL $HOME/settings/mac-poly64-M4;
@@ -115,11 +112,9 @@
$MAKEALL $HOME/settings/mac-poly-M8-skip_proofs;
$MAKEALL $HOME/settings/mac-poly-M8-quick_and_dirty"
sleep 15
-$SSH macbroy30 "
- $MAKEALL $HOME/settings/mac-poly-M2;
- $MAKEALL $HOME/settings/mac-poly64-M2"
+$SSH macbroy30 "$MAKEALL $HOME/settings/mac-poly-M2"
sleep 15
-$SSH macbroy31 "$MAKEALL $HOME/settings/mac-poly-M2-alternative"
+$SSH macbroy31 "$MAKEALL $MAKEALL $HOME/settings/mac-poly64-M2"
echo ------------------- spawned tests successfully --- `date` --- $HOSTNAME >> $DISTLOG 2>&1
--- a/Admin/isatest/settings/at-poly-e Sun Feb 28 21:19:58 2016 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,30 +0,0 @@
-# -*- shell-script -*- :mode=shellscript:
-
-init_components /home/isabelle/contrib "$HOME/admin/components/main"
-
- POLYML_HOME="/home/polyml/polyml-5.4.1"
- ML_SYSTEM="polyml-5.4.1"
- ML_PLATFORM="x86-linux"
- ML_HOME="$POLYML_HOME/$ML_PLATFORM"
- ML_OPTIONS="-H 1000"
-
-ISABELLE_GHC=/usr/bin/ghc
-
-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_BUILD_OPTIONS="browser_info=true document=pdf"
-
--- a/Admin/isatest/settings/at-poly-test Sun Feb 28 21:19:58 2016 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,34 +0,0 @@
-# -*- shell-script -*- :mode=shellscript:
-
-init_components /home/isabelle/contrib "$HOME/admin/components/main"
-
- POLYML_HOME="/home/polyml/polyml-svn"
- ML_SYSTEM="polyml-5.5.2"
- ML_PLATFORM="x86-linux"
- ML_HOME="$POLYML_HOME/$ML_PLATFORM"
- ML_OPTIONS="-H 500 --gcthreads 4"
-
-ISABELLE_GHC=/usr/bin/ghc
-
-ISABELLE_HOME_USER=~/isabelle-at-poly-test
-
-# 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_BUILD_OPTIONS="browser_info=true document=pdf threads=4 parallel_proofs=2"
-
-ISABELLE_GHC="/usr/bin/ghc"
-ISABELLE_OCAML="/usr/bin/ocaml"
-ISABELLE_SWIPL="/usr/bin/swipl"
-
--- a/Admin/isatest/settings/mac-poly-M2 Sun Feb 28 21:19:58 2016 +0100
+++ b/Admin/isatest/settings/mac-poly-M2 Sun Feb 28 21:20:11 2016 +0100
@@ -4,10 +4,9 @@
init_components /home/isabelle/contrib "$HOME/admin/components/optional"
init_components /home/isabelle/contrib "$HOME/admin/components/nonfree"
-ML_SYSTEM="polyml-5.5.0"
-ML_PLATFORM="x86-darwin"
-ML_HOME="/home/polyml/polyml-5.5.0/$ML_PLATFORM"
-ML_OPTIONS="-H 500"
+ML_PLATFORM="$ISABELLE_PLATFORM32"
+ML_HOME="$POLYML_HOME/$ML_PLATFORM"
+ML_OPTIONS="-H 1000 --gcthreads 4"
ISABELLE_GHC=ghc
@@ -28,4 +27,3 @@
ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info"
ISABELLE_BUILD_OPTIONS="browser_info=true document=pdf threads=2 parallel_proofs=2"
-
--- a/Admin/isatest/settings/mac-poly-M2-alternative Sun Feb 28 21:19:58 2016 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,29 +0,0 @@
-# -*- shell-script -*- :mode=shellscript:
-
-init_components /home/isabelle/contrib "$HOME/admin/components/main"
-init_components /home/isabelle/contrib "$HOME/admin/components/optional"
-init_components /home/isabelle/contrib "$HOME/admin/components/nonfree"
-
-ML_PLATFORM="$ISABELLE_PLATFORM32"
-ML_HOME="$POLYML_HOME/$ML_PLATFORM"
-ML_OPTIONS="-H 1000"
-
-ISABELLE_HOME_USER=~/isabelle-mac-poly-M2-alternative
-
-# 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_BUILD_OPTIONS="browser_info=true document=pdf threads=2 parallel_proofs=2"
-
-ISABELLE_GHC=ghc
--- a/Admin/isatest/settings/mac-poly-M4 Sun Feb 28 21:19:58 2016 +0100
+++ b/Admin/isatest/settings/mac-poly-M4 Sun Feb 28 21:20:11 2016 +0100
@@ -1,10 +1,12 @@
# -*- shell-script -*- :mode=shellscript:
init_components /home/isabelle/contrib "$HOME/admin/components/main"
+init_components /home/isabelle/contrib "$HOME/admin/components/optional"
+init_components /home/isabelle/contrib "$HOME/admin/components/nonfree"
ML_PLATFORM="$ISABELLE_PLATFORM32"
ML_HOME="$POLYML_HOME/$ML_PLATFORM"
-ML_OPTIONS="-H 500 --gcthreads 4"
+ML_OPTIONS="-H 1000 --gcthreads 4"
ISABELLE_HOME_USER=~/isabelle-mac-poly-M4
--- a/Admin/isatest/settings/mac-poly-M8 Sun Feb 28 21:19:58 2016 +0100
+++ b/Admin/isatest/settings/mac-poly-M8 Sun Feb 28 21:20:11 2016 +0100
@@ -1,10 +1,12 @@
# -*- shell-script -*- :mode=shellscript:
init_components /home/isabelle/contrib "$HOME/admin/components/main"
+init_components /home/isabelle/contrib "$HOME/admin/components/optional"
+init_components /home/isabelle/contrib "$HOME/admin/components/nonfree"
ML_PLATFORM="$ISABELLE_PLATFORM32"
ML_HOME="$POLYML_HOME/$ML_PLATFORM"
-ML_OPTIONS="-H 500 --gcthreads 8"
+ML_OPTIONS="-H 1000 --gcthreads 8"
ISABELLE_HOME_USER=~/isabelle-mac-poly-M8
--- a/Admin/isatest/settings/mac-poly-M8-quick_and_dirty Sun Feb 28 21:19:58 2016 +0100
+++ b/Admin/isatest/settings/mac-poly-M8-quick_and_dirty Sun Feb 28 21:20:11 2016 +0100
@@ -1,14 +1,12 @@
# -*- shell-script -*- :mode=shellscript:
init_components /home/isabelle/contrib "$HOME/admin/components/main"
+init_components /home/isabelle/contrib "$HOME/admin/components/optional"
+init_components /home/isabelle/contrib "$HOME/admin/components/nonfree"
- POLYML_HOME="/home/polyml/polyml-5.5.1"
- ML_SYSTEM="polyml-5.5.1"
- ML_PLATFORM="x86-darwin"
- ML_HOME="$POLYML_HOME/$ML_PLATFORM"
- ML_OPTIONS="-H 1000"
-
-ISABELLE_GHC=ghc
+ML_PLATFORM="$ISABELLE_PLATFORM32"
+ML_HOME="$POLYML_HOME/$ML_PLATFORM"
+ML_OPTIONS="-H 1000 --gcthreads 8"
ISABELLE_HOME_USER=~/isabelle-mac-poly-M8-quick_and_dirty
@@ -27,3 +25,11 @@
ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info"
ISABELLE_BUILD_OPTIONS="threads=8 quick_and_dirty"
+
+ISABELLE_GHC=ghc
+ISABELLE_MLTON=mlton
+ISABELLE_OCAML=ocaml
+ISABELLE_OCAMLC=ocamlc
+ISABELLE_POLYML="$ML_HOME/poly"
+#ISABELLE_SCALA="$SCALA_HOME/bin"
+ISABELLE_SMLNJ="/mnt/nfsbroy/home/smlnj/bin/sml"
--- a/Admin/isatest/settings/mac-poly-M8-skip_proofs Sun Feb 28 21:19:58 2016 +0100
+++ b/Admin/isatest/settings/mac-poly-M8-skip_proofs Sun Feb 28 21:20:11 2016 +0100
@@ -1,14 +1,12 @@
# -*- shell-script -*- :mode=shellscript:
init_components /home/isabelle/contrib "$HOME/admin/components/main"
+init_components /home/isabelle/contrib "$HOME/admin/components/optional"
+init_components /home/isabelle/contrib "$HOME/admin/components/nonfree"
- POLYML_HOME="/home/polyml/polyml-5.5.0"
- ML_SYSTEM="polyml-5.5.0"
- ML_PLATFORM="x86-darwin"
- ML_HOME="$POLYML_HOME/$ML_PLATFORM"
- ML_OPTIONS="-H 1000 --gcthreads 8"
-
-ISABELLE_GHC=ghc
+ML_PLATFORM="$ISABELLE_PLATFORM32"
+ML_HOME="$POLYML_HOME/$ML_PLATFORM"
+ML_OPTIONS="-H 1000 --gcthreads 8"
ISABELLE_HOME_USER=~/isabelle-mac-poly-M8-skip_proofs
@@ -27,3 +25,11 @@
ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info"
ISABELLE_BUILD_OPTIONS="threads=8 skip_proofs"
+
+ISABELLE_GHC=ghc
+ISABELLE_MLTON=mlton
+ISABELLE_OCAML=ocaml
+ISABELLE_OCAMLC=ocamlc
+ISABELLE_POLYML="$ML_HOME/poly"
+#ISABELLE_SCALA="$SCALA_HOME/bin"
+ISABELLE_SMLNJ="/mnt/nfsbroy/home/smlnj/bin/sml"
--- a/Admin/isatest/settings/mac-poly64-M2 Sun Feb 28 21:19:58 2016 +0100
+++ b/Admin/isatest/settings/mac-poly64-M2 Sun Feb 28 21:20:11 2016 +0100
@@ -1,12 +1,12 @@
# -*- shell-script -*- :mode=shellscript:
init_components /home/isabelle/contrib "$HOME/admin/components/main"
+init_components /home/isabelle/contrib "$HOME/admin/components/optional"
+init_components /home/isabelle/contrib "$HOME/admin/components/nonfree"
- POLYML_HOME="/home/polyml/polyml-5.5.0"
- ML_SYSTEM="polyml-5.5.0"
- ML_PLATFORM="x86_64-darwin"
- ML_HOME="$POLYML_HOME/$ML_PLATFORM"
- ML_OPTIONS="-H 1000"
+ML_PLATFORM="$ISABELLE_PLATFORM64"
+ML_HOME="$POLYML_HOME/$ML_PLATFORM"
+ML_OPTIONS="-H 2000 --gcthreads 2"
ISABELLE_GHC=ghc
@@ -27,4 +27,3 @@
ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info"
ISABELLE_BUILD_OPTIONS="browser_info=false document=false threads=2 parallel_proofs=2"
-
--- a/Admin/isatest/settings/mac-poly64-M4 Sun Feb 28 21:19:58 2016 +0100
+++ b/Admin/isatest/settings/mac-poly64-M4 Sun Feb 28 21:20:11 2016 +0100
@@ -1,13 +1,13 @@
# -*- shell-script -*- :mode=shellscript:
init_components /home/isabelle/contrib "$HOME/admin/components/main"
+init_components /home/isabelle/contrib "$HOME/admin/components/optional"
+init_components /home/isabelle/contrib "$HOME/admin/components/nonfree"
ML_PLATFORM="$ISABELLE_PLATFORM64"
ML_HOME="$POLYML_HOME/$ML_PLATFORM"
ML_OPTIONS="-H 2000 --gcthreads 4"
-ISABELLE_GHC=ghc
-
ISABELLE_HOME_USER=~/isabelle-mac-poly64-M4
# Where to look for isabelle tools (multiple dirs separated by ':').
@@ -26,3 +26,10 @@
ISABELLE_BUILD_OPTIONS="browser_info=false document=false threads=4 parallel_proofs=2"
+ISABELLE_GHC=ghc
+ISABELLE_MLTON=mlton
+ISABELLE_OCAML=ocaml
+ISABELLE_OCAMLC=ocamlc
+ISABELLE_POLYML="$ML_HOME/poly"
+#ISABELLE_SCALA="$SCALA_HOME/bin"
+ISABELLE_SMLNJ="/mnt/nfsbroy/home/smlnj/bin/sml"
--- a/Admin/isatest/settings/mac-poly64-M8 Sun Feb 28 21:19:58 2016 +0100
+++ b/Admin/isatest/settings/mac-poly64-M8 Sun Feb 28 21:20:11 2016 +0100
@@ -1,13 +1,13 @@
# -*- shell-script -*- :mode=shellscript:
init_components /home/isabelle/contrib "$HOME/admin/components/main"
+init_components /home/isabelle/contrib "$HOME/admin/components/optional"
+init_components /home/isabelle/contrib "$HOME/admin/components/nonfree"
ML_PLATFORM="$ISABELLE_PLATFORM64"
ML_HOME="$POLYML_HOME/$ML_PLATFORM"
ML_OPTIONS="-H 2000 --gcthreads 8"
-ISABELLE_GHC=ghc
-
ISABELLE_HOME_USER=~/isabelle-mac-poly64-M8
# Where to look for isabelle tools (multiple dirs separated by ':').
@@ -26,3 +26,10 @@
ISABELLE_BUILD_OPTIONS="browser_info=false document=false threads=8 parallel_proofs=2"
+ISABELLE_GHC=ghc
+ISABELLE_MLTON=mlton
+ISABELLE_OCAML=ocaml
+ISABELLE_OCAMLC=ocamlc
+ISABELLE_POLYML="$ML_HOME/poly"
+#ISABELLE_SCALA="$SCALA_HOME/bin"
+ISABELLE_SMLNJ="/mnt/nfsbroy/home/smlnj/bin/sml"
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/lib/Tools/check_sources Sun Feb 28 21:20:11 2016 +0100
@@ -0,0 +1,9 @@
+#!/usr/bin/env bash
+#
+# Author: Makarius
+#
+# DESCRIPTION: some sanity checks for Isabelle sources
+
+isabelle_admin_build jars || exit $?
+
+"$ISABELLE_TOOL" java isabelle.Check_Sources "$@"
--- a/NEWS Sun Feb 28 21:19:58 2016 +0100
+++ b/NEWS Sun Feb 28 21:20:11 2016 +0100
@@ -11,6 +11,9 @@
* New symbol \<circle>, e.g. for temporal operator.
+* Old 'header' command is no longer supported (legacy since
+Isabelle2015).
+
*** Isar ***
@@ -182,6 +185,10 @@
executables are found within the PATH: isabelle, isabelle_process,
isabelle_scala_script.
+* The somewhat pointless command-line tool "isabelle yxml" has been
+discontinued. INCOMPATIBILITY, use operations from the modules "XML" and
+"YXML" in Isabelle/ML or Isabelle/Scala.
+
* SML/NJ is no longer supported.
--- a/lib/Tools/update_cartouches Sun Feb 28 21:19:58 2016 +0100
+++ b/lib/Tools/update_cartouches Sun Feb 28 21:20:11 2016 +0100
@@ -4,62 +4,6 @@
#
# DESCRIPTION: update theory syntax to use cartouches
-
-## diagnostics
-
-PRG="$(basename "$0")"
-
-function usage()
-{
- echo
- echo "Usage: isabelle $PRG [FILES|DIRS...]"
- echo
- echo " Options are:"
- echo " -c replace comment marker \"--\" by symbol \"\\<comment>\""
- echo " -t replace @{text} antiquotations within text tokens"
- echo
- echo " Recursively find .thy files and update theory syntax to use cartouches"
- echo " instead of old-style {* verbatim *} or \`alt_string\` tokens."
- echo
- echo " Old versions of files are preserved by appending \"~~\"."
- echo
- exit 1
-}
-
-
-## process command line
-
-# options
-
-COMMENT="false"
-TEXT="false"
+isabelle_admin_build jars || exit $?
-while getopts "ct" OPT
-do
- case "$OPT" in
- c)
- COMMENT="true"
- ;;
- t)
- TEXT="true"
- ;;
- \?)
- usage
- ;;
- esac
-done
-
-shift $(($OPTIND - 1))
-
-
-# args
-
-[ "$#" -eq 0 -o "$1" = "-?" ] && usage
-
-SPECS="$@"; shift "$#"
-
-
-## main
-
-find $SPECS -name \*.thy -print0 | \
- xargs -0 "$ISABELLE_TOOL" java isabelle.Update_Cartouches "$COMMENT" "$TEXT"
+"$ISABELLE_TOOL" java isabelle.Update_Cartouches "$@"
--- a/lib/Tools/update_header Sun Feb 28 21:19:58 2016 +0100
+++ b/lib/Tools/update_header Sun Feb 28 21:20:11 2016 +0100
@@ -4,57 +4,6 @@
#
# DESCRIPTION: replace obsolete theory header command
-
-## diagnostics
-
-PRG="$(basename "$0")"
-
-function usage()
-{
- echo
- echo "Usage: isabelle $PRG [FILES|DIRS...]"
- echo
- echo " Options are:"
- echo " -s COMMAND alternative heading command (default 'section')"
- echo
- echo " Recursively find .thy files and replace obsolete theory header commands"
- echo " by 'section' (default), or 'chapter', 'subsection', 'subsubsection'."
- echo
- echo " Old versions of files are preserved by appending \"~~\"."
- echo
- exit 1
-}
-
-
-## process command line
-
-#options
+isabelle_admin_build jars || exit $?
-SECTION="section"
-
-while getopts "s:" OPT
-do
- case "$OPT" in
- s)
- SECTION="$OPTARG"
- ;;
- \?)
- usage
- ;;
- esac
-done
-
-shift $(($OPTIND - 1))
-
-
-# args
-
-[ "$#" -eq 0 -o "$1" = "-?" ] && usage
-
-SPECS="$@"; shift "$#"
-
-
-## main
-
-find $SPECS -name \*.thy -print0 | \
- xargs -0 "$ISABELLE_TOOL" java isabelle.Update_Header "$SECTION"
+"$ISABELLE_TOOL" java isabelle.Update_Header "$@"
--- a/lib/Tools/update_semicolons Sun Feb 28 21:19:58 2016 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,35 +0,0 @@
-#!/usr/bin/env bash
-#
-# Author: Makarius
-#
-# DESCRIPTION: remove obsolete semicolons from theory sources
-
-
-## diagnostics
-
-PRG="$(basename "$0")"
-
-function usage()
-{
- echo
- echo "Usage: isabelle $PRG [FILES|DIRS...]"
- echo
- echo " Recursively find .thy files and remove obsolete semicolons."
- echo
- echo " Old versions of files are preserved by appending \"~~\"."
- echo
- exit 1
-}
-
-
-## process command line
-
-[ "$#" -eq 0 -o "$1" = "-?" ] && usage
-
-SPECS="$@"; shift "$#"
-
-
-## main
-
-find $SPECS -name \*.thy -print0 | \
- xargs -0 "$ISABELLE_TOOL" java isabelle.Update_Semicolons
--- a/lib/Tools/update_sub_sup Sun Feb 28 21:19:58 2016 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,36 +0,0 @@
-#!/usr/bin/env bash
-#
-# Author: Makarius
-#
-# DESCRIPTION: update Isabelle symbols involving sub/superscripts
-
-
-## diagnostics
-
-PRG="$(basename "$0")"
-
-function usage()
-{
- echo
- echo "Usage: isabelle $PRG [FILES|DIRS...]"
- echo
- echo " Recursively find .thy/.ML files and update Isabelle symbols involving"
- echo " sub- and superscript."
- echo
- echo " Old versions of files are preserved by appending \"~~\"."
- echo
- exit 1
-}
-
-
-## process command line
-
-[ "$#" -eq 0 -o "$1" = "-?" ] && usage
-
-SPECS="$@"; shift "$#"
-
-
-## main
-
-find $SPECS \( -name \*.ML -o -name \*.thy \) -print0 | \
- xargs -0 "$ISABELLE_HOME/lib/scripts/update_sub_sup"
--- a/lib/Tools/update_then Sun Feb 28 21:19:58 2016 +0100
+++ b/lib/Tools/update_then Sun Feb 28 21:20:11 2016 +0100
@@ -4,35 +4,6 @@
#
# DESCRIPTION: expand old Isar command conflations 'hence' and 'thus'
-
-## diagnostics
-
-PRG="$(basename "$0")"
+isabelle_admin_build jars || exit $?
-function usage()
-{
- echo
- echo "Usage: isabelle $PRG [FILES|DIRS...]"
- echo
- echo " Recursively find .thy files and expand old Isar command conflations:"
- echo
- echo " hence ~> then have"
- echo " thus ~> then show"
- echo
- echo " Old versions of files are preserved by appending \"~~\"."
- echo
- exit 1
-}
-
-
-## process command line
-
-[ "$#" -eq 0 -o "$1" = "-?" ] && usage
-
-SPECS="$@"; shift "$#"
-
-
-## main
-
-find $SPECS -name \*.thy -print0 | \
- xargs -0 "$ISABELLE_TOOL" java isabelle.Update_Then
+"$ISABELLE_TOOL" java isabelle.Update_Then "$@"
--- a/lib/Tools/update_theorems Sun Feb 28 21:19:58 2016 +0100
+++ b/lib/Tools/update_theorems Sun Feb 28 21:20:11 2016 +0100
@@ -4,37 +4,6 @@
#
# DESCRIPTION: update toplevel theorem keywords
-
-## diagnostics
-
-PRG="$(basename "$0")"
+isabelle_admin_build jars || exit $?
-function usage()
-{
- echo
- echo "Usage: isabelle $PRG [FILES|DIRS...]"
- echo
- echo " Recursively find .thy files and update toplevel theorem keywords:"
- echo
- echo " theorems ~> lemmas"
- echo " schematic_theorem ~> schematic_goal"
- echo " schematic_lemma ~> schematic_goal"
- echo " schematic_corollary ~> schematic_goal"
- echo
- echo " Old versions of files are preserved by appending \"~~\"."
- echo
- exit 1
-}
-
-
-## process command line
-
-[ "$#" -eq 0 -o "$1" = "-?" ] && usage
-
-SPECS="$@"; shift "$#"
-
-
-## main
-
-find $SPECS -name \*.thy -print0 | \
- xargs -0 "$ISABELLE_TOOL" java isabelle.Update_Theorems
+"$ISABELLE_TOOL" java isabelle.Update_Theorems "$@"
--- a/lib/Tools/yxml Sun Feb 28 21:19:58 2016 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,34 +0,0 @@
-#!/usr/bin/env bash
-#
-# Author: Makarius
-#
-# DESCRIPTION: simple XML to YXML converter
-
-
-PRG="$(basename "$0")"
-
-function usage()
-{
- echo
- echo "Usage: isabelle $PRG"
- echo
- echo " Convert XML (stdin) to YXML (stdout)."
- echo
- exit 1
-}
-
-function fail()
-{
- echo "$1" >&2
- exit 2
-}
-
-
-## process command line
-
-[ "$#" -ne 0 ] && usage
-
-
-## main
-
-exec "$ISABELLE_HOME/lib/scripts/yxml"
--- a/lib/scripts/update_sub_sup Sun Feb 28 21:19:58 2016 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,44 +0,0 @@
-#!/usr/bin/env perl
-#
-# Author: Makarius
-#
-# update_sub_sup - update Isabelle symbols involving sub/superscripts
-
-use warnings;
-use strict;
-
-sub update_sub_sup {
- my ($file) = @_;
-
- open (FILE, $file) || die $!;
- undef $/; my $text = <FILE>; $/ = "\n"; # slurp whole file
- close FILE || die $!;
-
- $_ = $text;
-
- s/\Q\<^isub>\E/\\<^sub>/g;
- s/\Q\<^isup>\E/\\<^sup>/g;
- s/\Q\<onesuperior>\E/\\<^sup>1/g;
- s/\Q\<twosuperior>\E/\\<^sup>2/g;
- s/\Q\<threesuperior>\E/\\<^sup>3/g;
-
- my $result = $_;
-
- if ($text ne $result) {
- print STDERR "changing $file\n";
- if (! -f "$file~~") {
- rename $file, "$file~~" || die $!;
- }
- open (FILE, "> $file") || die $!;
- print FILE $result;
- close FILE || die $!;
- }
-}
-
-
-## main
-
-foreach my $file (@ARGV) {
- eval { &update_sub_sup($file); };
- if ($@) { print STDERR "*** update_sub_sup $file: ", $@, "\n"; }
-}
--- a/lib/scripts/yxml Sun Feb 28 21:19:58 2016 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,37 +0,0 @@
-#!/usr/bin/env perl
-#
-# Author: Makarius
-#
-# yxml.pl - simple XML to YXML converter
-#
-
-use warnings;
-use strict;
-
-use XML::Parser;
-
-binmode(STDOUT, ":utf8");
-
-sub handle_start {
- print chr(5), chr(6), $_[1];
- for (my $i = 2; $i <= $#_; $i++) {
- print ($i % 2 == 0 ? chr(6) : "=");
- print $_[$i];
- }
- print chr(5);
-}
-
-sub handle_end {
- print chr(5), chr(6), chr(5);
-}
-
-sub handle_char {
- print $_[1];
-}
-
-my $parser = new XML::Parser(Handlers =>
- {Start => \&handle_start,
- End => \&handle_end,
- Char => \&handle_char});
-
-$parser->parse(*STDIN) or die $!;
--- a/src/Doc/System/Basics.thy Sun Feb 28 21:19:58 2016 +0100
+++ b/src/Doc/System/Basics.thy Sun Feb 28 21:20:11 2016 +0100
@@ -447,4 +447,41 @@
@{verbatim [display] \<open>isabelle getenv ISABELLE_HOME_USER\<close>}
\<close>
+
+section \<open>YXML versus XML\<close>
+
+text \<open>
+ Isabelle tools often use YXML, which is a simple and efficient syntax for
+ untyped XML trees. The YXML format is defined as follows.
+
+ \<^enum> The encoding is always UTF-8.
+
+ \<^enum> Body text is represented verbatim (no escaping, no special treatment of
+ white space, no named entities, no CDATA chunks, no comments).
+
+ \<^enum> Markup elements are represented via ASCII control characters \<open>\<^bold>X = 5\<close>
+ and \<open>\<^bold>Y = 6\<close> as follows:
+
+ \begin{tabular}{ll}
+ XML & YXML \\\hline
+ \<^verbatim>\<open><\<close>\<open>name attribute\<close>\<^verbatim>\<open>=\<close>\<open>value \<dots>\<close>\<^verbatim>\<open>>\<close> &
+ \<open>\<^bold>X\<^bold>Yname\<^bold>Yattribute\<close>\<^verbatim>\<open>=\<close>\<open>value\<dots>\<^bold>X\<close> \\
+ \<^verbatim>\<open></\<close>\<open>name\<close>\<^verbatim>\<open>>\<close> & \<open>\<^bold>X\<^bold>Y\<^bold>X\<close> \\
+ \end{tabular}
+
+ There is no special case for empty body text, i.e.\ \<^verbatim>\<open><foo/>\<close> is treated
+ like \<^verbatim>\<open><foo></foo>\<close>. Also note that \<open>\<^bold>X\<close> and \<open>\<^bold>Y\<close> may never occur in
+ well-formed XML documents.
+
+ Parsing YXML is pretty straight-forward: split the text into chunks
+ separated by \<open>\<^bold>X\<close>, then split each chunk into sub-chunks separated by \<open>\<^bold>Y\<close>.
+ Markup chunks start with an empty sub-chunk, and a second empty sub-chunk
+ indicates close of an element. Any other non-empty chunk consists of plain
+ text. For example, see @{file "~~/src/Pure/PIDE/yxml.ML"} or @{file
+ "~~/src/Pure/PIDE/yxml.scala"}.
+
+ YXML documents may be detected quickly by checking that the first two
+ characters are \<open>\<^bold>X\<^bold>Y\<close>.
+\<close>
+
end
\ No newline at end of file
--- a/src/Doc/System/Misc.thy Sun Feb 28 21:19:58 2016 +0100
+++ b/src/Doc/System/Misc.thy Sun Feb 28 21:20:11 2016 +0100
@@ -265,42 +265,4 @@
id of the @{setting ISABELLE_HOME} directory.
\<close>
-
-section \<open>Convert XML to YXML\<close>
-
-text \<open>
- The @{tool_def yxml} tool converts a standard XML document (stdin) to the
- much simpler and more efficient YXML format of Isabelle (stdout). The YXML
- format is defined as follows.
-
- \<^enum> The encoding is always UTF-8.
-
- \<^enum> Body text is represented verbatim (no escaping, no special treatment of
- white space, no named entities, no CDATA chunks, no comments).
-
- \<^enum> Markup elements are represented via ASCII control characters \<open>\<^bold>X = 5\<close>
- and \<open>\<^bold>Y = 6\<close> as follows:
-
- \begin{tabular}{ll}
- XML & YXML \\\hline
- \<^verbatim>\<open><\<close>\<open>name attribute\<close>\<^verbatim>\<open>=\<close>\<open>value \<dots>\<close>\<^verbatim>\<open>>\<close> &
- \<open>\<^bold>X\<^bold>Yname\<^bold>Yattribute\<close>\<^verbatim>\<open>=\<close>\<open>value\<dots>\<^bold>X\<close> \\
- \<^verbatim>\<open></\<close>\<open>name\<close>\<^verbatim>\<open>>\<close> & \<open>\<^bold>X\<^bold>Y\<^bold>X\<close> \\
- \end{tabular}
-
- There is no special case for empty body text, i.e.\ \<^verbatim>\<open><foo/>\<close> is treated
- like \<^verbatim>\<open><foo></foo>\<close>. Also note that \<open>\<^bold>X\<close> and \<open>\<^bold>Y\<close> may never occur in
- well-formed XML documents.
-
- Parsing YXML is pretty straight-forward: split the text into chunks
- separated by \<open>\<^bold>X\<close>, then split each chunk into sub-chunks separated by \<open>\<^bold>Y\<close>.
- Markup chunks start with an empty sub-chunk, and a second empty sub-chunk
- indicates close of an element. Any other non-empty chunk consists of plain
- text. For example, see @{file "~~/src/Pure/PIDE/yxml.ML"} or @{file
- "~~/src/Pure/PIDE/yxml.scala"}.
-
- YXML documents may be detected quickly by checking that the first two
- characters are \<open>\<^bold>X\<^bold>Y\<close>.
-\<close>
-
end
\ No newline at end of file
--- a/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy Sun Feb 28 21:19:58 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy Sun Feb 28 21:20:11 2016 +0100
@@ -200,7 +200,7 @@
text \<open>
John Harrison writes as follows:
-``The usual assumption in complex analysis texts is that a path \<gamma> should be piecewise
+``The usual assumption in complex analysis texts is that a path \<open>\<gamma>\<close> should be piecewise
continuously differentiable, which ensures that the path integral exists at least for any continuous
f, since all piecewise continuous functions are integrable. However, our notion of validity is
weaker, just piecewise differentiability... [namely] continuity plus differentiability except on a
--- a/src/Pure/General/file.scala Sun Feb 28 21:19:58 2016 +0100
+++ b/src/Pure/General/file.scala Sun Feb 28 21:20:11 2016 +0100
@@ -10,7 +10,8 @@
import java.io.{BufferedWriter, OutputStreamWriter, FileOutputStream, BufferedOutputStream,
OutputStream, InputStream, FileInputStream, BufferedInputStream, BufferedReader,
InputStreamReader, File => JFile, IOException}
-import java.nio.file.{StandardCopyOption, Files}
+import java.nio.file.{StandardCopyOption, Path => JPath, Files, SimpleFileVisitor, FileVisitResult}
+import java.nio.file.attribute.BasicFileAttributes
import java.net.{URL, URLDecoder, MalformedURLException}
import java.util.zip.{GZIPInputStream, GZIPOutputStream}
import java.util.regex.Pattern
@@ -107,24 +108,29 @@
def shell_path(file: JFile): String = shell_quote(standard_path(file))
- /* directory content */
+ /* find files */
- def read_dir(dir: Path): List[String] =
+ def find_files(start: JFile, pred: JFile => Boolean = _ => true): List[JFile] =
{
- if (!dir.is_dir) error("Bad directory: " + dir.toString)
- val files = dir.file.listFiles
- if (files == null) Nil
- else files.toList.map(_.getName)
+ val result = new mutable.ListBuffer[JFile]
+
+ if (start.isFile && pred(start)) result += start
+ else if (start.isDirectory) {
+ Files.walkFileTree(start.toPath,
+ new SimpleFileVisitor[JPath] {
+ override def visitFile(path: JPath, attrs: BasicFileAttributes): FileVisitResult =
+ {
+ val file = path.toFile
+ if (pred(file)) result += file
+ FileVisitResult.CONTINUE
+ }
+ }
+ )
+ }
+
+ result.toList
}
- def find_files(dir: Path): Stream[Path] =
- read_dir(dir).toStream.map(name =>
- if (Path.is_wellformed(name)) {
- val path = dir + Path.basic(name)
- path #:: (if (path.is_dir) find_files(path) else Stream.empty)
- }
- else Stream.empty).flatten
-
/* read */
@@ -190,13 +196,13 @@
def write_backup(path: Path, text: CharSequence)
{
path.file renameTo path.backup.file
- File.write(path, text)
+ write(path, text)
}
def write_backup2(path: Path, text: CharSequence)
{
path.file renameTo path.backup2.file
- File.write(path, text)
+ write(path, text)
}
--- a/src/Pure/Isar/outer_syntax.scala Sun Feb 28 21:19:58 2016 +0100
+++ b/src/Pure/Isar/outer_syntax.scala Sun Feb 28 21:20:11 2016 +0100
@@ -237,7 +237,7 @@
val name = command.span.name
name match {
case Thy_Header.CHAPTER => Some(0)
- case Thy_Header.SECTION | Thy_Header.HEADER => Some(1)
+ case Thy_Header.SECTION => Some(1)
case Thy_Header.SUBSECTION => Some(2)
case Thy_Header.SUBSUBSECTION => Some(3)
case Thy_Header.PARAGRAPH => Some(4)
--- a/src/Pure/System/getopts.scala Sun Feb 28 21:19:58 2016 +0100
+++ b/src/Pure/System/getopts.scala Sun Feb 28 21:20:11 2016 +0100
@@ -9,7 +9,7 @@
object Getopts
{
- def apply(usage_text: () => String, option_specs: (String, String => Unit)*): Getopts =
+ def apply(usage_text: String, option_specs: (String, String => Unit)*): Getopts =
{
val options =
(Map.empty[Char, (Boolean, String => Unit)] /: option_specs) {
@@ -25,11 +25,11 @@
}
}
-class Getopts private(usage_text: () => String, options: Map[Char, (Boolean, String => Unit)])
+class Getopts private(usage_text: String, options: Map[Char, (Boolean, String => Unit)])
{
def usage(): Nothing =
{
- Console.println(usage_text())
+ Console.println(usage_text)
sys.exit(1)
}
--- a/src/Pure/System/options.scala Sun Feb 28 21:19:58 2016 +0100
+++ b/src/Pure/System/options.scala Sun Feb 28 21:20:11 2016 +0100
@@ -150,7 +150,7 @@
var list_options = false
var export_file = ""
- val getopts = Getopts(() => """
+ val getopts = Getopts("""
Usage: isabelle options [OPTIONS] [MORE_OPTIONS ...]
Options are:
--- a/src/Pure/Thy/thy_header.ML Sun Feb 28 21:19:58 2016 +0100
+++ b/src/Pure/Thy/thy_header.ML Sun Feb 28 21:20:11 2016 +0100
@@ -42,8 +42,6 @@
(* bootstrap keywords *)
-val headerN = "header"; (* FIXME legacy *)
-
val chapterN = "chapter";
val sectionN = "section";
val subsectionN = "subsection";
@@ -72,7 +70,6 @@
((beginN, @{here}), NONE),
((importsN, @{here}), NONE),
((keywordsN, @{here}), NONE),
- ((headerN, @{here}), SOME ((Keyword.document_heading, []), [])),
((chapterN, @{here}), SOME ((Keyword.document_heading, []), [])),
((sectionN, @{here}), SOME ((Keyword.document_heading, []), [])),
((subsectionN, @{here}), SOME ((Keyword.document_heading, []), [])),
@@ -147,8 +144,7 @@
(* read header *)
val heading =
- (Parse.command headerN ||
- Parse.command chapterN ||
+ (Parse.command chapterN ||
Parse.command sectionN ||
Parse.command subsectionN ||
Parse.command subsubsectionN ||
--- a/src/Pure/Thy/thy_header.scala Sun Feb 28 21:19:58 2016 +0100
+++ b/src/Pure/Thy/thy_header.scala Sun Feb 28 21:20:11 2016 +0100
@@ -19,8 +19,6 @@
type Keywords = List[(String, Option[Keyword.Spec], Option[String])]
- val HEADER = "header" /* FIXME legacy */
-
val CHAPTER = "chapter"
val SECTION = "section"
val SUBSECTION = "subsection"
@@ -49,7 +47,6 @@
(BEGIN, None, None),
(IMPORTS, None, None),
(KEYWORDS, None, None),
- (HEADER, Some(((Keyword.DOCUMENT_HEADING, Nil), Nil)), None),
(CHAPTER, Some(((Keyword.DOCUMENT_HEADING, Nil), Nil)), None),
(SECTION, Some(((Keyword.DOCUMENT_HEADING, Nil), Nil)), None),
(SUBSECTION, Some(((Keyword.DOCUMENT_HEADING, Nil), Nil)), None),
@@ -115,8 +112,7 @@
{ case x ~ ys ~ zs ~ _ => Thy_Header(x, ys, zs) }
val heading =
- (command(HEADER) |
- command(CHAPTER) |
+ (command(CHAPTER) |
command(SECTION) |
command(SUBSECTION) |
command(SUBSUBSECTION) |
--- a/src/Pure/Thy/thy_output.ML Sun Feb 28 21:19:58 2016 +0100
+++ b/src/Pure/Thy/thy_output.ML Sun Feb 28 21:20:11 2016 +0100
@@ -35,7 +35,6 @@
val string_of_margin: Proof.context -> Pretty.T -> string
val output: Proof.context -> Pretty.T list -> string
val verbatim_text: Proof.context -> string -> string
- val old_header_command: Input.source -> Toplevel.transition -> Toplevel.transition
val document_command: {markdown: bool} -> (xstring * Position.T) option * Input.source ->
Toplevel.transition -> Toplevel.transition
end;
@@ -647,14 +646,7 @@
-(** document commands **)
-
-fun old_header_command txt =
- Toplevel.keep (fn state =>
- if Toplevel.is_toplevel state then
- (legacy_feature "Obsolete 'header' command -- use 'chapter', 'section' etc. instead";
- ignore (output_text state {markdown = false} txt))
- else raise Toplevel.UNDEF);
+(** document command **)
fun document_command markdown (loc, txt) =
Toplevel.keep (fn state =>
--- a/src/Pure/Tools/build_doc.scala Sun Feb 28 21:19:58 2016 +0100
+++ b/src/Pure/Tools/build_doc.scala Sun Feb 28 21:20:11 2016 +0100
@@ -77,7 +77,7 @@
var system_mode = false
val getopts =
- Getopts(() => """
+ Getopts("""
Usage: isabelle build_doc [OPTIONS] [DOCS ...]"
Options are:
--- a/src/Pure/Tools/check_source.scala Sun Feb 28 21:19:58 2016 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,61 +0,0 @@
-/* Title: Pure/Tools/check_source.scala
- Author: Makarius
-
-Some sanity checks for Isabelle sources.
-*/
-
-package isabelle
-
-
-object Check_Source
-{
- def check_file(path: Path)
- {
- val file_name = path.implode
- val file_pos = path.position
- def line_pos(i: Int) = Position.Line_File(i + 1, file_name)
-
- val content = File.read(path)
-
- for { (line, i) <- split_lines(content).iterator.zipWithIndex }
- {
- try {
- Symbol.decode_strict(line)
-
- for { c <- Word.codepoint_iterator(line); if c > 128 && !Character.isAlphabetic(c) }
- {
- Output.warning("Suspicious Unicode character " + quote(Word.codepoint(c)) +
- Position.here(line_pos(i)))
- }
- }
- catch { case ERROR(msg) => Output.error_message(msg + Position.here(line_pos(i))) }
-
- if (line.contains('\t'))
- Output.warning("TAB character" + Position.here(line_pos(i)))
- }
-
- if (content.contains('\r'))
- Output.warning("CR character" + Position.here(file_pos))
- }
-
- def check_hg(root: Path)
- {
- Output.writeln("Checking " + root + " ...")
- Isabelle_System.hg("--repository " + File.shell_path(root) + " root").check
- for {
- file <- Isabelle_System.hg("manifest", root).check.out_lines
- if file.endsWith(".thy") || file.endsWith(".ML") || file.endsWith("/ROOT")
- } check_file(root + Path.explode(file))
- }
-
-
- /* command line entry point */
-
- def main(args: Array[String])
- {
- Command_Line.tool0 {
- for (root <- args) check_hg(Path.explode(root))
- }
- }
-}
-
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Tools/check_sources.scala Sun Feb 28 21:20:11 2016 +0100
@@ -0,0 +1,69 @@
+/* Title: Pure/Tools/check_sources.scala
+ Author: Makarius
+
+Some sanity checks for Isabelle sources.
+*/
+
+package isabelle
+
+
+object Check_Sources
+{
+ def check_file(path: Path)
+ {
+ val file_name = path.implode
+ val file_pos = path.position
+ def line_pos(i: Int) = Position.Line_File(i + 1, file_name)
+
+ val content = File.read(path)
+
+ for { (line, i) <- split_lines(content).iterator.zipWithIndex }
+ {
+ try {
+ Symbol.decode_strict(line)
+
+ for { c <- Word.codepoint_iterator(line); if c > 128 && !Character.isAlphabetic(c) }
+ {
+ Output.warning("Suspicious Unicode character " + quote(Word.codepoint(c)) +
+ Position.here(line_pos(i)))
+ }
+ }
+ catch { case ERROR(msg) => Output.error_message(msg + Position.here(line_pos(i))) }
+
+ if (line.contains('\t'))
+ Output.warning("TAB character" + Position.here(line_pos(i)))
+ }
+
+ if (content.contains('\r'))
+ Output.warning("CR character" + Position.here(file_pos))
+ }
+
+ def check_hg(root: Path)
+ {
+ Output.writeln("Checking " + root + " ...")
+ Isabelle_System.hg("--repository " + File.shell_path(root) + " root").check
+ for {
+ file <- Isabelle_System.hg("manifest", root).check.out_lines
+ if file.endsWith(".thy") || file.endsWith(".ML") || file.endsWith("/ROOT")
+ } check_file(root + Path.explode(file))
+ }
+
+
+ /* command line entry point */
+
+ def main(args: Array[String])
+ {
+ Command_Line.tool0 {
+ val getopts = Getopts("""
+Usage: isabelle check_sources [ROOT_DIRS...]
+
+ Check .thy, .ML, ROOT files from manifest of Mercurial ROOT_DIRS.
+""")
+
+ val specs = getopts(args)
+ if (specs.isEmpty) getopts.usage()
+
+ for (root <- specs) check_hg(Path.explode(root))
+ }
+ }
+}
--- a/src/Pure/Tools/doc.scala Sun Feb 28 21:19:58 2016 +0100
+++ b/src/Pure/Tools/doc.scala Sun Feb 28 21:20:11 2016 +0100
@@ -96,7 +96,7 @@
def main(args: Array[String])
{
Command_Line.tool0 {
- val getopts = Getopts(() => """
+ val getopts = Getopts("""
Usage: isabelle doc [DOC ...]
View Isabelle documentation.
--- a/src/Pure/Tools/update_cartouches.scala Sun Feb 28 21:19:58 2016 +0100
+++ b/src/Pure/Tools/update_cartouches.scala Sun Feb 28 21:20:11 2016 +0100
@@ -87,13 +87,31 @@
def main(args: Array[String])
{
Command_Line.tool0 {
- args.toList match {
- case Properties.Value.Boolean(replace_comment) ::
- Properties.Value.Boolean(replace_text) :: files =>
- files.foreach(file =>
- update_cartouches(replace_comment, replace_text, Path.explode(file)))
- case _ => error("Bad arguments:\n" + cat_lines(args))
- }
+ var replace_comment = false
+ var replace_text = false
+
+ val getopts = Getopts("""
+Usage: isabelle update_cartouches [FILES|DIRS...]
+
+ Options are:
+ -c replace comment marker "--" by symbol "\<comment>"
+ -t replace @{text} antiquotations within text tokens
+
+ Recursively find .thy files and update theory syntax to use cartouches
+ instead of old-style {* verbatim *} or `alt_string` tokens.
+
+ Old versions of files are preserved by appending "~~".
+""",
+ "c" -> (_ => replace_comment = true),
+ "t" -> (_ => replace_text = true))
+
+ val specs = getopts(args)
+ if (specs.isEmpty) getopts.usage()
+
+ for {
+ spec <- specs
+ file <- File.find_files(Path.explode(spec).file, file => file.getName.endsWith(".thy"))
+ } update_cartouches(replace_comment, replace_text, Path.explode(File.standard_path(file)))
}
}
}
--- a/src/Pure/Tools/update_header.scala Sun Feb 28 21:19:58 2016 +0100
+++ b/src/Pure/Tools/update_header.scala Sun Feb 28 21:20:11 2016 +0100
@@ -31,14 +31,32 @@
def main(args: Array[String])
{
Command_Line.tool0 {
- args.toList match {
- case section :: files =>
- if (!headings.contains(section))
- error("Bad heading command: " + quote(section))
- files.foreach(file => update_header(section, Path.explode(file)))
- case _ =>
- error("Bad arguments:\n" + cat_lines(args))
- }
+ var section = "section"
+
+ val getopts = Getopts("""
+Usage: isabelle update_header [FILES|DIRS...]
+
+ Options are:
+ -s COMMAND alternative heading command (default 'section')
+
+ Recursively find .thy files and replace obsolete theory header commands
+ by 'chapter', 'section' (default), 'subsection', 'subsubsection',
+ 'paragraph', 'subparagraph'.
+
+ Old versions of files are preserved by appending "~~".
+""",
+ "s:" -> (arg => section = arg))
+
+ val specs = getopts(args)
+ if (specs.isEmpty) getopts.usage()
+
+ if (!headings.contains(section))
+ error("Bad heading command: " + quote(section))
+
+ for {
+ spec <- specs
+ file <- File.find_files(Path.explode(spec).file, file => file.getName.endsWith(".thy"))
+ } update_header(section, Path.explode(File.standard_path(file)))
}
}
}
--- a/src/Pure/Tools/update_semicolons.scala Sun Feb 28 21:19:58 2016 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,34 +0,0 @@
-/* Title: Pure/Tools/update_semicolons.scala
- Author: Makarius
-
-Remove obsolete semicolons from theory sources.
-*/
-
-package isabelle
-
-
-object Update_Semicolons
-{
- def update_semicolons(path: Path)
- {
- val text0 = File.read(path)
- val text1 =
- (for (tok <- Token.explode(Keyword.Keywords.empty, text0).iterator if tok.source != ";")
- yield tok.source).mkString
-
- if (text0 != text1) {
- Output.writeln("changing " + path)
- File.write_backup2(path, text1)
- }
- }
-
-
- /* command line entry point */
-
- def main(args: Array[String])
- {
- Command_Line.tool0 {
- args.foreach(arg => update_semicolons(Path.explode(arg)))
- }
- }
-}
--- a/src/Pure/Tools/update_then.scala Sun Feb 28 21:19:58 2016 +0100
+++ b/src/Pure/Tools/update_then.scala Sun Feb 28 21:20:11 2016 +0100
@@ -33,7 +33,24 @@
def main(args: Array[String])
{
Command_Line.tool0 {
- args.foreach(arg => update_then(Path.explode(arg)))
+ val getopts = Getopts("""
+Usage: isabelle update_then [FILES|DIRS...]
+
+ Recursively find .thy files and expand old Isar command conflations:
+
+ hence ~> then have
+ thus ~> then show
+
+ Old versions of files are preserved by appending "~~".
+""")
+
+ val specs = getopts(args)
+ if (specs.isEmpty) getopts.usage()
+
+ for {
+ spec <- specs
+ file <- File.find_files(Path.explode(spec).file, file => file.getName.endsWith(".thy"))
+ } update_then(Path.explode(File.standard_path(file)))
}
}
}
--- a/src/Pure/Tools/update_theorems.scala Sun Feb 28 21:19:58 2016 +0100
+++ b/src/Pure/Tools/update_theorems.scala Sun Feb 28 21:20:11 2016 +0100
@@ -34,7 +34,26 @@
def main(args: Array[String])
{
Command_Line.tool0 {
- args.foreach(arg => update_theorems(Path.explode(arg)))
+ val getopts = Getopts("""
+Usage: isabelle update_theorems [FILES|DIRS...]
+
+ Recursively find .thy files and update toplevel theorem keywords:
+
+ theorems ~> lemmas
+ schematic_theorem ~> schematic_goal
+ schematic_lemma ~> schematic_goal
+ schematic_corollary ~> schematic_goal
+
+ Old versions of files are preserved by appending "~~".
+""")
+
+ val specs = getopts(args)
+ if (specs.isEmpty) getopts.usage()
+
+ for {
+ spec <- specs
+ file <- File.find_files(Path.explode(spec).file, file => file.getName.endsWith(".thy"))
+ } update_theorems(Path.explode(File.standard_path(file)))
}
}
}
--- a/src/Pure/build-jars Sun Feb 28 21:19:58 2016 +0100
+++ b/src/Pure/build-jars Sun Feb 28 21:20:11 2016 +0100
@@ -97,7 +97,7 @@
Tools/build_console.scala
Tools/build_doc.scala
Tools/check_keywords.scala
- Tools/check_source.scala
+ Tools/check_sources.scala
Tools/debugger.scala
Tools/doc.scala
Tools/main.scala
@@ -108,7 +108,6 @@
Tools/task_statistics.scala
Tools/update_cartouches.scala
Tools/update_header.scala
- Tools/update_semicolons.scala
Tools/update_then.scala
Tools/update_theorems.scala
library.scala
--- a/src/Pure/pure_syn.ML Sun Feb 28 21:19:58 2016 +0100
+++ b/src/Pure/pure_syn.ML Sun Feb 28 21:20:11 2016 +0100
@@ -14,10 +14,6 @@
struct
val _ =
- Outer_Syntax.command ("header", @{here}) "theory header"
- (Parse.document_source >> Thy_Output.old_header_command);
-
-val _ =
Outer_Syntax.command ("chapter", @{here}) "chapter heading"
(Parse.opt_target -- Parse.document_source >> Thy_Output.document_command {markdown = false});
--- a/src/Tools/jEdit/src/scala_console.scala Sun Feb 28 21:19:58 2016 +0100
+++ b/src/Tools/jEdit/src/scala_console.scala Sun Feb 28 21:20:11 2016 +0100
@@ -27,23 +27,10 @@
private def reconstruct_classpath(): String =
{
- def find_files(start: JFile, ok: JFile => Boolean = _ => true): List[JFile] =
- {
- val files = new mutable.ListBuffer[JFile]
- val filter = new FileFilter { def accept(entry: JFile) = entry.isDirectory || ok(entry) }
- def find_entry(entry: JFile)
- {
- if (ok(entry)) files += entry
- if (entry.isDirectory) entry.listFiles(filter).foreach(find_entry)
- }
- find_entry(start)
- files.toList
- }
-
def find_jars(start: String): List[String] =
if (start != null)
- find_files(new JFile(start),
- entry => entry.isFile && entry.getName.endsWith(".jar")).map(_.getAbsolutePath)
+ File.find_files(new JFile(start), file => file.getName.endsWith(".jar")).
+ map(_.getAbsolutePath)
else Nil
val initial_class_path =