lib/scripts/unsymbolize.pl
author wenzelm
Sun, 15 Oct 2000 19:50:35 +0200
changeset 10220 2a726de6e124
parent 10071 ff08faf26d58
child 10506 01333dbe1431
permissions -rw-r--r--
proper symbol markup with \isamath, \isatext; support sub/super scripts:
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
10026
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
     1
#
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
     2
# $Id$
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
     3
# Author: Markus Wenzel, TU Muenchen
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
     4
# License: GPL (GNU GENERAL PUBLIC LICENSE)
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
     5
#
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
     6
# unsymbolize.pl - remove unreadable symbol names from sources
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
     7
#
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
     8
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
     9
sub unsymbolize {
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
    10
    my ($file) = @_;
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
    11
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
    12
    open (FILE, $file) || die $!;
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
    13
    undef $/; $text = <FILE>; $/ = "\n";         # slurp whole file
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
    14
    close FILE || die $!;
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
    15
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
    16
    $_ = $text;
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
    17
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
    18
    # Pure
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
    19
    s/\\?\\<And>/!!/g;
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
    20
    s/\\?\\<Colon>/::/g;
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
    21
    s/\\?\\<Longrightarrow>/==>/g;
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
    22
    s/\\?\\<Midarrow>\\?\\<Rightarrow>/==>/g;
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
    23
    s/\\?\\<Rightarrow>/=>/g;
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
    24
    s/\\?\\<equiv>/==/g;
10071
ff08faf26d58 tuned replacements;
wenzelm
parents: 10026
diff changeset
    25
    s/\\?\\<lbrakk> ?/[| /g;
ff08faf26d58 tuned replacements;
wenzelm
parents: 10026
diff changeset
    26
    s/\\?\\ ?<rbrakk>/ |]/g;
ff08faf26d58 tuned replacements;
wenzelm
parents: 10026
diff changeset
    27
    s/\\?\\<lparr> ?/(| /g;
ff08faf26d58 tuned replacements;
wenzelm
parents: 10026
diff changeset
    28
    s/\\?\\ ?<rparr>/ |)/g;
10026
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
    29
    # HOL
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
    30
    s/\\?\\<longrightarrow>/-->/g;
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
    31
    s/\\?\\<midarrow>\\?\\<rightarrow>/-->/g;
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
    32
    s/\\?\\<rightarrow>/->/g;
10071
ff08faf26d58 tuned replacements;
wenzelm
parents: 10026
diff changeset
    33
    s/\\?\\<epsilon> ?/SOME /g;
10026
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
    34
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
    35
    $result = $_;
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
    36
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
    37
    if ($text ne $result) {
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
    38
	print STDERR "fixing $file\n";
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
    39
        if (! -f "$file~~") {
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
    40
	    rename $file, "$file~~" || die $!;
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
    41
        }
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
    42
	open (FILE, "> $file") || die $!;
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
    43
	print FILE $result;
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
    44
	close FILE || die $!;
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
    45
    }
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
    46
}
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
    47
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
    48
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
    49
## main
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
    50
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
    51
foreach $file (@ARGV) {
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
    52
  eval { &unsymbolize($file); };
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
    53
  if ($@) { print STDERR "*** unsymbolize $file: ", $@, "\n"; }
dfa85ba2295a remove unreadable symbol names from sources;
wenzelm
parents:
diff changeset
    54
}