lib/scripts/keywords
author wenzelm
Mon, 20 Aug 2012 14:09:09 +0200
changeset 48864 3ee314ae1e0a
parent 46969 481b7d9ad6fe
child 50714 2af9e4614ba4
permissions -rwxr-xr-x
added keyword kind "thy_load" (with optional list of file extensions);
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
46967
499d9bbd8de9 uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents: 36316
diff changeset
    33
my %convert_kinds = (
499d9bbd8de9 uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents: 36316
diff changeset
    34
  "thy_begin" => "theory-begin",
499d9bbd8de9 uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents: 36316
diff changeset
    35
  "thy_end" => "theory-end",
46969
481b7d9ad6fe more abstract heading level;
wenzelm
parents: 46967
diff changeset
    36
  "thy_heading1" => "theory-heading",
481b7d9ad6fe more abstract heading level;
wenzelm
parents: 46967
diff changeset
    37
  "thy_heading2" => "theory-heading",
481b7d9ad6fe more abstract heading level;
wenzelm
parents: 46967
diff changeset
    38
  "thy_heading3" => "theory-heading",
481b7d9ad6fe more abstract heading level;
wenzelm
parents: 46967
diff changeset
    39
  "thy_heading4" => "theory-heading",
48864
3ee314ae1e0a added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents: 46969
diff changeset
    40
  "thy_load" => "theory-decl",
46967
499d9bbd8de9 uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents: 36316
diff changeset
    41
  "thy_decl" => "theory-decl",
499d9bbd8de9 uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents: 36316
diff changeset
    42
  "thy_script" => "theory-script",
499d9bbd8de9 uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents: 36316
diff changeset
    43
  "thy_goal" => "theory-goal",
499d9bbd8de9 uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents: 36316
diff changeset
    44
  "thy_schematic_goal" => "theory-goal",
499d9bbd8de9 uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents: 36316
diff changeset
    45
  "qed_block" => "qed-block",
499d9bbd8de9 uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents: 36316
diff changeset
    46
  "qed_global" => "qed-global",
46969
481b7d9ad6fe more abstract heading level;
wenzelm
parents: 46967
diff changeset
    47
  "prf_heading2" => "proof-heading",
481b7d9ad6fe more abstract heading level;
wenzelm
parents: 46967
diff changeset
    48
  "prf_heading3" => "proof-heading",
481b7d9ad6fe more abstract heading level;
wenzelm
parents: 46967
diff changeset
    49
  "prf_heading4" => "proof-heading",
46967
499d9bbd8de9 uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents: 36316
diff changeset
    50
  "prf_goal" => "proof-goal",
499d9bbd8de9 uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents: 36316
diff changeset
    51
  "prf_block" => "proof-block",
499d9bbd8de9 uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents: 36316
diff changeset
    52
  "prf_open" => "proof-open",
499d9bbd8de9 uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents: 36316
diff changeset
    53
  "prf_close" => "proof-close",
499d9bbd8de9 uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents: 36316
diff changeset
    54
  "prf_chain" => "proof-chain",
499d9bbd8de9 uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents: 36316
diff changeset
    55
  "prf_decl" => "proof-decl",
499d9bbd8de9 uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents: 36316
diff changeset
    56
  "prf_asm" => "proof-asm",
499d9bbd8de9 uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents: 36316
diff changeset
    57
  "prf_asm_goal" => "proof-asm-goal",
499d9bbd8de9 uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents: 36316
diff changeset
    58
  "prf_script" => "proof-script"
499d9bbd8de9 uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents: 36316
diff changeset
    59
);
499d9bbd8de9 uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents: 36316
diff changeset
    60
499d9bbd8de9 uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents: 36316
diff changeset
    61
my @emacs_kinds = (
499d9bbd8de9 uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents: 36316
diff changeset
    62
  "major",
499d9bbd8de9 uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents: 36316
diff changeset
    63
  "minor",
499d9bbd8de9 uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents: 36316
diff changeset
    64
  "control",
499d9bbd8de9 uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents: 36316
diff changeset
    65
  "diag",
499d9bbd8de9 uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents: 36316
diff changeset
    66
  "theory-begin",
499d9bbd8de9 uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents: 36316
diff changeset
    67
  "theory-switch",
499d9bbd8de9 uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents: 36316
diff changeset
    68
  "theory-end",
499d9bbd8de9 uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents: 36316
diff changeset
    69
  "theory-heading",
499d9bbd8de9 uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents: 36316
diff changeset
    70
  "theory-decl",
499d9bbd8de9 uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents: 36316
diff changeset
    71
  "theory-script",
499d9bbd8de9 uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents: 36316
diff changeset
    72
  "theory-goal",
499d9bbd8de9 uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents: 36316
diff changeset
    73
  "qed",
499d9bbd8de9 uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents: 36316
diff changeset
    74
  "qed-block",
499d9bbd8de9 uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents: 36316
diff changeset
    75
  "qed-global",
499d9bbd8de9 uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents: 36316
diff changeset
    76
  "proof-heading",
499d9bbd8de9 uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents: 36316
diff changeset
    77
  "proof-goal",
499d9bbd8de9 uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents: 36316
diff changeset
    78
  "proof-block",
499d9bbd8de9 uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents: 36316
diff changeset
    79
  "proof-open",
499d9bbd8de9 uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents: 36316
diff changeset
    80
  "proof-close",
499d9bbd8de9 uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents: 36316
diff changeset
    81
  "proof-chain",
499d9bbd8de9 uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents: 36316
diff changeset
    82
  "proof-decl",
499d9bbd8de9 uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents: 36316
diff changeset
    83
  "proof-asm",
499d9bbd8de9 uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents: 36316
diff changeset
    84
  "proof-asm-goal",
499d9bbd8de9 uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents: 36316
diff changeset
    85
  "proof-script"
499d9bbd8de9 uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents: 36316
diff changeset
    86
);
499d9bbd8de9 uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents: 36316
diff changeset
    87
24875
8e6ca75bf5aa generate outer syntax keyword files from session logs;
wenzelm
parents:
diff changeset
    88
sub collect_keywords {
8e6ca75bf5aa generate outer syntax keyword files from session logs;
wenzelm
parents:
diff changeset
    89
  while(<STDIN>) {
46967
499d9bbd8de9 uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents: 36316
diff changeset
    90
    if (m/^Outer syntax keyword "([^"]*)" :: (\S*)/) {
499d9bbd8de9 uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents: 36316
diff changeset
    91
      my $name = $1;
499d9bbd8de9 uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents: 36316
diff changeset
    92
      my $kind = $2;
499d9bbd8de9 uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents: 36316
diff changeset
    93
      if (defined $convert_kinds{$kind}) { $kind = $convert_kinds{$kind} }
499d9bbd8de9 uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents: 36316
diff changeset
    94
      &set_keyword($name, $kind);
499d9bbd8de9 uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents: 36316
diff changeset
    95
    }
499d9bbd8de9 uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents: 36316
diff changeset
    96
    elsif (m/^Outer syntax keyword "([^"]*)"/) {
24875
8e6ca75bf5aa generate outer syntax keyword files from session logs;
wenzelm
parents:
diff changeset
    97
      my $name = $1;
8e6ca75bf5aa generate outer syntax keyword files from session logs;
wenzelm
parents:
diff changeset
    98
      &set_keyword($name, "minor");
8e6ca75bf5aa generate outer syntax keyword files from session logs;
wenzelm
parents:
diff changeset
    99
    }
8e6ca75bf5aa generate outer syntax keyword files from session logs;
wenzelm
parents:
diff changeset
   100
  }
8e6ca75bf5aa generate outer syntax keyword files from session logs;
wenzelm
parents:
diff changeset
   101
}
8e6ca75bf5aa generate outer syntax keyword files from session logs;
wenzelm
parents:
diff changeset
   102
8e6ca75bf5aa generate outer syntax keyword files from session logs;
wenzelm
parents:
diff changeset
   103
8e6ca75bf5aa generate outer syntax keyword files from session logs;
wenzelm
parents:
diff changeset
   104
## Emacs output
8e6ca75bf5aa generate outer syntax keyword files from session logs;
wenzelm
parents:
diff changeset
   105
8e6ca75bf5aa generate outer syntax keyword files from session logs;
wenzelm
parents:
diff changeset
   106
sub emacs_output {
8e6ca75bf5aa generate outer syntax keyword files from session logs;
wenzelm
parents:
diff changeset
   107
  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
   108
  open (OUTPUT, "> ${file}") || die "$!";
8e6ca75bf5aa generate outer syntax keyword files from session logs;
wenzelm
parents:
diff changeset
   109
  select OUTPUT;
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
  print ";;\n";
8e6ca75bf5aa generate outer syntax keyword files from session logs;
wenzelm
parents:
diff changeset
   112
  print ";; Keyword classification tables for Isabelle/Isar.\n";
24912
52bc004950c4 tuned generated comment;
wenzelm
parents: 24905
diff changeset
   113
  print ";; Generated from ${sessions}.\n";
24905
65830ab42016 tuned generated comment;
wenzelm
parents: 24890
diff changeset
   114
  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
   115
  print ";;\n";
8e6ca75bf5aa generate outer syntax keyword files from session logs;
wenzelm
parents:
diff changeset
   116
46967
499d9bbd8de9 uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents: 36316
diff changeset
   117
  for my $kind (@emacs_kinds) {
24875
8e6ca75bf5aa generate outer syntax keyword files from session logs;
wenzelm
parents:
diff changeset
   118
    my @names;
8e6ca75bf5aa generate outer syntax keyword files from session logs;
wenzelm
parents:
diff changeset
   119
    for my $name (keys(%keywords)) {
8e6ca75bf5aa generate outer syntax keyword files from session logs;
wenzelm
parents:
diff changeset
   120
      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
   121
        if ($kind ne "minor" or $name =~ m/^[A-Za-z0-9_]+$/) {
8e6ca75bf5aa generate outer syntax keyword files from session logs;
wenzelm
parents:
diff changeset
   122
          push @names, $name;
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
      }
8e6ca75bf5aa generate outer syntax keyword files from session logs;
wenzelm
parents:
diff changeset
   125
    }
8e6ca75bf5aa generate outer syntax keyword files from session logs;
wenzelm
parents:
diff changeset
   126
    @names = sort(@names);
8e6ca75bf5aa generate outer syntax keyword files from session logs;
wenzelm
parents:
diff changeset
   127
8e6ca75bf5aa generate outer syntax keyword files from session logs;
wenzelm
parents:
diff changeset
   128
    print "\n(defconst isar-keywords-${kind}";
8e6ca75bf5aa generate outer syntax keyword files from session logs;
wenzelm
parents:
diff changeset
   129
    print "\n  '(";
8e6ca75bf5aa generate outer syntax keyword files from session logs;
wenzelm
parents:
diff changeset
   130
    my $first = 1;
8e6ca75bf5aa generate outer syntax keyword files from session logs;
wenzelm
parents:
diff changeset
   131
    for my $name (@names) {
8e6ca75bf5aa generate outer syntax keyword files from session logs;
wenzelm
parents:
diff changeset
   132
      $name =~ s/([\.\*\+\?\[\]\^\$])/\\\\$1/g;
8e6ca75bf5aa generate outer syntax keyword files from session logs;
wenzelm
parents:
diff changeset
   133
      if ($first) {
8e6ca75bf5aa generate outer syntax keyword files from session logs;
wenzelm
parents:
diff changeset
   134
        print "\"${name}\"";
8e6ca75bf5aa generate outer syntax keyword files from session logs;
wenzelm
parents:
diff changeset
   135
        $first = 0;
8e6ca75bf5aa generate outer syntax keyword files from session logs;
wenzelm
parents:
diff changeset
   136
      }
8e6ca75bf5aa generate outer syntax keyword files from session logs;
wenzelm
parents:
diff changeset
   137
      else {
8e6ca75bf5aa generate outer syntax keyword files from session logs;
wenzelm
parents:
diff changeset
   138
        print "\n    \"${name}\"";
8e6ca75bf5aa generate outer syntax keyword files from session logs;
wenzelm
parents:
diff changeset
   139
      }
8e6ca75bf5aa generate outer syntax keyword files from session logs;
wenzelm
parents:
diff changeset
   140
    }
8e6ca75bf5aa generate outer syntax keyword files from session logs;
wenzelm
parents:
diff changeset
   141
    print "))\n";
8e6ca75bf5aa generate outer syntax keyword files from session logs;
wenzelm
parents:
diff changeset
   142
  }
8e6ca75bf5aa generate outer syntax keyword files from session logs;
wenzelm
parents:
diff changeset
   143
  print "\n(provide 'isar-keywords)\n";
8e6ca75bf5aa generate outer syntax keyword files from session logs;
wenzelm
parents:
diff changeset
   144
8e6ca75bf5aa generate outer syntax keyword files from session logs;
wenzelm
parents:
diff changeset
   145
  close OUTPUT;
8e6ca75bf5aa generate outer syntax keyword files from session logs;
wenzelm
parents:
diff changeset
   146
  select;
33684
29d8aaeb56e5 generate keywords for Emacs Proof General only;
wenzelm
parents: 29145
diff changeset
   147
  print STDERR "${file}\n";
24875
8e6ca75bf5aa generate outer syntax keyword files from session logs;
wenzelm
parents:
diff changeset
   148
}
8e6ca75bf5aa generate outer syntax keyword files from session logs;
wenzelm
parents:
diff changeset
   149
8e6ca75bf5aa generate outer syntax keyword files from session logs;
wenzelm
parents:
diff changeset
   150
8e6ca75bf5aa generate outer syntax keyword files from session logs;
wenzelm
parents:
diff changeset
   151
## main
8e6ca75bf5aa generate outer syntax keyword files from session logs;
wenzelm
parents:
diff changeset
   152
8e6ca75bf5aa generate outer syntax keyword files from session logs;
wenzelm
parents:
diff changeset
   153
&collect_keywords();
33684
29d8aaeb56e5 generate keywords for Emacs Proof General only;
wenzelm
parents: 29145
diff changeset
   154
&emacs_output();