# HG changeset patch
# User wenzelm
# Date 935062766 -7200
# Node ID 8cc10843475039ba1be76aa5f1d66b6955fbbb87
# Parent  da64f7413efd4dbb797c0de51170b472c57929c4
removed fixnumerals (for the time being);

diff -r da64f7413efd -r 8cc108434750 lib/Tools/fixnumerals
--- 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
diff -r da64f7413efd -r 8cc108434750 lib/scripts/fixnumerals.pl
--- 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"; }
-}