--- a/lib/scripts/keywords.pl Sun Oct 07 13:32:15 2007 +0200
+++ b/lib/scripts/keywords.pl Sun Oct 07 13:32:16 2007 +0200
@@ -5,36 +5,9 @@
# keywords.pl - generate outer syntax keyword files from session logs
#
-## global parameters
-
-my ($keywords_name, $sessions) = @ARGV;
+## arguments
-my @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"
-);
+my ($keywords_name, $target_tool, $sessions) = @ARGV;
## keywords
@@ -67,6 +40,32 @@
## Emacs output
sub emacs_output {
+ my @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"
+ );
my $file = $keywords_name eq "" ? "isar-keywords.el" : "isar-keywords-${keywords_name}.el";
open (OUTPUT, "> ${file}") || die "$!";
select OUTPUT;
@@ -108,12 +107,102 @@
close OUTPUT;
select;
- print STDERR "${file}\n";
+ print STDERR "${target_tool}: ${file}\n";
+}
+
+
+## jEdit output
+
+sub jedit_output {
+ my %keyword_types = (
+ "minor" => "KEYWORD4",
+ "control" => "INVALID",
+ "diag" => "LABEL",
+ "theory-begin" => "KEYWORD3",
+ "theory-switch" => "KEYWORD3",
+ "theory-end" => "KEYWORD3",
+ "theory-heading" => "OPERATOR",
+ "theory-decl" => "OPERATOR",
+ "theory-script" => "KEYWORD1",
+ "theory-goal" => "OPERATOR",
+ "qed" => "OPERATOR",
+ "qed-block" => "OPERATOR",
+ "qed-global" => "OPERATOR",
+ "proof-heading" => "OPERATOR",
+ "proof-goal" => "OPERATOR",
+ "proof-block" => "OPERATOR",
+ "proof-open" => "OPERATOR",
+ "proof-close" => "OPERATOR",
+ "proof-chain" => "OPERATOR",
+ "proof-decl" => "OPERATOR",
+ "proof-asm" => "KEYWORD2",
+ "proof-asm-goal" => "KEYWORD2",
+ "proof-script" => "KEYWORD1"
+ );
+ my $file = "isabelle.xml";
+ open (OUTPUT, "> ${file}") || die "$!";
+ select OUTPUT;
+
+ print <<'EOF';
+<?xml version="1.0"?>
+<!DOCTYPE MODE SYSTEM "xmode.dtd">
+<MODE>
+ <PROPS>
+ <PROPERTY NAME="commentStart" VALUE="(*"/>
+ <PROPERTY NAME="commentEnd" VALUE="*)"/>
+ <PROPERTY NAME="noWordSep" VALUE="_'.?"/>
+ <PROPERTY NAME="indentOpenBrackets" VALUE="{"/>
+ <PROPERTY NAME="indentCloseBrackets" VALUE="}"/>
+ <PROPERTY NAME="unalignedOpenBrackets" VALUE="(" />
+ <PROPERTY NAME="unalignedCloseBrackets" VALUE=")" />
+ <PROPERTY NAME="tabSize" VALUE="2" />
+ <PROPERTY NAME="indentSize" VALUE="2" />
+ </PROPS>
+ <RULES IGNORE_CASE="FALSE" HIGHLIGHT_DIGITS="FALSE" ESCAPE="\">
+ <SPAN TYPE="COMMENT1" NO_ESCAPE="TRUE">
+ <BEGIN>(*</BEGIN>
+ <END>*)</END>
+ </SPAN>
+ <SPAN TYPE="COMMENT3" NO_ESCAPE="TRUE">
+ <BEGIN>{*</BEGIN>
+ <END>*}</END>
+ </SPAN>
+ <SPAN TYPE="LITERAL1">
+ <BEGIN>`</BEGIN>
+ <END>`</END>
+ </SPAN>
+ <SPAN TYPE="LITERAL3">
+ <BEGIN>"</BEGIN>
+ <END>"</END>
+ </SPAN>
+ <KEYWORDS>
+EOF
+
+ for my $name (sort(keys(%keywords))) {
+ my $kind = $keywords{$name};
+ my $type = $keyword_types{$kind};
+ if ($kind ne "minor" or $name =~ m/^[A-Za-z0-9_]+$/) {
+ $name =~ s/&/&/g;
+ $name =~ s/</</g;
+ $name =~ s/>/</g;
+ print " <${type}>${name}</${type}>\n";
+ }
+ }
+
+ print <<'EOF';
+ </KEYWORDS>
+ </RULES>
+</MODE>
+EOF
+
+ close OUTPUT;
+ select;
+ print STDERR "${target_tool}: ${file}\n";
}
## main
&collect_keywords();
-&emacs_output();
+eval "${target_tool}_output()";