isabelle: lib/Tools/fixgreek@a6d0428dea8e (annotated)

14171 0cab06e3bbd0 Extended the notion of letter and digit, such that now one may use greek, skalberg parents: diff changeset	1	#!/usr/bin/env bash
0cab06e3bbd0 Extended the notion of letter and digit, such that now one may use greek, skalberg parents: diff changeset	2	#
0cab06e3bbd0 Extended the notion of letter and digit, such that now one may use greek, skalberg parents: diff changeset	3	# $Id$
0cab06e3bbd0 Extended the notion of letter and digit, such that now one may use greek, skalberg parents: diff changeset	4	# Author: Sebastian Skalberg, TU Muenchen
0cab06e3bbd0 Extended the notion of letter and digit, such that now one may use greek, skalberg parents: diff changeset	5	#
0cab06e3bbd0 Extended the notion of letter and digit, such that now one may use greek, skalberg parents: diff changeset	6	# DESCRIPTION: fix problems with greek and other foreign letters
0cab06e3bbd0 Extended the notion of letter and digit, such that now one may use greek, skalberg parents: diff changeset	7
0cab06e3bbd0 Extended the notion of letter and digit, such that now one may use greek, skalberg parents: diff changeset	8
0cab06e3bbd0 Extended the notion of letter and digit, such that now one may use greek, skalberg parents: diff changeset	9	## diagnostics
0cab06e3bbd0 Extended the notion of letter and digit, such that now one may use greek, skalberg parents: diff changeset	10
0cab06e3bbd0 Extended the notion of letter and digit, such that now one may use greek, skalberg parents: diff changeset	11	PRG="$(basename "$0")"
0cab06e3bbd0 Extended the notion of letter and digit, such that now one may use greek, skalberg parents: diff changeset	12
0cab06e3bbd0 Extended the notion of letter and digit, such that now one may use greek, skalberg parents: diff changeset	13	function usage()
0cab06e3bbd0 Extended the notion of letter and digit, such that now one may use greek, skalberg parents: diff changeset	14	{
0cab06e3bbd0 Extended the notion of letter and digit, such that now one may use greek, skalberg parents: diff changeset	15	echo
0cab06e3bbd0 Extended the notion of letter and digit, such that now one may use greek, skalberg parents: diff changeset	16	echo "Usage: $PRG [FILES\|DIRS...]"
0cab06e3bbd0 Extended the notion of letter and digit, such that now one may use greek, skalberg parents: diff changeset	17	echo
0cab06e3bbd0 Extended the notion of letter and digit, such that now one may use greek, skalberg parents: diff changeset	18	echo " Recursively find .thy files, fixing parse problems stemming"
0cab06e3bbd0 Extended the notion of letter and digit, such that now one may use greek, skalberg parents: diff changeset	19	echo " from the classification change of greek and other foreign"
0cab06e3bbd0 Extended the notion of letter and digit, such that now one may use greek, skalberg parents: diff changeset	20	echo " letters from symbols to letters."
0cab06e3bbd0 Extended the notion of letter and digit, such that now one may use greek, skalberg parents: diff changeset	21	echo
0cab06e3bbd0 Extended the notion of letter and digit, such that now one may use greek, skalberg parents: diff changeset	22	echo " Renames old versions of FILES by appending \"~~\"."
0cab06e3bbd0 Extended the notion of letter and digit, such that now one may use greek, skalberg parents: diff changeset	23	echo
0cab06e3bbd0 Extended the notion of letter and digit, such that now one may use greek, skalberg parents: diff changeset	24	exit 1
0cab06e3bbd0 Extended the notion of letter and digit, such that now one may use greek, skalberg parents: diff changeset	25	}
0cab06e3bbd0 Extended the notion of letter and digit, such that now one may use greek, skalberg parents: diff changeset	26
0cab06e3bbd0 Extended the notion of letter and digit, such that now one may use greek, skalberg parents: diff changeset	27
0cab06e3bbd0 Extended the notion of letter and digit, such that now one may use greek, skalberg parents: diff changeset	28	## process command line
0cab06e3bbd0 Extended the notion of letter and digit, such that now one may use greek, skalberg parents: diff changeset	29
0cab06e3bbd0 Extended the notion of letter and digit, such that now one may use greek, skalberg parents: diff changeset	30	[ "$#" -eq 0 -o "$1" = "-?" ] && usage
0cab06e3bbd0 Extended the notion of letter and digit, such that now one may use greek, skalberg parents: diff changeset	31
0cab06e3bbd0 Extended the notion of letter and digit, such that now one may use greek, skalberg parents: diff changeset	32	SPECS="$@"; shift "$#"
0cab06e3bbd0 Extended the notion of letter and digit, such that now one may use greek, skalberg parents: diff changeset	33
0cab06e3bbd0 Extended the notion of letter and digit, such that now one may use greek, skalberg parents: diff changeset	34
0cab06e3bbd0 Extended the notion of letter and digit, such that now one may use greek, skalberg parents: diff changeset	35	## main
0cab06e3bbd0 Extended the notion of letter and digit, such that now one may use greek, skalberg parents: diff changeset	36
0cab06e3bbd0 Extended the notion of letter and digit, such that now one may use greek, skalberg parents: diff changeset	37	#set by configure
15847 c05c7670f166 restored AUTO_BASH/PERL -- beware of ./configure! wenzelm parents: 15574 diff changeset	38	AUTO_PERL=perl
14171 0cab06e3bbd0 Extended the notion of letter and digit, such that now one may use greek, skalberg parents: diff changeset	39
0cab06e3bbd0 Extended the notion of letter and digit, such that now one may use greek, skalberg parents: diff changeset	40	find $SPECS -name \*.thy -print \| xargs "$AUTO_PERL" -w "$ISABELLE_HOME/lib/scripts/fixgreek.pl"
0cab06e3bbd0 Extended the notion of letter and digit, such that now one may use greek, skalberg parents: diff changeset	41	find $SPECS -name \*.ML -print \| xargs "$AUTO_PERL" -w "$ISABELLE_HOME/lib/scripts/fixgreek.pl"

author	urbanc
	Thu, 13 Sep 2007 23:58:38 +0200
changeset 24571	a6d0428dea8e
parent 15847	c05c7670f166
permissions	-rwxr-xr-x