# HG changeset patch
# User wenzelm
# Date 1372109594 -7200
# Node ID 4cf3f6153eb8cee65aabc0fa0b6d18ddc717af84
# Parent  7b5a5116f3af77be44521229f025bff970339fa1
improved "isabelle keywords" and "isabelle update_keywords" based on Isabelle/Scala, without requiring to build sessions first;
tuned signature;

diff -r 7b5a5116f3af -r 4cf3f6153eb8 Admin/Release/CHECKLIST
--- a/Admin/Release/CHECKLIST	Mon Jun 24 17:17:17 2013 +0200
+++ b/Admin/Release/CHECKLIST	Mon Jun 24 23:33:14 2013 +0200
@@ -17,8 +17,6 @@
 
 - check file positions within logic images (hyperlinks etc.);
 
-- isabelle update_keywords;
-
 - check ANNOUNCE, README, NEWS, COPYRIGHT, CONTRIBUTORS;
 
 - check funny base directory, e.g. "Test 中国";
diff -r 7b5a5116f3af -r 4cf3f6153eb8 Admin/lib/Tools/update_keywords
--- a/Admin/lib/Tools/update_keywords	Mon Jun 24 17:17:17 2013 +0200
+++ b/Admin/lib/Tools/update_keywords	Mon Jun 24 23:33:14 2013 +0200
@@ -4,13 +4,11 @@
 #
 # DESCRIPTION: update standard keyword files for Emacs Proof General
 
-LOG="$ISABELLE_OUTPUT/log"
+[ -e "$ISABELLE_HOME/Admin/build" ] && { "$ISABELLE_HOME/Admin/build" jars || exit $?; }
+
+declare -a JAVA_ARGS; eval "JAVA_ARGS=($ISABELLE_BUILD_JAVA_OPTIONS)"
 
 cd "$ISABELLE_HOME/etc"
 
-"$ISABELLE_TOOL" keywords \
-  "$LOG/HOLCF.gz" "$LOG/HOL-BNF.gz" "$LOG/HOL-Boogie.gz" "$LOG/HOL-Library.gz" "$LOG/HOL-Nominal.gz" \
-  "$LOG/HOL-Statespace.gz" "$LOG/HOL-SPARK.gz" "$LOG/HOL-TPTP.gz" "$LOG/HOL-Import.gz"
+"$ISABELLE_TOOL" java "${JAVA_ARGS[@]}" isabelle.Keywords update_keywords
 
-"$ISABELLE_TOOL" keywords -k ZF "$LOG/ZF.gz"
-
diff -r 7b5a5116f3af -r 4cf3f6153eb8 NEWS
--- a/NEWS	Mon Jun 24 17:17:17 2013 +0200
+++ b/NEWS	Mon Jun 24 23:33:14 2013 +0200
@@ -297,6 +297,10 @@
 * Toplevel executable $ISABELLE_HOME/bin/isabelle_scala_script allows
 to run Isabelle/Scala source files as standalone programs.
 
+* Improved "isabelle keywords" tool (for old-style ProofGeneral
+keyword tables): use Isabelle/Scala operations, which inspect outer
+syntax without requiring to build sessions first.
+
 
 
 New in Isabelle2013 (February 2013)
diff -r 7b5a5116f3af -r 4cf3f6153eb8 etc/isar-keywords-ZF.el
--- a/etc/isar-keywords-ZF.el	Mon Jun 24 17:17:17 2013 +0200
+++ b/etc/isar-keywords-ZF.el	Mon Jun 24 23:33:14 2013 +0200
@@ -1,6 +1,5 @@
 ;;
-;; Keyword classification tables for Isabelle/Isar.
-;; Generated from ZF.
+;; Generated keyword classification tables for Isabelle/Isar.
 ;; *** DO NOT EDIT *** DO NOT EDIT *** DO NOT EDIT ***
 ;;
 
diff -r 7b5a5116f3af -r 4cf3f6153eb8 etc/isar-keywords.el
--- a/etc/isar-keywords.el	Mon Jun 24 17:17:17 2013 +0200
+++ b/etc/isar-keywords.el	Mon Jun 24 23:33:14 2013 +0200
@@ -1,6 +1,5 @@
 ;;
-;; Keyword classification tables for Isabelle/Isar.
-;; Generated from HOLCF + HOL-BNF + HOL-Boogie + HOL-Library + HOL-Nominal + HOL-Statespace + HOL-SPARK + HOL-TPTP + HOL-Import.
+;; Generated keyword classification tables for Isabelle/Isar.
 ;; *** DO NOT EDIT *** DO NOT EDIT *** DO NOT EDIT ***
 ;;
 
diff -r 7b5a5116f3af -r 4cf3f6153eb8 lib/Tools/keywords
--- a/lib/Tools/keywords	Mon Jun 24 17:17:17 2013 +0200
+++ b/lib/Tools/keywords	Mon Jun 24 23:33:14 2013 +0200
@@ -2,7 +2,7 @@
 #
 # Author: Makarius
 #
-# DESCRIPTION: generate outer syntax keyword files from session logs
+# DESCRIPTION: generate keyword files for Emacs Proof General
 
 
 ## diagnostics
@@ -12,13 +12,13 @@
 function usage()
 {
   echo
-  echo "Usage: isabelle $PRG [OPTIONS] [LOGS ...]"
+  echo "Usage: isabelle $PRG [OPTIONS] [SESSIONS ...]"
   echo
   echo "  Options are:"
+  echo "    -d DIR       include session directory"
   echo "    -k NAME      specific name of keywords collection (default: empty)"
   echo
-  echo "  Generate outer syntax keyword files from (compressed) session LOGS."
-  echo "  Targets Emacs Proof General."
+  echo "  Generate keyword files for Emacs Proof General from Isabelle sessions."
   echo
   exit 1
 }
@@ -28,11 +28,15 @@
 
 # options
 
+declare -a DIRS=()
 KEYWORDS_NAME=""
 
-while getopts "k:" OPT
+while getopts "d:k:" OPT
 do
   case "$OPT" in
+    d)
+      DIRS["${#DIRS[@]}"]="$OPTARG"
+      ;;
     k)
       KEYWORDS_NAME="$OPTARG"
       ;;
@@ -47,23 +51,10 @@
 
 ## main
 
-SESSIONS=""
-for LOG in "$@"
-do
-  NAME="$(basename "$LOG" .gz)"
-  if [ -z "$SESSIONS" ]; then
-    SESSIONS="$NAME"
-  else
-    SESSIONS="$SESSIONS + $NAME"
-  fi
-done
+[ -e "$ISABELLE_HOME/Admin/build" ] && { "$ISABELLE_HOME/Admin/build" jars || exit $?; }
+
+declare -a JAVA_ARGS; eval "JAVA_ARGS=($ISABELLE_BUILD_JAVA_OPTIONS)"
 
-for LOG in "$@"
-do
-  if [ "${LOG%.gz}" = "$LOG" ]; then
-    cat "$LOG"
-  else
-    gzip -dc "$LOG"
-  fi
-  echo
-done | "$ISABELLE_HOME/lib/scripts/keywords" "$KEYWORDS_NAME" "$SESSIONS"
+"$ISABELLE_TOOL" java "${JAVA_ARGS[@]}" isabelle.Keywords keywords \
+  "$KEYWORDS_NAME" "${DIRS[@]}" $'\n' "$@"
+
diff -r 7b5a5116f3af -r 4cf3f6153eb8 lib/scripts/keywords
--- a/lib/scripts/keywords	Mon Jun 24 17:17:17 2013 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,153 +0,0 @@
-#!/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_heading1" => "theory-heading",
-  "thy_heading2" => "theory-heading",
-  "thy_heading3" => "theory-heading",
-  "thy_heading4" => "theory-heading",
-  "thy_load" => "theory-decl",
-  "thy_decl" => "theory-decl",
-  "thy_script" => "theory-script",
-  "thy_goal" => "theory-goal",
-  "qed_block" => "qed-block",
-  "qed_global" => "qed-global",
-  "prf_heading2" => "proof-heading",
-  "prf_heading3" => "proof-heading",
-  "prf_heading4" => "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/^\fOuter syntax keyword "([^"]*)" :: (\S*)/) {
-      my $name = $1;
-      my $kind = $2;
-      if (defined $convert_kinds{$kind}) { $kind = $convert_kinds{$kind} }
-      &set_keyword($name, $kind);
-    }
-    elsif (m/^\fOuter 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();
diff -r 7b5a5116f3af -r 4cf3f6153eb8 src/Pure/Isar/outer_syntax.scala
--- a/src/Pure/Isar/outer_syntax.scala	Mon Jun 24 17:17:17 2013 +0200
+++ b/src/Pure/Isar/outer_syntax.scala	Mon Jun 24 23:33:14 2013 +0200
@@ -37,9 +37,6 @@
   val empty: Outer_Syntax = new Outer_Syntax()
 
   def init(): Outer_Syntax = new Outer_Syntax(completion = Completion.init())
-
-  def init_pure(): Outer_Syntax =
-    init() + ("theory", Keyword.THY_BEGIN) + ("ML_file", Keyword.THY_LOAD)
 }
 
 final class Outer_Syntax private(
@@ -76,11 +73,11 @@
 
   def add_keywords(keywords: Thy_Header.Keywords): Outer_Syntax =
     (this /: keywords) {
-      case (syntax, ((name, Some((kind, _)), replace))) =>
+      case (syntax, (name, Some((kind, _)), replace)) =>
         syntax +
           (Symbol.decode(name), kind, replace) +
           (Symbol.encode(name), kind, replace)
-      case (syntax, ((name, None, replace))) =>
+      case (syntax, (name, None, replace)) =>
         syntax +
           (Symbol.decode(name), replace) +
           (Symbol.encode(name), replace)
diff -r 7b5a5116f3af -r 4cf3f6153eb8 src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Mon Jun 24 17:17:17 2013 +0200
+++ b/src/Pure/Pure.thy	Mon Jun 24 23:33:14 2013 +0200
@@ -13,6 +13,8 @@
     "identifier" "if" "imports" "in" "includes" "infix" "infixl"
     "infixr" "is" "keywords" "notes" "obtains" "open" "output"
     "overloaded" "pervasive" "shows" "structure" "unchecked" "where" "|"
+  and "theory" :: thy_begin
+  and "ML_file" :: thy_load
   and "header" :: diag
   and "chapter" :: thy_heading1
   and "section" :: thy_heading2
diff -r 7b5a5116f3af -r 4cf3f6153eb8 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Mon Jun 24 17:17:17 2013 +0200
+++ b/src/Pure/Tools/build.scala	Mon Jun 24 23:33:14 2013 +0200
@@ -394,6 +394,7 @@
 
   sealed case class Session_Content(
     loaded_theories: Set[String],
+    keywords: Thy_Header.Keywords,
     syntax: Outer_Syntax,
     sources: List[(Path, SHA1.Digest)])
 
@@ -411,7 +412,7 @@
           val (preloaded, parent_syntax) =
             info.parent match {
               case None =>
-                (Set.empty[String], Outer_Syntax.init_pure())
+                (Set.empty[String], Outer_Syntax.init())
               case Some(parent_name) =>
                 val parent = deps(parent_name)
                 (parent.loaded_theories, parent.syntax)
@@ -431,6 +432,7 @@
                 map(thy => Thy_Load.path_node_name(info.dir + Thy_Load.thy_path(thy))))
 
           val loaded_theories = thy_deps.loaded_theories
+          val keywords = thy_deps.keywords
           val syntax = thy_deps.syntax
 
           val body_files = if (inlined_files) thy_deps.load_files else Nil
@@ -450,19 +452,31 @@
                   quote(name) + Position.here(info.pos))
             }
 
-          deps + (name -> Session_Content(loaded_theories, syntax, sources))
+          deps + (name -> Session_Content(loaded_theories, keywords, syntax, sources))
       }))
 
-  def session_content(inlined_files: Boolean, dirs: List[Path], session: String): Session_Content =
+  def session_dependencies(
+    options: Options,
+    inlined_files: Boolean,
+    dirs: List[Path],
+    sessions: List[String]): Deps =
   {
-    val options = Options.init()
     val (_, tree) =
-      find_sessions(options, dirs.map((false, _))).selection(false, false, Nil, List(session))
-    dependencies(Ignore_Progress, inlined_files, false, false, tree)(session)
+      find_sessions(options, dirs.map((false, _))).selection(false, false, Nil, sessions)
+    dependencies(Ignore_Progress, inlined_files, false, false, tree)
   }
 
-  def outer_syntax(session: String): Outer_Syntax =
-    session_content(false, Nil, session).syntax
+  def session_content(
+    options: Options,
+    inlined_files: Boolean,
+    dirs: List[Path],
+    session: String): Session_Content =
+  {
+    session_dependencies(options, inlined_files, dirs, List(session))(session)
+  }
+
+  def outer_syntax(options: Options, session: String): Outer_Syntax =
+    session_content(options, false, Nil, session).syntax
 
 
   /* jobs */
diff -r 7b5a5116f3af -r 4cf3f6153eb8 src/Pure/Tools/keywords.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Tools/keywords.scala	Mon Jun 24 23:33:14 2013 +0200
@@ -0,0 +1,163 @@
+/*  Title:      Pure/Tools/keywords.scala
+    Author:     Makarius
+
+Generate keyword files for Emacs Proof General.
+*/
+
+package isabelle
+
+
+import scala.collection.mutable
+
+
+object Keywords
+{
+  /* keywords */
+
+  private val convert_kinds = Map(
+    "thy_begin" -> "theory-begin",
+    "thy_end" -> "theory-end",
+    "thy_heading1" -> "theory-heading",
+    "thy_heading2" -> "theory-heading",
+    "thy_heading3" -> "theory-heading",
+    "thy_heading4" -> "theory-heading",
+    "thy_load" -> "theory-decl",
+    "thy_decl" -> "theory-decl",
+    "thy_script" -> "theory-script",
+    "thy_goal" -> "theory-goal",
+    "qed_block" -> "qed-block",
+    "qed_global" -> "qed-global",
+    "prf_heading2" -> "proof-heading",
+    "prf_heading3" -> "proof-heading",
+    "prf_heading4" -> "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"
+  ).withDefault((s: String) => s)
+
+  private val emacs_kinds = List(
+    "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")
+
+  def keywords(
+    options: Options,
+    name: String = "",
+    dirs: List[Path] = Nil,
+    sessions: List[String] = Nil)
+  {
+    val deps = Build.session_dependencies(options, false, dirs, sessions).deps
+    val keywords =
+    {
+      var keywords = Map.empty[String, String]
+      for {
+        (_, dep) <- deps
+        (name, kind_spec, _) <- dep.keywords
+        kind = kind_spec match { case Some(((kind, _), _)) => kind case None => "minor" }
+        k = convert_kinds(kind)
+      } {
+        keywords.get(name) match {
+          case Some(k1) if k1 != k && k1 != "minor" && k != "minor" =>
+            error("Inconsistent declaration of keyword " + quote(name) + ": " + k1 + " vs " + k)
+          case _ =>
+        }
+        keywords += (name -> k)
+      }
+      keywords
+    }
+
+    val output =
+    {
+      val out = new mutable.StringBuilder
+
+      out ++= ";;\n"
+      out ++= ";; Generated keyword classification tables for Isabelle/Isar.\n"
+      out ++= ";; *** DO NOT EDIT *** DO NOT EDIT *** DO NOT EDIT ***\n"
+      out ++= ";;\n"
+
+      for (kind <- emacs_kinds) {
+        val names =
+          (for {
+            (name, k) <- keywords.iterator
+            if (if (kind == "major") k != "minor" else k == kind)
+            if kind != "minor" || Symbol.is_ascii_identifier(name)
+          } yield name).toList.sorted
+
+        out ++= "\n(defconst isar-keywords-" + kind
+        out ++= "\n  '("
+        out ++=
+          names.map(name => quote("""[\.\*\+\?\[\]\^\$]""".r replaceAllIn (name, """\\\\$0""")))
+            .mkString("\n    ")
+        out ++= "))\n"
+      }
+
+      out ++= "\n(provide 'isar-keywords)\n"
+
+      out.toString
+    }
+
+    val file = if (name == "") "isar-keywords.el" else "isar-keywords-" + name + ".el"
+    java.lang.System.err.println(file)
+    File.write(Path.explode(file), output)
+  }
+
+
+  /* administrative update_keywords */
+
+  def update_keywords(options: Options)
+  {
+    val tree = Build.find_sessions(options, Nil)
+
+    def chapter(ch: String): List[String] =
+      for ((name, info) <- tree.topological_order if info.chapter == ch) yield name
+
+    keywords(options, sessions = chapter("HOL"))
+    keywords(options, name = "ZF", sessions = chapter("ZF"))
+  }
+
+
+  /* command line entry point */
+
+  def main(args: Array[String])
+  {
+    Command_Line.tool {
+      args.toList match {
+        case "keywords" :: name :: Command_Line.Chunks(dirs, sessions) =>
+          keywords(Options.init(), name, dirs.map(Path.explode), sessions)
+          0
+        case "update_keywords" :: Nil =>
+          update_keywords(Options.init())
+          0
+        case _ => error("Bad arguments:\n" + cat_lines(args))
+      }
+    }
+  }
+}
+
diff -r 7b5a5116f3af -r 4cf3f6153eb8 src/Pure/build-jars
--- a/src/Pure/build-jars	Mon Jun 24 17:17:17 2013 +0200
+++ b/src/Pure/build-jars	Mon Jun 24 23:33:14 2013 +0200
@@ -68,6 +68,7 @@
   Thy/thy_syntax.scala
   Tools/build.scala
   Tools/build_dialog.scala
+  Tools/keywords.scala
   Tools/main.scala
   Tools/ml_statistics.scala
   Tools/task_statistics.scala
diff -r 7b5a5116f3af -r 4cf3f6153eb8 src/Tools/jEdit/src/isabelle_logic.scala
--- a/src/Tools/jEdit/src/isabelle_logic.scala	Mon Jun 24 17:17:17 2013 +0200
+++ b/src/Tools/jEdit/src/isabelle_logic.scala	Mon Jun 24 23:33:14 2013 +0200
@@ -79,7 +79,7 @@
   {
     val dirs = session_dirs()
     val name = session_args().last
-    Build.session_content(inlined_files, dirs, name)
+    Build.session_content(PIDE.options.value, inlined_files, dirs, name)
   }
 }