--- a/lib/Tools/fixnumerals Thu Aug 19 12:47:45 1999 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,63 +0,0 @@
-#!/bin/bash
-#
-# $Id$
-#
-# DESCRIPTION: fix occurences of numerals in HOL/ZF terms
-
-
-## diagnostics
-
-PRG=$(basename $0)
-
-function usage()
-{
- echo
- echo "Usage: $PRG [FILES|DIRS...]"
- echo
- echo " Options are:"
- echo " -c add '(_::int)' type constraints (for HOL only)"
- echo
- echo " Recursively find .thy/.ML files, fixing occurences of"
- echo " HOL/ZF numerals: #42 becomes 42, #-42 becomes ~42".
- echo
- echo " Renames old versions of FILES by appending \"~~\"."
- echo
- exit 1
-}
-
-
-## process command line
-
-# options
-
-CONSTRAINTS=false
-
-while getopts "c" OPT
-do
- case "$OPT" in
- c)
- CONSTRAINTS=true
- ;;
- \?)
- usage
- ;;
- esac
-done
-
-shift $(($OPTIND - 1))
-
-
-# args
-
-[ $# -eq 0 ] && 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/fixnumerals.pl $CONSTRAINTS
--- a/lib/scripts/fixnumerals.pl Thu Aug 19 12:47:45 1999 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,64 +0,0 @@
-#
-# $Id$
-#
-# fixnumerals.pl - fix occurences of numerals in HOL/ZF terms
-#
-# tries to be smart; may produce garbage if nested comments and
-# solitary quotes (") are intermixed badly;
-#
-
-sub fixdots {
- my ($constr, $file) = @_;
-
- open (FILE, $file) || die $!;
- undef $/; $text = <FILE>; $/ = "\n"; # slurp whole file
- close FILE || die $!;
-
-
- $result = "";
- $rest = $text;
-
- while (1) {
- $_ = $rest;
- ($pre, $str, $rest) =
- m/^((?: \(\*.*?\*\) | [^"] )*) # pre: text or (non-nested!) comments
- "((?: [^"\\] | \\\S | \\\s+\\ )*)" # quoted string
- (.*)$/sx; # rest of file
- if ($str) {
- $_ = $str;
- if (!m/^[a-zA-Z0-9_\/\.]*$/s && !m/\.ML/s && !m/\.thy/s) { # exclude filenames!
- if ($constr eq "true") {
- s/#([0-9]+)/($1::int)/sg;
- s/#-([0-9]+)/(~$1::int)/sg;
- } else {
- s/#([0-9]+)/$1/sg;
- s/#-([0-9]+)/~$1/sg;
- }
- }
- $result = $result . $pre . '"' . $_ . '"';
- } else {
- $result = $result . $_;
- last;
- }
- }
-
- 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
-
-$constr = shift;
-
-foreach $file (@ARGV) {
- eval { &fixdots($constr, $file); };
- if ($@) { print STDERR "*** fixdots $file: ", $@, "\n"; }
-}