# HG changeset patch
# User wenzelm
# Date 1191756736 -7200
# Node ID ce449d6aef3fb95323f85485a730be18b0795626
# Parent  0fc7ba713a276c1e07f87bb3709ab36dc0d49c3d
added target tool specification;
added jEdit output;

diff -r 0fc7ba713a27 -r ce449d6aef3f lib/scripts/keywords.pl
--- 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/&/&amp;/g;
+      $name =~ s/</&lt;/g;
+      $name =~ s/>/&lt;/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()";