lib/scripts/keywords

uniform keyword names within ML/Scala -- produce elisp names via external conversion;
discontinued obsolete Keyword.thy_switch;

#!/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_heading" => "theory-heading",
  "thy_decl" => "theory-decl",
  "thy_script" => "theory-script",
  "thy_goal" => "theory-goal",
  "thy_schematic_goal" => "theory-goal",
  "qed_block" => "qed-block",
  "qed_global" => "qed-global",
  "prf_heading" => "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/^Outer syntax keyword "([^"]*)" :: (\S*)/) {
      my $name = $1;
      my $kind = $2;
      if (defined $convert_kinds{$kind}) { $kind = $convert_kinds{$kind} }
      &set_keyword($name, $kind);
    }
    elsif (m/^Outer 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();