--- a/lib/Tools/expandshort Tue Apr 08 15:47:14 2008 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,39 +0,0 @@
-#!/usr/bin/env bash
-#
-# $Id$
-# Author: Markus Wenzel, TU Muenchen
-#
-# DESCRIPTION: expand shorthand goal commands
-
-
-PRG="$(basename "$0")"
-
-function usage()
-{
- echo
- echo "Usage: $PRG [FILES|DIRS...]"
- echo
- echo " Recursively find .ML files, expand shorthand goal commands. Also"
- echo " contracts uses of resolve_tac, dresolve_tac, eresolve_tac,"
- echo " forward_tac, rewrite_goals_tac on 1-element lists; furthermore"
- echo " expands tabs, which are forbidden in SML string constants."
- echo
- echo " Renames old versions of files by appending \"~~\"."
- echo
- exit 1
-}
-
-
-## process command line
-
-[ "$#" -eq 0 -o "$1" = "-?" ] && usage
-
-SPECS="$@"; shift "$#"
-
-
-## main
-
-#set by configure
-AUTO_PERL=perl
-
-find $SPECS -name \*.ML -print | xargs "$AUTO_PERL" -w "$ISABELLE_HOME/lib/scripts/expandshort.pl"
--- a/lib/Tools/fixcpure Tue Apr 08 15:47:14 2008 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,40 +0,0 @@
-#!/usr/bin/env bash
-#
-# $Id$
-# Author: Makarius
-#
-# DESCRIPTION: adapt theories and ML files to new CPure/Pure arrangement
-
-
-## diagnostics
-
-PRG="$(basename "$0")"
-
-function usage()
-{
- echo
- echo "Usage: $PRG [FILES|DIRS...]"
- echo
- echo " Recursively find .thy/.ML files, adapting them to"
- echo " the new CPure/Pure arrangement"
- echo
- echo " Renames old versions of FILES by appending \"~~\"."
- echo
- exit 1
-}
-
-
-## process command line
-
-[ "$#" -eq 0 -o "$1" = "-?" ] && usage
-
-SPECS="$@"; shift "$#"
-
-
-## main
-
-#set by configure
-AUTO_PERL=perl
-
-find $SPECS \( -name \*.thy -o -name \*.ML \) -print | \
- xargs "$AUTO_PERL" -w "$ISABELLE_HOME/lib/scripts/fixcpure.pl"
--- a/lib/Tools/fixgreek Tue Apr 08 15:47:14 2008 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,41 +0,0 @@
-#!/usr/bin/env bash
-#
-# $Id$
-# Author: Sebastian Skalberg, TU Muenchen
-#
-# DESCRIPTION: fix problems with greek and other foreign letters
-
-
-## diagnostics
-
-PRG="$(basename "$0")"
-
-function usage()
-{
- echo
- echo "Usage: $PRG [FILES|DIRS...]"
- echo
- echo " Recursively find .thy files, fixing parse problems stemming"
- echo " from the classification change of greek and other foreign"
- echo " letters from symbols to letters."
- echo
- echo " Renames old versions of FILES by appending \"~~\"."
- echo
- exit 1
-}
-
-
-## process command line
-
-[ "$#" -eq 0 -o "$1" = "-?" ] && usage
-
-SPECS="$@"; shift "$#"
-
-
-## main
-
-#set by configure
-AUTO_PERL=perl
-
-find $SPECS -name \*.thy -print | xargs "$AUTO_PERL" -w "$ISABELLE_HOME/lib/scripts/fixgreek.pl"
-find $SPECS -name \*.ML -print | xargs "$AUTO_PERL" -w "$ISABELLE_HOME/lib/scripts/fixgreek.pl"
--- a/lib/Tools/fixsome Tue Apr 08 15:47:14 2008 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,40 +0,0 @@
-#!/usr/bin/env bash
-#
-# $Id$
-# Author: Markus Wenzel, TU Muenchen
-#
-# DESCRIPTION: fix theorem names related to SOME (Eps) in HOL
-
-
-## diagnostics
-
-PRG="$(basename "$0")"
-
-function usage()
-{
- echo
- echo "Usage: $PRG [FILES|DIRS...]"
- echo
- echo " Recursively find .thy/.ML files, fixing theorem names related"
- echo " to SOME (Eps) in HOL."
- echo
- echo " Renames old versions of FILES by appending \"~~\"."
- echo
- exit 1
-}
-
-
-## process command line
-
-[ "$#" -eq 0 -o "$1" = "-?" ] && usage
-
-SPECS="$@"; shift "$#"
-
-
-## main
-
-#set by configure
-AUTO_PERL=perl
-
-find $SPECS \( -name \*.ML -o -name \*.thy \) -print | \
- xargs "$AUTO_PERL" -w "$ISABELLE_HOME/lib/scripts/fixsome.pl"
--- a/lib/scripts/configure Tue Apr 08 15:47:14 2008 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,18 +0,0 @@
-#!/bin/sh
-#
-# $Id$
-# Author: Markus Wenzel, TU Muenchen
-#
-# configure - adapt Isabelle distribution to system environment
-
-## patch scripts
-
-cd "`dirname "$0"`"
-
-if bash -c :
-then
- bash lib/scripts/patch-scripts.bash
-else
- echo "FATAL ERROR: bash not found!"
- exit 2
-fi
--- a/lib/scripts/expandshort.pl Tue Apr 08 15:47:14 2008 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,61 +0,0 @@
-#
-# $Id$
-#
-# expandshort.pl - expand shorthand goal commands
-#
-# in "be ... i;" -> "by (etac ... i);" the "..." phrase is not allowed to
-# contain punctuation. Otherwise, comments can be affected!
-# a special case is made to detect be alpha.alpha digits
-#
-
-sub expandshort {
- my ($file) = @_;
-
- open (FILE, $file) || die $!;
- undef $/; $text = <FILE>; $/ = "\n"; # slurp whole file
- close FILE || die $!;
-
- $_ = $text;
-
- s/\bsafe_tac *\(claset *\( *\) *\)/Safe_tac/sg;
- s/ *\(Safe_tac\) *([0-9]+)/ Safe_tac $1/sg;
- s/ *\(Safe_tac\)/ Safe_tac/sg;
- s/\bby\(/by (/sg;
- s/\bba\b *(\d+);/by (assume_tac $1);/sg;
- s/\bbr\b *([^;*!]*) (\d+);/by (rtac $1 $2);/sg;
- s/\bbrs\b *([^;*!]*) (\d+);/by (resolve_tac $1 $2);/sg;
- s/\bbd\b *([^;*!]*) (\d+);/by (dtac $1 $2);/sg;
- s/\bbds\b *([^;*!]*) (\d+);/by (dresolve_tac $1 $2);/sg;
- s/\bbe\b *([^;.*!]*) (\d+);/by (etac $1 $2);/sg;
- s/\bbe\b *(\w+\.\w+) (\d+);/by (etac $1 $2);/sg;
- s/\bbes\b *([^;*!]*) (\d+);/by (eresolve_tac $1 $2);/sg;
- s/\bbw\b *([^;*!]*);/by (rewtac $1);/sg;
- s/\bbws\b *([^;*!]*);/by (rewrite_goals_tac $1);/sg;
- s/\bauto *\(\)/by Auto_tac/sg;
- s/dresolve_tac *\[(\w+)\] */dtac $1 /sg;
- s/eresolve_tac *\[(\w+)\] */etac $1 /sg;
- s/forward_tac *\[(\w+)\] */ftac $1 /sg;
- s/resolve_tac *\[(\w+)\] */rtac $1 /sg;
- s/rewrite_goals_tac *\[(\w+)\]( *)/rewtac $1$2/sg;
- s/rtac *\((\w+)\s+RS\s+ssubst\)\s+/stac $1 /sg;
-
- $result = $_;
-
- if ($text ne $result) {
- print STDERR "expanding $file\n";
- if (! -f "$file~~") {
- rename $file, "$file~~" || die $!;
- }
- open (FILE, "> $file") || die $!;
- print FILE $result;
- close FILE || die $!;
- }
-}
-
-
-## main
-
-foreach $file (@ARGV) {
- eval { &expandshort($file); };
- if ($@) { print STDERR "*** expandshort $file: ", $@, "\n"; }
-}
--- a/lib/scripts/fixcpure.pl Tue Apr 08 15:47:14 2008 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,40 +0,0 @@
-#
-# $Id$
-# Author: Makarius
-#
-# fixcpure.pl - adapt theories and ML files to new CPure/Pure arrangement
-#
-
-sub fixcpure {
- my ($file) = @_;
-
- open (FILE, $file) || die $!;
- undef $/; $text = <FILE>; $/ = "\n"; # slurp whole file
- close FILE || die $!;
-
- $_ = $text;
-
- s/\bCPure\.thy\b/-THE-CPURE-THEORY-/sg;
- s/\bCPure\.([A-Za-z_\-])/Pure.$1/sg;
- s/-THE-CPURE-THEORY-/CPure.thy/sg;
-
- $result = $_;
-
- if ($text ne $result) {
- print STDERR "fixing $file\n";
- if (! -f "$file~~") {
- rename $file, "$file~~" || die $!;
- }
- open (FILE, "> $file") || die $!;
- print FILE $result;
- close FILE || die $!;
- }
-}
-
-
-## main
-
-foreach $file (@ARGV) {
- eval { &fixcpure($file); };
- if ($@) { print STDERR "*** fixcpure $file: ", $@, "\n"; }
-}
--- a/lib/scripts/fixgreek.pl Tue Apr 08 15:47:14 2008 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,49 +0,0 @@
-#
-# $Id$
-# Author: Sebastian Skalberg, TU Muenchen
-#
-# fixgreek.pl - fix problems with greek and other foreign letters now
-# being classified as letters instead of symbols.
-#
-
-sub fixgreek {
- my ($file) = @_;
-
- open (FILE, $file) || die $!;
- undef $/; $text = <FILE>; $/ = "\n"; # slurp whole file
- close FILE || die $!;
-
- $_ = $text;
-
- s/(\\<(a|b|c|d|e|f|g|h|i|j|k|l|m|n|o|p|q|r|s|t|u|v|w|x|y|z|A|B|C|D|E|F|G|H|I|J|K|L|M|N|O|P|Q|R|S|T|U|V|W|X|Y|Z)>)([a-zA-Z0-9])/$1 $3/sg;
-
- s/([a-zA-Z][a-zA-Z0-9]*)(\\<(a|b|c|d|e|f|g|h|i|j|k|l|m|n|o|p|q|r|s|t|u|v|w|x|y|z|A|B|C|D|E|F|G|H|I|J|K|L|M|N|O|P|Q|R|S|T|U|V|W|X|Y|Z)>)/$1 $2/sg;
-
- s/(\\<(aa|bb|cc|dd|ee|ff|gg|hh|ii|jj|kk|ll|mm|nn|oo|pp|qq|rr|ss|tt|uu|vv|ww|xx|yy|zz|AA|BB|CC|DD|EE|FF|GG|HH|II|JJ|KK|LL|MM|NN|OO|PP|QQ|RR|SS|TT|UU|VV|WW|XX|YY|ZZ)>)([a-zA-Z0-9])/$1 $3/sg;
-
- s/([a-zA-Z][a-zA-Z0-9]*)(\\<(aa|bb|cc|dd|ee|ff|gg|hh|ii|jj|kk|ll|mm|nn|oo|pp|qq|rr|ss|tt|uu|vv|ww|xx|yy|zz|AA|BB|CC|DD|EE|FF|GG|HH|II|JJ|KK|LL|MM|NN|OO|PP|QQ|RR|SS|TT|UU|VV|WW|XX|YY|ZZ)>)/$1 $2/sg;
-
- s/(\\<(alpha|beta|gamma|delta|epsilon|zeta|eta|theta|iota|kappa|mu|nu|xi|pi|rho|sigma|tau|upsilon|phi|psi|omega|Gamma|Delta|Theta|Lambda|Xi|Pi|Sigma|Upsilon|Phi|Psi|Omega)>)([a-zA-Z0-9])/$1 $3/sg;
-
- s/([a-zA-Z][a-zA-Z0-9]*)(\\<(alpha|beta|gamma|delta|epsilon|zeta|eta|theta|iota|kappa|mu|nu|xi|pi|rho|sigma|tau|upsilon|phi|psi|omega|Gamma|Delta|Theta|Lambda|Xi|Pi|Sigma|Upsilon|Phi|Psi|Omega)>)/$1 $2/sg;
-
- $result = $_;
-
- if ($text ne $result) {
- print STDERR "fixing $file\n";
- if (! -f "$file~~") {
- rename $file, "$file~~" || die $!;
- }
- open (FILE, "> $file") || die $!;
- print FILE $result;
- close FILE || die $!;
- }
-}
-
-
-## main
-
-foreach $file (@ARGV) {
- eval { &fixgreek($file); };
- if ($@) { print STDERR "*** fixgreek $file: ", $@, "\n"; }
-}
--- a/lib/scripts/fixsome.pl Tue Apr 08 15:47:14 2008 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,45 +0,0 @@
-#
-# $Id$
-# Author: Markus Wenzel, TU Muenchen
-#
-# fixsome.pl - fix theorem names related to SOME (Eps) in HOL
-#
-
-sub fixsome {
- my ($file) = @_;
-
- open (FILE, $file) || die $!;
- undef $/; $text = <FILE>; $/ = "\n"; # slurp whole file
- close FILE || die $!;
-
- $_ = $text;
-
- s/select_equality/some_equality/g;
- s/select_eq_Ex/some_eq_ex/g;
- s/selectI2EX/someI2_ex/g;
- s/selectI2/someI2/g;
- s/selectI/someI/g;
- s/select1_equality/some1_equality/g;
- s/Eps_sym_eq/some_sym_eq_trivial/g;
- s/Eps_eq/some_eq_trivial/g;
-
- $result = $_;
-
- if ($text ne $result) {
- print STDERR "fixing $file\n";
- if (! -f "$file~~") {
- rename $file, "$file~~" || die $!;
- }
- open (FILE, "> $file") || die $!;
- print FILE $result;
- close FILE || die $!;
- }
-}
-
-
-## main
-
-foreach $file (@ARGV) {
- eval { &fixsome($file); };
- if ($@) { print STDERR "*** fixsome $file: ", $@, "\n"; }
-}
--- a/lib/scripts/patch-scripts.bash Tue Apr 08 15:47:14 2008 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,52 +0,0 @@
-# -*- shell-script -*-
-# $Id$
-# Author: Markus Wenzel, TU Muenchen
-#
-# patch-scripts.bash - relocate interpreter paths of executable scripts and
-# insert AUTO_BASH/AUTO_PERL values
-#
-
-## find binaries
-
-function findbin()
-{
- local BASE="$1"
- local BINARY=""
-
- BINARY=$(type -path "$BASE")
-
- if [ -n "$BINARY" ]; then
- echo "found $BINARY" >&2
- echo "$BINARY"
- return
- else
- echo "ERROR: $BASE not found!" >&2
- echo "$DEFAULT"
- return
- fi
-}
-
-
-## main
-
-[ -z "$BASH_PATH" ] && BASH_PATH=$(findbin bash)
-[ -z "$PERL_PATH" ] && PERL_PATH=$(findbin perl)
-[ -z "$AUTO_BASH" ] && AUTO_BASH="$BASH_PATH"
-[ -z "$AUTO_PERL" ] && AUTO_PERL="$PERL_PATH"
-
-for FILE in $(find . -type f -print)
-do
- if [ -x "$FILE" ]; then
- sed -e "s:^#!.*/bash:#!$BASH_PATH:" -e "s:^#!.*/perl:#!$PERL_PATH:" \
- -e "s:^AUTO_BASH=.*bash:AUTO_BASH=$AUTO_BASH:" \
- -e "s:^AUTO_PERL=.*perl:AUTO_PERL=$AUTO_PERL:" "$FILE" > "$FILE~~"
- if cmp -s "$FILE" "$FILE~~"; then
- rm "$FILE~~"
- else
- rm -f "$FILE"
- mv "$FILE~~" "$FILE"
- chmod +x "$FILE"
- echo "fixed $FILE"
- fi
- fi
-done