diff -r 7b5a5116f3af -r 4cf3f6153eb8 lib/scripts/keywords
--- a/lib/scripts/keywords	Mon Jun 24 17:17:17 2013 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,153 +0,0 @@
-#!/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;
-  }
-}
-
-my %convert_kinds = (
-  "thy_begin" => "theory-begin",
-  "thy_end" => "theory-end",
-  "thy_heading1" => "theory-heading",
-  "thy_heading2" => "theory-heading",
-  "thy_heading3" => "theory-heading",
-  "thy_heading4" => "theory-heading",
-  "thy_load" => "theory-decl",
-  "thy_decl" => "theory-decl",
-  "thy_script" => "theory-script",
-  "thy_goal" => "theory-goal",
-  "qed_block" => "qed-block",
-  "qed_global" => "qed-global",
-  "prf_heading2" => "proof-heading",
-  "prf_heading3" => "proof-heading",
-  "prf_heading4" => "proof-heading",
-  "prf_goal" => "proof-goal",
-  "prf_block" => "proof-block",
-  "prf_open" => "proof-open",
-  "prf_close" => "proof-close",
-  "prf_chain" => "proof-chain",
-  "prf_decl" => "proof-decl",
-  "prf_asm" => "proof-asm",
-  "prf_asm_goal" => "proof-asm-goal",
-  "prf_script" => "proof-script"
-);
-
-my @emacs_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"
-);
-
-sub collect_keywords {
-  while(<STDIN>) {
-    if (m/^\fOuter syntax keyword "([^"]*)" :: (\S*)/) {
-      my $name = $1;
-      my $kind = $2;
-      if (defined $convert_kinds{$kind}) { $kind = $convert_kinds{$kind} }
-      &set_keyword($name, $kind);
-    }
-    elsif (m/^\fOuter syntax keyword "([^"]*)"/) {
-      my $name = $1;
-      &set_keyword($name, "minor");
-    }
-  }
-}
-
-
-## Emacs output
-
-sub emacs_output {
-  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 (@emacs_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();