modernized perl scripts: prefer standalone executables;
authorwenzelm
Sun Feb 07 19:54:12 2010 +0100 (2010-02-07)
changeset 35022c844b93dd147
parent 35021 c839a4c670c6
child 35023 16f9877abf0b
modernized perl scripts: prefer standalone executables;
lib/Tools/keywords
lib/Tools/unsymbolize
lib/Tools/yxml
lib/scripts/keywords
lib/scripts/keywords.pl
lib/scripts/unsymbolize
lib/scripts/unsymbolize.pl
lib/scripts/yxml
lib/scripts/yxml.pl
     1.1 --- a/lib/Tools/keywords	Sun Feb 07 19:33:34 2010 +0100
     1.2 +++ b/lib/Tools/keywords	Sun Feb 07 19:54:12 2010 +0100
     1.3 @@ -66,5 +66,4 @@
     1.4      gzip -dc "$LOG"
     1.5    fi
     1.6    echo
     1.7 -done | \
     1.8 -perl -w "$ISABELLE_HOME/lib/scripts/keywords.pl" "$KEYWORDS_NAME" "$SESSIONS"
     1.9 +done | "$ISABELLE_HOME/lib/scripts/keywords" "$KEYWORDS_NAME" "$SESSIONS"
     2.1 --- a/lib/Tools/unsymbolize	Sun Feb 07 19:33:34 2010 +0100
     2.2 +++ b/lib/Tools/unsymbolize	Sun Feb 07 19:54:12 2010 +0100
     2.3 @@ -34,4 +34,4 @@
     2.4  ## main
     2.5  
     2.6  find $SPECS \( -name \*.ML -o -name \*.thy \) -print | \
     2.7 -  xargs perl -w "$ISABELLE_HOME/lib/scripts/unsymbolize.pl"
     2.8 +  xargs "$ISABELLE_HOME/lib/scripts/unsymbolize"
     3.1 --- a/lib/Tools/yxml	Sun Feb 07 19:33:34 2010 +0100
     3.2 +++ b/lib/Tools/yxml	Sun Feb 07 19:54:12 2010 +0100
     3.3 @@ -31,4 +31,4 @@
     3.4  
     3.5  ## main
     3.6  
     3.7 -exec perl -w "$ISABELLE_HOME/lib/scripts/yxml.pl"
     3.8 +exec "$ISABELLE_HOME/lib/scripts/yxml"
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/lib/scripts/keywords	Sun Feb 07 19:54:12 2010 +0100
     4.3 @@ -0,0 +1,124 @@
     4.4 +#!/usr/bin/env perl
     4.5 +#
     4.6 +# Author: Makarius
     4.7 +#
     4.8 +# keywords.pl - generate outer syntax keyword files from session logs
     4.9 +#
    4.10 +
    4.11 +use warnings;
    4.12 +use strict;
    4.13 +
    4.14 +
    4.15 +## arguments
    4.16 +
    4.17 +my ($keywords_name, $sessions) = @ARGV;
    4.18 +
    4.19 +
    4.20 +## keywords
    4.21 +
    4.22 +my %keywords;
    4.23 +
    4.24 +sub set_keyword {
    4.25 +  my ($name, $kind) = @_;
    4.26 +  if (defined $keywords{$name} and $keywords{$name} ne $kind and $keywords{$name} ne "minor") {
    4.27 +    if ($kind ne "minor") {
    4.28 +      print STDERR "### Inconsistent declaration of keyword \"${name}\": $keywords{$name} vs ${kind}\n";
    4.29 +      $keywords{$name} = $kind;
    4.30 +    }
    4.31 +  } else {
    4.32 +    $keywords{$name} = $kind;
    4.33 +  }
    4.34 +}
    4.35 +
    4.36 +sub collect_keywords {
    4.37 +  while(<STDIN>) {
    4.38 +    if (m/^Outer syntax keyword:\s*"(.*)"/) {
    4.39 +      my $name = $1;
    4.40 +      &set_keyword($name, "minor");
    4.41 +    }
    4.42 +    elsif (m/^Outer syntax command:\s*"(.*)"\s*\((.*)\)/) {
    4.43 +      my $name = $1;
    4.44 +      my $kind = $2;
    4.45 +      &set_keyword($name, $kind);
    4.46 +    }
    4.47 +  }
    4.48 +}
    4.49 +
    4.50 +
    4.51 +## Emacs output
    4.52 +
    4.53 +sub emacs_output {
    4.54 +  my @kinds = (
    4.55 +    "major",
    4.56 +    "minor",
    4.57 +    "control",
    4.58 +    "diag",
    4.59 +    "theory-begin",
    4.60 +    "theory-switch",
    4.61 +    "theory-end",
    4.62 +    "theory-heading",
    4.63 +    "theory-decl",
    4.64 +    "theory-script",
    4.65 +    "theory-goal",
    4.66 +    "qed",
    4.67 +    "qed-block",
    4.68 +    "qed-global",
    4.69 +    "proof-heading",
    4.70 +    "proof-goal",
    4.71 +    "proof-block",
    4.72 +    "proof-open",
    4.73 +    "proof-close",
    4.74 +    "proof-chain",
    4.75 +    "proof-decl",
    4.76 +    "proof-asm",
    4.77 +    "proof-asm-goal",
    4.78 +    "proof-script"
    4.79 +  );
    4.80 +  my $file = $keywords_name eq "" ? "isar-keywords.el" : "isar-keywords-${keywords_name}.el";
    4.81 +  open (OUTPUT, "> ${file}") || die "$!";
    4.82 +  select OUTPUT;
    4.83 +
    4.84 +  print ";;\n";
    4.85 +  print ";; Keyword classification tables for Isabelle/Isar.\n";
    4.86 +  print ";; Generated from ${sessions}.\n";
    4.87 +  print ";; *** DO NOT EDIT *** DO NOT EDIT *** DO NOT EDIT ***\n";
    4.88 +  print ";;\n";
    4.89 +
    4.90 +  for my $kind (@kinds) {
    4.91 +    my @names;
    4.92 +    for my $name (keys(%keywords)) {
    4.93 +      if ($kind eq "major" ? $keywords{$name} ne "minor" : $keywords{$name} eq $kind) {
    4.94 +        if ($kind ne "minor" or $name =~ m/^[A-Za-z0-9_]+$/) {
    4.95 +          push @names, $name;
    4.96 +        }
    4.97 +      }
    4.98 +    }
    4.99 +    @names = sort(@names);
   4.100 +
   4.101 +    print "\n(defconst isar-keywords-${kind}";
   4.102 +    print "\n  '(";
   4.103 +    my $first = 1;
   4.104 +    for my $name (@names) {
   4.105 +      $name =~ s/([\.\*\+\?\[\]\^\$])/\\\\$1/g;
   4.106 +      if ($first) {
   4.107 +        print "\"${name}\"";
   4.108 +        $first = 0;
   4.109 +      }
   4.110 +      else {
   4.111 +        print "\n    \"${name}\"";
   4.112 +      }
   4.113 +    }
   4.114 +    print "))\n";
   4.115 +  }
   4.116 +  print "\n(provide 'isar-keywords)\n";
   4.117 +
   4.118 +  close OUTPUT;
   4.119 +  select;
   4.120 +  print STDERR "${file}\n";
   4.121 +}
   4.122 +
   4.123 +
   4.124 +## main
   4.125 +
   4.126 +&collect_keywords();
   4.127 +&emacs_output();
     5.1 --- a/lib/scripts/keywords.pl	Sun Feb 07 19:33:34 2010 +0100
     5.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.3 @@ -1,120 +0,0 @@
     5.4 -#
     5.5 -# Author: Makarius
     5.6 -#
     5.7 -# keywords.pl - generate outer syntax keyword files from session logs
     5.8 -#
     5.9 -
    5.10 -## arguments
    5.11 -
    5.12 -my ($keywords_name, $sessions) = @ARGV;
    5.13 -
    5.14 -
    5.15 -## keywords
    5.16 -
    5.17 -my %keywords;
    5.18 -
    5.19 -sub set_keyword {
    5.20 -  my ($name, $kind) = @_;
    5.21 -  if (defined $keywords{$name} and $keywords{$name} ne $kind and $keywords{$name} ne "minor") {
    5.22 -    if ($kind ne "minor") {
    5.23 -      print STDERR "### Inconsistent declaration of keyword \"${name}\": $keywords{$name} vs ${kind}\n";
    5.24 -      $keywords{$name} = $kind;
    5.25 -    }
    5.26 -  } else {
    5.27 -    $keywords{$name} = $kind;
    5.28 -  }
    5.29 -}
    5.30 -
    5.31 -sub collect_keywords {
    5.32 -  while(<STDIN>) {
    5.33 -    if (m/^Outer syntax keyword:\s*"(.*)"/) {
    5.34 -      my $name = $1;
    5.35 -      &set_keyword($name, "minor");
    5.36 -    }
    5.37 -    elsif (m/^Outer syntax command:\s*"(.*)"\s*\((.*)\)/) {
    5.38 -      my $name = $1;
    5.39 -      my $kind = $2;
    5.40 -      &set_keyword($name, $kind);
    5.41 -    }
    5.42 -  }
    5.43 -}
    5.44 -
    5.45 -
    5.46 -## Emacs output
    5.47 -
    5.48 -sub emacs_output {
    5.49 -  my @kinds = (
    5.50 -    "major",
    5.51 -    "minor",
    5.52 -    "control",
    5.53 -    "diag",
    5.54 -    "theory-begin",
    5.55 -    "theory-switch",
    5.56 -    "theory-end",
    5.57 -    "theory-heading",
    5.58 -    "theory-decl",
    5.59 -    "theory-script",
    5.60 -    "theory-goal",
    5.61 -    "qed",
    5.62 -    "qed-block",
    5.63 -    "qed-global",
    5.64 -    "proof-heading",
    5.65 -    "proof-goal",
    5.66 -    "proof-block",
    5.67 -    "proof-open",
    5.68 -    "proof-close",
    5.69 -    "proof-chain",
    5.70 -    "proof-decl",
    5.71 -    "proof-asm",
    5.72 -    "proof-asm-goal",
    5.73 -    "proof-script"
    5.74 -  );
    5.75 -  my $file = $keywords_name eq "" ? "isar-keywords.el" : "isar-keywords-${keywords_name}.el";
    5.76 -  open (OUTPUT, "> ${file}") || die "$!";
    5.77 -  select OUTPUT;
    5.78 -
    5.79 -  print ";;\n";
    5.80 -  print ";; Keyword classification tables for Isabelle/Isar.\n";
    5.81 -  print ";; Generated from ${sessions}.\n";
    5.82 -  print ";; *** DO NOT EDIT *** DO NOT EDIT *** DO NOT EDIT ***\n";
    5.83 -  print ";;\n";
    5.84 -
    5.85 -  for my $kind (@kinds) {
    5.86 -    my @names;
    5.87 -    for my $name (keys(%keywords)) {
    5.88 -      if ($kind eq "major" ? $keywords{$name} ne "minor" : $keywords{$name} eq $kind) {
    5.89 -        if ($kind ne "minor" or $name =~ m/^[A-Za-z0-9_]+$/) {
    5.90 -          push @names, $name;
    5.91 -        }
    5.92 -      }
    5.93 -    }
    5.94 -    @names = sort(@names);
    5.95 -
    5.96 -    print "\n(defconst isar-keywords-${kind}";
    5.97 -    print "\n  '(";
    5.98 -    my $first = 1;
    5.99 -    for my $name (@names) {
   5.100 -      $name =~ s/([\.\*\+\?\[\]\^\$])/\\\\$1/g;
   5.101 -      if ($first) {
   5.102 -        print "\"${name}\"";
   5.103 -        $first = 0;
   5.104 -      }
   5.105 -      else {
   5.106 -        print "\n    \"${name}\"";
   5.107 -      }
   5.108 -    }
   5.109 -    print "))\n";
   5.110 -  }
   5.111 -  print "\n(provide 'isar-keywords)\n";
   5.112 -
   5.113 -  close OUTPUT;
   5.114 -  select;
   5.115 -  print STDERR "${file}\n";
   5.116 -}
   5.117 -
   5.118 -
   5.119 -## main
   5.120 -
   5.121 -&collect_keywords();
   5.122 -&emacs_output();
   5.123 -
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/lib/scripts/unsymbolize	Sun Feb 07 19:54:12 2010 +0100
     6.3 @@ -0,0 +1,65 @@
     6.4 +#!/usr/bin/env perl
     6.5 +#
     6.6 +# Author: Markus Wenzel, TU Muenchen
     6.7 +#
     6.8 +# unsymbolize.pl - remove unreadable symbol names from sources
     6.9 +#
    6.10 +
    6.11 +use warnings;
    6.12 +use strict;
    6.13 +
    6.14 +sub unsymbolize {
    6.15 +    my ($file) = @_;
    6.16 +
    6.17 +    open (FILE, $file) || die $!;
    6.18 +    undef $/; my $text = <FILE>; $/ = "\n";         # slurp whole file
    6.19 +    close FILE || die $!;
    6.20 +
    6.21 +    $_ = $text;
    6.22 +
    6.23 +    # Pure
    6.24 +    s/\\?\\<And>/!!/g;
    6.25 +    s/\\?\\<Colon>/::/g;
    6.26 +    s/\\?\\<Longrightarrow>/==>/g;
    6.27 +    s/\\?\\<Midarrow>\\?\\<Rightarrow>/==>/g;
    6.28 +    s/\\?\\<Rightarrow>/=>/g;
    6.29 +    s/\\?\\<equiv>/==/g;
    6.30 +    s/\\?\\<dots>/.../g;
    6.31 +    s/\\?\\<lbrakk> ?/[| /g;
    6.32 +    s/\\?\\ ?<rbrakk>/ |]/g;
    6.33 +    s/\\?\\<lparr> ?/(| /g;
    6.34 +    s/\\?\\ ?<rparr>/ |)/g;
    6.35 +    # HOL
    6.36 +    s/\\?\\<longleftrightarrow>/<->/g;
    6.37 +    s/\\?\\<longrightarrow>/-->/g;
    6.38 +    s/\\?\\<midarrow>\\?\\<rightarrow>/-->/g;
    6.39 +    s/\\?\\<rightarrow>/->/g;
    6.40 +    s/\\?\\<not>/~/g;
    6.41 +    s/\\?\\<notin>/~:/g;
    6.42 +    s/\\?\\<noteq>/~=/g;
    6.43 +    s/\\?\\<some> ?/SOME /g;
    6.44 +    # outer syntax
    6.45 +    s/\\?\\<rightleftharpoons>/==/g;
    6.46 +    s/\\?\\<rightharpoonup>/=>/g;
    6.47 +    s/\\?\\<leftharpoondown>/<=/g;
    6.48 +
    6.49 +    my $result = $_;
    6.50 +
    6.51 +    if ($text ne $result) {
    6.52 +	print STDERR "fixing $file\n";
    6.53 +        if (! -f "$file~~") {
    6.54 +	    rename $file, "$file~~" || die $!;
    6.55 +        }
    6.56 +	open (FILE, "> $file") || die $!;
    6.57 +	print FILE $result;
    6.58 +	close FILE || die $!;
    6.59 +    }
    6.60 +}
    6.61 +
    6.62 +
    6.63 +## main
    6.64 +
    6.65 +foreach my $file (@ARGV) {
    6.66 +  eval { &unsymbolize($file); };
    6.67 +  if ($@) { print STDERR "*** unsymbolize $file: ", $@, "\n"; }
    6.68 +}
     7.1 --- a/lib/scripts/unsymbolize.pl	Sun Feb 07 19:33:34 2010 +0100
     7.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.3 @@ -1,61 +0,0 @@
     7.4 -#
     7.5 -# Author: Markus Wenzel, TU Muenchen
     7.6 -#
     7.7 -# unsymbolize.pl - remove unreadable symbol names from sources
     7.8 -#
     7.9 -
    7.10 -sub unsymbolize {
    7.11 -    my ($file) = @_;
    7.12 -
    7.13 -    open (FILE, $file) || die $!;
    7.14 -    undef $/; $text = <FILE>; $/ = "\n";         # slurp whole file
    7.15 -    close FILE || die $!;
    7.16 -
    7.17 -    $_ = $text;
    7.18 -
    7.19 -    # Pure
    7.20 -    s/\\?\\<And>/!!/g;
    7.21 -    s/\\?\\<Colon>/::/g;
    7.22 -    s/\\?\\<Longrightarrow>/==>/g;
    7.23 -    s/\\?\\<Midarrow>\\?\\<Rightarrow>/==>/g;
    7.24 -    s/\\?\\<Rightarrow>/=>/g;
    7.25 -    s/\\?\\<equiv>/==/g;
    7.26 -    s/\\?\\<dots>/.../g;
    7.27 -    s/\\?\\<lbrakk> ?/[| /g;
    7.28 -    s/\\?\\ ?<rbrakk>/ |]/g;
    7.29 -    s/\\?\\<lparr> ?/(| /g;
    7.30 -    s/\\?\\ ?<rparr>/ |)/g;
    7.31 -    # HOL
    7.32 -    s/\\?\\<longleftrightarrow>/<->/g;
    7.33 -    s/\\?\\<longrightarrow>/-->/g;
    7.34 -    s/\\?\\<midarrow>\\?\\<rightarrow>/-->/g;
    7.35 -    s/\\?\\<rightarrow>/->/g;
    7.36 -    s/\\?\\<not>/~/g;
    7.37 -    s/\\?\\<notin>/~:/g;
    7.38 -    s/\\?\\<noteq>/~=/g;
    7.39 -    s/\\?\\<some> ?/SOME /g;
    7.40 -    # outer syntax
    7.41 -    s/\\?\\<rightleftharpoons>/==/g;
    7.42 -    s/\\?\\<rightharpoonup>/=>/g;
    7.43 -    s/\\?\\<leftharpoondown>/<=/g;
    7.44 -
    7.45 -    $result = $_;
    7.46 -
    7.47 -    if ($text ne $result) {
    7.48 -	print STDERR "fixing $file\n";
    7.49 -        if (! -f "$file~~") {
    7.50 -	    rename $file, "$file~~" || die $!;
    7.51 -        }
    7.52 -	open (FILE, "> $file") || die $!;
    7.53 -	print FILE $result;
    7.54 -	close FILE || die $!;
    7.55 -    }
    7.56 -}
    7.57 -
    7.58 -
    7.59 -## main
    7.60 -
    7.61 -foreach $file (@ARGV) {
    7.62 -  eval { &unsymbolize($file); };
    7.63 -  if ($@) { print STDERR "*** unsymbolize $file: ", $@, "\n"; }
    7.64 -}
     8.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.2 +++ b/lib/scripts/yxml	Sun Feb 07 19:54:12 2010 +0100
     8.3 @@ -0,0 +1,37 @@
     8.4 +#!/usr/bin/env perl
     8.5 +#
     8.6 +# Author: Makarius
     8.7 +#
     8.8 +# yxml.pl - simple XML to YXML converter
     8.9 +#
    8.10 +
    8.11 +use warnings;
    8.12 +use strict;
    8.13 +
    8.14 +use XML::Parser;
    8.15 +
    8.16 +binmode(STDOUT, ":utf8");
    8.17 +
    8.18 +sub handle_start {
    8.19 +  print chr(5), chr(6), $_[1];
    8.20 +  for (my $i = 2; $i <= $#_; $i++) {
    8.21 +    print ($i % 2 == 0 ? chr(6) : "=");
    8.22 +    print $_[$i];
    8.23 +  }
    8.24 +  print chr(5);
    8.25 +}
    8.26 +
    8.27 +sub handle_end {
    8.28 +  print chr(5), chr(6), chr(5);
    8.29 +}
    8.30 +
    8.31 +sub handle_char {
    8.32 +  print $_[1];
    8.33 +}
    8.34 +
    8.35 +my $parser = new XML::Parser(Handlers =>
    8.36 +  {Start => \&handle_start,
    8.37 +    End => \&handle_end,
    8.38 +    Char => \&handle_char});
    8.39 +
    8.40 +$parser->parse(*STDIN) or die $!;
     9.1 --- a/lib/scripts/yxml.pl	Sun Feb 07 19:33:34 2010 +0100
     9.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.3 @@ -1,35 +0,0 @@
     9.4 -#
     9.5 -# Author: Makarius
     9.6 -#
     9.7 -# yxml.pl - simple XML to YXML converter
     9.8 -#
     9.9 -
    9.10 -use strict;
    9.11 -use XML::Parser;
    9.12 -
    9.13 -binmode(STDOUT, ":utf8");
    9.14 -
    9.15 -sub handle_start {
    9.16 -  print chr(5), chr(6), $_[1];
    9.17 -  for (my $i = 2; $i <= $#_; $i++) {
    9.18 -    print ($i % 2 == 0 ? chr(6) : "=");
    9.19 -    print $_[$i];
    9.20 -  }
    9.21 -  print chr(5);
    9.22 -}
    9.23 -
    9.24 -sub handle_end {
    9.25 -  print chr(5), chr(6), chr(5);
    9.26 -}
    9.27 -
    9.28 -sub handle_char {
    9.29 -  print $_[1];
    9.30 -}
    9.31 -
    9.32 -my $parser = new XML::Parser(Handlers =>
    9.33 -  {Start => \&handle_start,
    9.34 -    End => \&handle_end,
    9.35 -    Char => \&handle_char});
    9.36 -
    9.37 -$parser->parse(*STDIN) or die $!;
    9.38 -