--- a/lib/scripts/unsymbolize.pl Mon Feb 08 15:49:01 2010 -0800
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,61 +0,0 @@
-#
-# Author: Markus Wenzel, TU Muenchen
-#
-# unsymbolize.pl - remove unreadable symbol names from sources
-#
-
-sub unsymbolize {
- my ($file) = @_;
-
- open (FILE, $file) || die $!;
- undef $/; $text = <FILE>; $/ = "\n"; # slurp whole file
- close FILE || die $!;
-
- $_ = $text;
-
- # Pure
- s/\\?\\<And>/!!/g;
- s/\\?\\<Colon>/::/g;
- s/\\?\\<Longrightarrow>/==>/g;
- s/\\?\\<Midarrow>\\?\\<Rightarrow>/==>/g;
- s/\\?\\<Rightarrow>/=>/g;
- s/\\?\\<equiv>/==/g;
- s/\\?\\<dots>/.../g;
- s/\\?\\<lbrakk> ?/[| /g;
- s/\\?\\ ?<rbrakk>/ |]/g;
- s/\\?\\<lparr> ?/(| /g;
- s/\\?\\ ?<rparr>/ |)/g;
- # HOL
- s/\\?\\<longleftrightarrow>/<->/g;
- s/\\?\\<longrightarrow>/-->/g;
- s/\\?\\<midarrow>\\?\\<rightarrow>/-->/g;
- s/\\?\\<rightarrow>/->/g;
- s/\\?\\<not>/~/g;
- s/\\?\\<notin>/~:/g;
- s/\\?\\<noteq>/~=/g;
- s/\\?\\<some> ?/SOME /g;
- # outer syntax
- s/\\?\\<rightleftharpoons>/==/g;
- s/\\?\\<rightharpoonup>/=>/g;
- s/\\?\\<leftharpoondown>/<=/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 { &unsymbolize($file); };
- if ($@) { print STDERR "*** unsymbolize $file: ", $@, "\n"; }
-}