generate keywords for Emacs Proof General only;
tuned;

--- a/Admin/update-keywords	Sat Nov 14 18:14:00 2009 +0100
+++ b/Admin/update-keywords	Sat Nov 14 18:15:21 2009 +0100
@@ -1,30 +1,19 @@
 #!/usr/bin/env bash
 #
-# $Id$
 # Author: Makarius
 #
-# DESCRIPTION: Update standard keyword files.
+# DESCRIPTION: Update standard keyword files for Emacs Proof General
 
 ISABELLE_HOME="$(isabelle getenv -b ISABELLE_HOME)"
 LOG="$(isabelle getenv -b ISABELLE_OUTPUT)"/log
 
 
-## Emacs ProofGeneral
-
 cd "$ISABELLE_HOME/etc"
 
-isabelle keywords -t emacs \
+isabelle keywords \
   "$LOG/Pure.gz" "$LOG/Pure-ProofGeneral.gz" "$LOG/HOL.gz" "$LOG/HOLCF.gz" \
   "$LOG/IOA.gz" "$LOG/HOL-Nominal.gz" "$LOG/HOL-Statespace.gz"
 
-isabelle keywords -t emacs -k ZF \
+isabelle keywords -k ZF \
   "$LOG/Pure.gz" "$LOG/Pure-ProofGeneral.gz" "$LOG/FOL.gz" "$LOG/ZF.gz"
 
-
-## jEdit
-
-cd "$ISABELLE_HOME/lib/jedit"
-
-isabelle keywords -t jedit \
-  "$LOG/Pure.gz" "$LOG/HOL.gz" "$LOG/HOLCF.gz" "$LOG/IOA.gz" "$LOG/HOL-Nominal.gz" \
-  "$LOG/HOL-Statespace.gz" "$LOG/FOL.gz" "$LOG/ZF.gz"

--- a/lib/Tools/keywords	Sat Nov 14 18:14:00 2009 +0100
+++ b/lib/Tools/keywords	Sat Nov 14 18:15:21 2009 +0100
@@ -16,9 +16,9 @@
   echo
   echo "  Options are:"
   echo "    -k NAME      specific name of keywords collection (default: empty)"
-  echo "    -t TARGET    target tool (default: emacs)"
   echo
   echo "  Generate outer syntax keyword files from (compressed) session LOGS."
+  echo "  Targets Emacs Proof General."
   echo
   exit 1
 }
@@ -29,17 +29,13 @@
 # options
 
 KEYWORDS_NAME=""
-TARGET_TOOL="emacs"
 
-while getopts "k:t:" OPT
+while getopts "k:" OPT
 do
   case "$OPT" in
     k)
       KEYWORDS_NAME="$OPTARG"
       ;;
-    t)
-      TARGET_TOOL="$OPTARG"
-      ;;
     \?)
       usage
       ;;
@@ -49,15 +45,10 @@
 shift $(($OPTIND - 1))
 
 
-# args
-
-LOGS="$@"; shift "$#"
-
-
 ## main
 
 SESSIONS=""
-for LOG in $LOGS
+for LOG in "$@"
 do
   NAME="$(basename "$LOG" .gz)"
   if [ -z "$SESSIONS" ]; then
@@ -67,7 +58,7 @@
   fi
 done
 
-for LOG in $LOGS
+for LOG in "$@"
 do
   if [ "${LOG%.gz}" = "$LOG" ]; then
     cat "$LOG"
@@ -76,4 +67,4 @@
   fi
   echo
 done | \
-perl -w "$ISABELLE_HOME/lib/scripts/keywords.pl" "$KEYWORDS_NAME" "$TARGET_TOOL" "$SESSIONS"
+perl -w "$ISABELLE_HOME/lib/scripts/keywords.pl" "$KEYWORDS_NAME" "$SESSIONS"

--- a/lib/scripts/keywords.pl	Sat Nov 14 18:14:00 2009 +0100
+++ b/lib/scripts/keywords.pl	Sat Nov 14 18:15:21 2009 +0100
@@ -6,7 +6,7 @@
 
 ## arguments
 
-my ($keywords_name, $target_tool, $sessions) = @ARGV;
+my ($keywords_name, $sessions) = @ARGV;
 
 
 ## keywords
@@ -109,106 +109,12 @@
 
   close OUTPUT;
   select;
-  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">
-EOF
-  print "<!-- Generated from ${sessions}. -->\n";
-  print "<!-- *** DO NOT EDIT *** DO NOT EDIT *** DO NOT EDIT *** -->\n";
-  print <<'EOF';
-<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";
+  print STDERR "${file}\n";
 }
 
 
 ## main
 
 &collect_keywords();
-eval "${target_tool}_output()";
+&emacs_output();