--- 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"
--- 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"
--- 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"
--- /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();
--- 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();
-
--- /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"; }
+}
--- 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"; }
-}
--- /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 $!;
--- 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 $!;
-