# HG changeset patch
# User wenzelm
# Date 1265568852 -3600
# Node ID c844b93dd147eeaf17aca7130aacf5b1b9a35786
# Parent  c839a4c670c695df4c6e93c597f0dc6c4b71865d
modernized perl scripts: prefer standalone executables;

diff -r c839a4c670c6 -r c844b93dd147 lib/Tools/keywords
--- a/lib/Tools/keywords	Sun Feb 07 19:33:34 2010 +0100
+++ b/lib/Tools/keywords	Sun Feb 07 19:54:12 2010 +0100
@@ -66,5 +66,4 @@
     gzip -dc "$LOG"
   fi
   echo
-done | \
-perl -w "$ISABELLE_HOME/lib/scripts/keywords.pl" "$KEYWORDS_NAME" "$SESSIONS"
+done | "$ISABELLE_HOME/lib/scripts/keywords" "$KEYWORDS_NAME" "$SESSIONS"
diff -r c839a4c670c6 -r c844b93dd147 lib/Tools/unsymbolize
--- a/lib/Tools/unsymbolize	Sun Feb 07 19:33:34 2010 +0100
+++ b/lib/Tools/unsymbolize	Sun Feb 07 19:54:12 2010 +0100
@@ -34,4 +34,4 @@
 ## main
 
 find $SPECS \( -name \*.ML -o -name \*.thy \) -print | \
-  xargs perl -w "$ISABELLE_HOME/lib/scripts/unsymbolize.pl"
+  xargs "$ISABELLE_HOME/lib/scripts/unsymbolize"
diff -r c839a4c670c6 -r c844b93dd147 lib/Tools/yxml
--- a/lib/Tools/yxml	Sun Feb 07 19:33:34 2010 +0100
+++ b/lib/Tools/yxml	Sun Feb 07 19:54:12 2010 +0100
@@ -31,4 +31,4 @@
 
 ## main
 
-exec perl -w "$ISABELLE_HOME/lib/scripts/yxml.pl"
+exec "$ISABELLE_HOME/lib/scripts/yxml"
diff -r c839a4c670c6 -r c844b93dd147 lib/scripts/keywords
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/scripts/keywords	Sun Feb 07 19:54:12 2010 +0100
@@ -0,0 +1,124 @@
+#!/usr/bin/env perl
+#
+# Author: Makarius
+#
+# keywords.pl - generate outer syntax keyword files from session logs
+#
+
+use warnings;
+use strict;
+
+
+## arguments
+
+my ($keywords_name, $sessions) = @ARGV;
+
+
+## keywords
+
+my %keywords;
+
+sub set_keyword {
+  my ($name, $kind) = @_;
+  if (defined $keywords{$name} and $keywords{$name} ne $kind and $keywords{$name} ne "minor") {
+    if ($kind ne "minor") {
+      print STDERR "### Inconsistent declaration of keyword \"${name}\": $keywords{$name} vs ${kind}\n";
+      $keywords{$name} = $kind;
+    }
+  } else {
+    $keywords{$name} = $kind;
+  }
+}
+
+sub collect_keywords {
+  while(<STDIN>) {
+    if (m/^Outer syntax keyword:\s*"(.*)"/) {
+      my $name = $1;
+      &set_keyword($name, "minor");
+    }
+    elsif (m/^Outer syntax command:\s*"(.*)"\s*\((.*)\)/) {
+      my $name = $1;
+      my $kind = $2;
+      &set_keyword($name, $kind);
+    }
+  }
+}
+
+
+## Emacs output
+
+sub emacs_output {
+  my @kinds = (
+    "major",
+    "minor",
+    "control",
+    "diag",
+    "theory-begin",
+    "theory-switch",
+    "theory-end",
+    "theory-heading",
+    "theory-decl",
+    "theory-script",
+    "theory-goal",
+    "qed",
+    "qed-block",
+    "qed-global",
+    "proof-heading",
+    "proof-goal",
+    "proof-block",
+    "proof-open",
+    "proof-close",
+    "proof-chain",
+    "proof-decl",
+    "proof-asm",
+    "proof-asm-goal",
+    "proof-script"
+  );
+  my $file = $keywords_name eq "" ? "isar-keywords.el" : "isar-keywords-${keywords_name}.el";
+  open (OUTPUT, "> ${file}") || die "$!";
+  select OUTPUT;
+
+  print ";;\n";
+  print ";; Keyword classification tables for Isabelle/Isar.\n";
+  print ";; Generated from ${sessions}.\n";
+  print ";; *** DO NOT EDIT *** DO NOT EDIT *** DO NOT EDIT ***\n";
+  print ";;\n";
+
+  for my $kind (@kinds) {
+    my @names;
+    for my $name (keys(%keywords)) {
+      if ($kind eq "major" ? $keywords{$name} ne "minor" : $keywords{$name} eq $kind) {
+        if ($kind ne "minor" or $name =~ m/^[A-Za-z0-9_]+$/) {
+          push @names, $name;
+        }
+      }
+    }
+    @names = sort(@names);
+
+    print "\n(defconst isar-keywords-${kind}";
+    print "\n  '(";
+    my $first = 1;
+    for my $name (@names) {
+      $name =~ s/([\.\*\+\?\[\]\^\$])/\\\\$1/g;
+      if ($first) {
+        print "\"${name}\"";
+        $first = 0;
+      }
+      else {
+        print "\n    \"${name}\"";
+      }
+    }
+    print "))\n";
+  }
+  print "\n(provide 'isar-keywords)\n";
+
+  close OUTPUT;
+  select;
+  print STDERR "${file}\n";
+}
+
+
+## main
+
+&collect_keywords();
+&emacs_output();
diff -r c839a4c670c6 -r c844b93dd147 lib/scripts/keywords.pl
--- a/lib/scripts/keywords.pl	Sun Feb 07 19:33:34 2010 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,120 +0,0 @@
-#
-# Author: Makarius
-#
-# keywords.pl - generate outer syntax keyword files from session logs
-#
-
-## arguments
-
-my ($keywords_name, $sessions) = @ARGV;
-
-
-## keywords
-
-my %keywords;
-
-sub set_keyword {
-  my ($name, $kind) = @_;
-  if (defined $keywords{$name} and $keywords{$name} ne $kind and $keywords{$name} ne "minor") {
-    if ($kind ne "minor") {
-      print STDERR "### Inconsistent declaration of keyword \"${name}\": $keywords{$name} vs ${kind}\n";
-      $keywords{$name} = $kind;
-    }
-  } else {
-    $keywords{$name} = $kind;
-  }
-}
-
-sub collect_keywords {
-  while(<STDIN>) {
-    if (m/^Outer syntax keyword:\s*"(.*)"/) {
-      my $name = $1;
-      &set_keyword($name, "minor");
-    }
-    elsif (m/^Outer syntax command:\s*"(.*)"\s*\((.*)\)/) {
-      my $name = $1;
-      my $kind = $2;
-      &set_keyword($name, $kind);
-    }
-  }
-}
-
-
-## Emacs output
-
-sub emacs_output {
-  my @kinds = (
-    "major",
-    "minor",
-    "control",
-    "diag",
-    "theory-begin",
-    "theory-switch",
-    "theory-end",
-    "theory-heading",
-    "theory-decl",
-    "theory-script",
-    "theory-goal",
-    "qed",
-    "qed-block",
-    "qed-global",
-    "proof-heading",
-    "proof-goal",
-    "proof-block",
-    "proof-open",
-    "proof-close",
-    "proof-chain",
-    "proof-decl",
-    "proof-asm",
-    "proof-asm-goal",
-    "proof-script"
-  );
-  my $file = $keywords_name eq "" ? "isar-keywords.el" : "isar-keywords-${keywords_name}.el";
-  open (OUTPUT, "> ${file}") || die "$!";
-  select OUTPUT;
-
-  print ";;\n";
-  print ";; Keyword classification tables for Isabelle/Isar.\n";
-  print ";; Generated from ${sessions}.\n";
-  print ";; *** DO NOT EDIT *** DO NOT EDIT *** DO NOT EDIT ***\n";
-  print ";;\n";
-
-  for my $kind (@kinds) {
-    my @names;
-    for my $name (keys(%keywords)) {
-      if ($kind eq "major" ? $keywords{$name} ne "minor" : $keywords{$name} eq $kind) {
-        if ($kind ne "minor" or $name =~ m/^[A-Za-z0-9_]+$/) {
-          push @names, $name;
-        }
-      }
-    }
-    @names = sort(@names);
-
-    print "\n(defconst isar-keywords-${kind}";
-    print "\n  '(";
-    my $first = 1;
-    for my $name (@names) {
-      $name =~ s/([\.\*\+\?\[\]\^\$])/\\\\$1/g;
-      if ($first) {
-        print "\"${name}\"";
-        $first = 0;
-      }
-      else {
-        print "\n    \"${name}\"";
-      }
-    }
-    print "))\n";
-  }
-  print "\n(provide 'isar-keywords)\n";
-
-  close OUTPUT;
-  select;
-  print STDERR "${file}\n";
-}
-
-
-## main
-
-&collect_keywords();
-&emacs_output();
-
diff -r c839a4c670c6 -r c844b93dd147 lib/scripts/unsymbolize
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/scripts/unsymbolize	Sun Feb 07 19:54:12 2010 +0100
@@ -0,0 +1,65 @@
+#!/usr/bin/env perl
+#
+# Author: Markus Wenzel, TU Muenchen
+#
+# unsymbolize.pl - remove unreadable symbol names from sources
+#
+
+use warnings;
+use strict;
+
+sub unsymbolize {
+    my ($file) = @_;
+
+    open (FILE, $file) || die $!;
+    undef $/; my $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;
+
+    my $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 my $file (@ARGV) {
+  eval { &unsymbolize($file); };
+  if ($@) { print STDERR "*** unsymbolize $file: ", $@, "\n"; }
+}
diff -r c839a4c670c6 -r c844b93dd147 lib/scripts/unsymbolize.pl
--- a/lib/scripts/unsymbolize.pl	Sun Feb 07 19:33:34 2010 +0100
+++ /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"; }
-}
diff -r c839a4c670c6 -r c844b93dd147 lib/scripts/yxml
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/scripts/yxml	Sun Feb 07 19:54:12 2010 +0100
@@ -0,0 +1,37 @@
+#!/usr/bin/env perl
+#
+# Author: Makarius
+#
+# yxml.pl - simple XML to YXML converter
+#
+
+use warnings;
+use strict;
+
+use XML::Parser;
+
+binmode(STDOUT, ":utf8");
+
+sub handle_start {
+  print chr(5), chr(6), $_[1];
+  for (my $i = 2; $i <= $#_; $i++) {
+    print ($i % 2 == 0 ? chr(6) : "=");
+    print $_[$i];
+  }
+  print chr(5);
+}
+
+sub handle_end {
+  print chr(5), chr(6), chr(5);
+}
+
+sub handle_char {
+  print $_[1];
+}
+
+my $parser = new XML::Parser(Handlers =>
+  {Start => \&handle_start,
+    End => \&handle_end,
+    Char => \&handle_char});
+
+$parser->parse(*STDIN) or die $!;
diff -r c839a4c670c6 -r c844b93dd147 lib/scripts/yxml.pl
--- a/lib/scripts/yxml.pl	Sun Feb 07 19:33:34 2010 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,35 +0,0 @@
-#
-# Author: Makarius
-#
-# yxml.pl - simple XML to YXML converter
-#
-
-use strict;
-use XML::Parser;
-
-binmode(STDOUT, ":utf8");
-
-sub handle_start {
-  print chr(5), chr(6), $_[1];
-  for (my $i = 2; $i <= $#_; $i++) {
-    print ($i % 2 == 0 ? chr(6) : "=");
-    print $_[$i];
-  }
-  print chr(5);
-}
-
-sub handle_end {
-  print chr(5), chr(6), chr(5);
-}
-
-sub handle_char {
-  print $_[1];
-}
-
-my $parser = new XML::Parser(Handlers =>
-  {Start => \&handle_start,
-    End => \&handle_end,
-    Char => \&handle_char});
-
-$parser->parse(*STDIN) or die $!;
-