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