lib/scripts/keywords
author wenzelm
Thu May 20 20:20:52 2010 +0200 (2010-05-20)
changeset 37012 106c56e916f8
parent 36316 f9b45eac4c60
child 46967 499d9bbd8de9
permissions -rwxr-xr-x
enable shell script editor mode;
wenzelm@35022
     1
#!/usr/bin/env perl
wenzelm@24875
     2
#
wenzelm@24875
     3
# Author: Makarius
wenzelm@24875
     4
#
wenzelm@24875
     5
# keywords.pl - generate outer syntax keyword files from session logs
wenzelm@24875
     6
#
wenzelm@24875
     7
wenzelm@35022
     8
use warnings;
wenzelm@35022
     9
use strict;
wenzelm@35022
    10
wenzelm@35022
    11
wenzelm@24886
    12
## arguments
wenzelm@24875
    13
wenzelm@33684
    14
my ($keywords_name, $sessions) = @ARGV;
wenzelm@24875
    15
wenzelm@24875
    16
wenzelm@24875
    17
## keywords
wenzelm@24875
    18
wenzelm@24875
    19
my %keywords;
wenzelm@24875
    20
wenzelm@24875
    21
sub set_keyword {
wenzelm@24875
    22
  my ($name, $kind) = @_;
wenzelm@27386
    23
  if (defined $keywords{$name} and $keywords{$name} ne $kind and $keywords{$name} ne "minor") {
wenzelm@27386
    24
    if ($kind ne "minor") {
wenzelm@27386
    25
      print STDERR "### Inconsistent declaration of keyword \"${name}\": $keywords{$name} vs ${kind}\n";
wenzelm@27386
    26
      $keywords{$name} = $kind;
wenzelm@27386
    27
    }
wenzelm@27386
    28
  } else {
wenzelm@27386
    29
    $keywords{$name} = $kind;
wenzelm@24875
    30
  }
wenzelm@24875
    31
}
wenzelm@24875
    32
wenzelm@24875
    33
sub collect_keywords {
wenzelm@24875
    34
  while(<STDIN>) {
wenzelm@24875
    35
    if (m/^Outer syntax keyword:\s*"(.*)"/) {
wenzelm@24875
    36
      my $name = $1;
wenzelm@24875
    37
      &set_keyword($name, "minor");
wenzelm@24875
    38
    }
wenzelm@24875
    39
    elsif (m/^Outer syntax command:\s*"(.*)"\s*\((.*)\)/) {
wenzelm@24875
    40
      my $name = $1;
wenzelm@24875
    41
      my $kind = $2;
wenzelm@36316
    42
      if ($kind eq "theory-schematic-goal") { $kind = "theory-goal"; }
wenzelm@24875
    43
      &set_keyword($name, $kind);
wenzelm@24875
    44
    }
wenzelm@24875
    45
  }
wenzelm@24875
    46
}
wenzelm@24875
    47
wenzelm@24875
    48
wenzelm@24875
    49
## Emacs output
wenzelm@24875
    50
wenzelm@24875
    51
sub emacs_output {
wenzelm@24886
    52
  my @kinds = (
wenzelm@24886
    53
    "major",
wenzelm@24886
    54
    "minor",
wenzelm@24886
    55
    "control",
wenzelm@24886
    56
    "diag",
wenzelm@24886
    57
    "theory-begin",
wenzelm@24886
    58
    "theory-switch",
wenzelm@24886
    59
    "theory-end",
wenzelm@24886
    60
    "theory-heading",
wenzelm@24886
    61
    "theory-decl",
wenzelm@24886
    62
    "theory-script",
wenzelm@24886
    63
    "theory-goal",
wenzelm@24886
    64
    "qed",
wenzelm@24886
    65
    "qed-block",
wenzelm@24886
    66
    "qed-global",
wenzelm@24886
    67
    "proof-heading",
wenzelm@24886
    68
    "proof-goal",
wenzelm@24886
    69
    "proof-block",
wenzelm@24886
    70
    "proof-open",
wenzelm@24886
    71
    "proof-close",
wenzelm@24886
    72
    "proof-chain",
wenzelm@24886
    73
    "proof-decl",
wenzelm@24886
    74
    "proof-asm",
wenzelm@24886
    75
    "proof-asm-goal",
wenzelm@24886
    76
    "proof-script"
wenzelm@24886
    77
  );
wenzelm@24875
    78
  my $file = $keywords_name eq "" ? "isar-keywords.el" : "isar-keywords-${keywords_name}.el";
wenzelm@24875
    79
  open (OUTPUT, "> ${file}") || die "$!";
wenzelm@24875
    80
  select OUTPUT;
wenzelm@24875
    81
wenzelm@24875
    82
  print ";;\n";
wenzelm@24875
    83
  print ";; Keyword classification tables for Isabelle/Isar.\n";
wenzelm@24912
    84
  print ";; Generated from ${sessions}.\n";
wenzelm@24905
    85
  print ";; *** DO NOT EDIT *** DO NOT EDIT *** DO NOT EDIT ***\n";
wenzelm@24875
    86
  print ";;\n";
wenzelm@24875
    87
wenzelm@24875
    88
  for my $kind (@kinds) {
wenzelm@24875
    89
    my @names;
wenzelm@24875
    90
    for my $name (keys(%keywords)) {
wenzelm@24875
    91
      if ($kind eq "major" ? $keywords{$name} ne "minor" : $keywords{$name} eq $kind) {
wenzelm@24875
    92
        if ($kind ne "minor" or $name =~ m/^[A-Za-z0-9_]+$/) {
wenzelm@24875
    93
          push @names, $name;
wenzelm@24875
    94
        }
wenzelm@24875
    95
      }
wenzelm@24875
    96
    }
wenzelm@24875
    97
    @names = sort(@names);
wenzelm@24875
    98
wenzelm@24875
    99
    print "\n(defconst isar-keywords-${kind}";
wenzelm@24875
   100
    print "\n  '(";
wenzelm@24875
   101
    my $first = 1;
wenzelm@24875
   102
    for my $name (@names) {
wenzelm@24875
   103
      $name =~ s/([\.\*\+\?\[\]\^\$])/\\\\$1/g;
wenzelm@24875
   104
      if ($first) {
wenzelm@24875
   105
        print "\"${name}\"";
wenzelm@24875
   106
        $first = 0;
wenzelm@24875
   107
      }
wenzelm@24875
   108
      else {
wenzelm@24875
   109
        print "\n    \"${name}\"";
wenzelm@24875
   110
      }
wenzelm@24875
   111
    }
wenzelm@24875
   112
    print "))\n";
wenzelm@24875
   113
  }
wenzelm@24875
   114
  print "\n(provide 'isar-keywords)\n";
wenzelm@24875
   115
wenzelm@24875
   116
  close OUTPUT;
wenzelm@24875
   117
  select;
wenzelm@33684
   118
  print STDERR "${file}\n";
wenzelm@24875
   119
}
wenzelm@24875
   120
wenzelm@24875
   121
wenzelm@24875
   122
## main
wenzelm@24875
   123
wenzelm@24875
   124
&collect_keywords();
wenzelm@33684
   125
&emacs_output();