diff -r e1afb42be5ad -r 9188d901209d lib/scripts/unsymbolize --- a/lib/scripts/unsymbolize Fri Jun 27 19:21:58 2014 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,64 +0,0 @@ -#!/usr/bin/env perl -# -# Author: Markus Wenzel, TU Muenchen -# -# unsymbolize - remove unreadable symbol names from sources - -use warnings; -use strict; - -sub unsymbolize { - my ($file) = @_; - - open (FILE, $file) || die $!; - undef $/; my $text = ; $/ = "\n"; # slurp whole file - close FILE || die $!; - - $_ = $text; - - # Pure - s/\\?\\/!!/g; - s/\\?\\/::/g; - s/\\?\\/==>/g; - s/\\?\\\\?\\/==>/g; - s/\\?\\/=>/g; - s/\\?\\/==/g; - s/\\?\\/.../g; - s/\\?\\ ?/[| /g; - s/\\?\\ ?/ |]/g; - s/\\?\\ ?/(| /g; - s/\\?\\ ?/ |)/g; - # HOL - s/\\?\\/<->/g; - s/\\?\\/-->/g; - s/\\?\\\\?\\/-->/g; - s/\\?\\/->/g; - s/\\?\\/~/g; - s/\\?\\/~:/g; - s/\\?\\/~=/g; - s/\\?\\ ?/SOME /g; - # outer syntax - s/\\?\\/==/g; - s/\\?\\/=>/g; - s/\\?\\/<=/g; - - my $result = $_; - - if ($text ne $result) { - print STDERR "changing $file\n"; - if (! -f "$file~~") { - rename $file, "$file~~" || die $!; - } - open (FILE, "> $file") || die $!; - print FILE $result; - close FILE || die $!; - } -} - - -## main - -foreach my $file (@ARGV) { - eval { &unsymbolize($file); }; - if ($@) { print STDERR "*** unsymbolize $file: ", $@, "\n"; } -}