lib/scripts/unsymbolize.pl
changeset 10071 ff08faf26d58
parent 10026 dfa85ba2295a
child 10506 01333dbe1431
equal deleted inserted replaced
10070:fefb958b52aa 10071:ff08faf26d58
    20     s/\\?\\<Colon>/::/g;
    20     s/\\?\\<Colon>/::/g;
    21     s/\\?\\<Longrightarrow>/==>/g;
    21     s/\\?\\<Longrightarrow>/==>/g;
    22     s/\\?\\<Midarrow>\\?\\<Rightarrow>/==>/g;
    22     s/\\?\\<Midarrow>\\?\\<Rightarrow>/==>/g;
    23     s/\\?\\<Rightarrow>/=>/g;
    23     s/\\?\\<Rightarrow>/=>/g;
    24     s/\\?\\<equiv>/==/g;
    24     s/\\?\\<equiv>/==/g;
    25     s/\\?\\<lbrakk>/[|/g;
    25     s/\\?\\<lbrakk> ?/[| /g;
    26     s/\\?\\<rbrakk>/|]/g;
    26     s/\\?\\ ?<rbrakk>/ |]/g;
       
    27     s/\\?\\<lparr> ?/(| /g;
       
    28     s/\\?\\ ?<rparr>/ |)/g;
    27     # HOL
    29     # HOL
    28     s/\\?\\<longrightarrow>/-->/g;
    30     s/\\?\\<longrightarrow>/-->/g;
    29     s/\\?\\<midarrow>\\?\\<rightarrow>/-->/g;
    31     s/\\?\\<midarrow>\\?\\<rightarrow>/-->/g;
    30     s/\\?\\<rightarrow>/->/g;
    32     s/\\?\\<rightarrow>/->/g;
    31     s/\\?\\<epsilon>\s*/SOME /g;
    33     s/\\?\\<epsilon> ?/SOME /g;
    32 
    34 
    33     $result = $_;
    35     $result = $_;
    34 
    36 
    35     if ($text ne $result) {
    37     if ($text ne $result) {
    36 	print STDERR "fixing $file\n";
    38 	print STDERR "fixing $file\n";