1.1 --- a/lib/scripts/keywords.pl	Mon Feb 08 15:49:01 2010 -0800
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,120 +0,0 @@
     1.4 -#
     1.5 -# Author: Makarius
     1.6 -#
     1.7 -# keywords.pl - generate outer syntax keyword files from session logs
     1.8 -#
     1.9 -
    1.10 -## arguments
    1.11 -
    1.12 -my ($keywords_name, $sessions) = @ARGV;
    1.13 -
    1.14 -
    1.15 -## keywords
    1.16 -
    1.17 -my %keywords;
    1.18 -
    1.19 -sub set_keyword {
    1.20 -  my ($name, $kind) = @_;
    1.21 -  if (defined $keywords{$name} and $keywords{$name} ne $kind and $keywords{$name} ne "minor") {
    1.22 -    if ($kind ne "minor") {
    1.23 -      print STDERR "### Inconsistent declaration of keyword \"${name}\": $keywords{$name} vs ${kind}\n";
    1.24 -      $keywords{$name} = $kind;
    1.25 -    }
    1.26 -  } else {
    1.27 -    $keywords{$name} = $kind;
    1.28 -  }
    1.29 -}
    1.30 -
    1.31 -sub collect_keywords {
    1.32 -  while(<STDIN>) {
    1.33 -    if (m/^Outer syntax keyword:\s*"(.*)"/) {
    1.34 -      my $name = $1;
    1.35 -      &set_keyword($name, "minor");
    1.36 -    }
    1.37 -    elsif (m/^Outer syntax command:\s*"(.*)"\s*\((.*)\)/) {
    1.38 -      my $name = $1;
    1.39 -      my $kind = $2;
    1.40 -      &set_keyword($name, $kind);
    1.41 -    }
    1.42 -  }
    1.43 -}
    1.44 -
    1.45 -
    1.46 -## Emacs output
    1.47 -
    1.48 -sub emacs_output {
    1.49 -  my @kinds = (
    1.50 -    "major",
    1.51 -    "minor",
    1.52 -    "control",
    1.53 -    "diag",
    1.54 -    "theory-begin",
    1.55 -    "theory-switch",
    1.56 -    "theory-end",
    1.57 -    "theory-heading",
    1.58 -    "theory-decl",
    1.59 -    "theory-script",
    1.60 -    "theory-goal",
    1.61 -    "qed",
    1.62 -    "qed-block",
    1.63 -    "qed-global",
    1.64 -    "proof-heading",
    1.65 -    "proof-goal",
    1.66 -    "proof-block",
    1.67 -    "proof-open",
    1.68 -    "proof-close",
    1.69 -    "proof-chain",
    1.70 -    "proof-decl",
    1.71 -    "proof-asm",
    1.72 -    "proof-asm-goal",
    1.73 -    "proof-script"
    1.74 -  );
    1.75 -  my $file = $keywords_name eq "" ? "isar-keywords.el" : "isar-keywords-${keywords_name}.el";
    1.76 -  open (OUTPUT, "> ${file}") || die "$!";
    1.77 -  select OUTPUT;
    1.78 -
    1.79 -  print ";;\n";
    1.80 -  print ";; Keyword classification tables for Isabelle/Isar.\n";
    1.81 -  print ";; Generated from ${sessions}.\n";
    1.82 -  print ";; *** DO NOT EDIT *** DO NOT EDIT *** DO NOT EDIT ***\n";
    1.83 -  print ";;\n";
    1.84 -
    1.85 -  for my $kind (@kinds) {
    1.86 -    my @names;
    1.87 -    for my $name (keys(%keywords)) {
    1.88 -      if ($kind eq "major" ? $keywords{$name} ne "minor" : $keywords{$name} eq $kind) {
    1.89 -        if ($kind ne "minor" or $name =~ m/^[A-Za-z0-9_]+$/) {
    1.90 -          push @names, $name;
    1.91 -        }
    1.92 -      }
    1.93 -    }
    1.94 -    @names = sort(@names);
    1.95 -
    1.96 -    print "\n(defconst isar-keywords-${kind}";
    1.97 -    print "\n  '(";
    1.98 -    my $first = 1;
    1.99 -    for my $name (@names) {
   1.100 -      $name =~ s/([\.\*\+\?\[\]\^\$])/\\\\$1/g;
   1.101 -      if ($first) {
   1.102 -        print "\"${name}\"";
   1.103 -        $first = 0;
   1.104 -      }
   1.105 -      else {
   1.106 -        print "\n    \"${name}\"";
   1.107 -      }
   1.108 -    }
   1.109 -    print "))\n";
   1.110 -  }
   1.111 -  print "\n(provide 'isar-keywords)\n";
   1.112 -
   1.113 -  close OUTPUT;
   1.114 -  select;
   1.115 -  print STDERR "${file}\n";
   1.116 -}
   1.117 -
   1.118 -
   1.119 -## main
   1.120 -
   1.121 -&collect_keywords();
   1.122 -&emacs_output();
   1.123 -