1.1 --- a/Admin/Release/CHECKLIST	Mon Jun 24 17:17:17 2013 +0200
     1.2 +++ b/Admin/Release/CHECKLIST	Mon Jun 24 23:33:14 2013 +0200
     1.3 @@ -17,8 +17,6 @@
     1.4  
     1.5  - check file positions within logic images (hyperlinks etc.);
     1.6  
     1.7 -- isabelle update_keywords;
     1.8 -
     1.9  - check ANNOUNCE, README, NEWS, COPYRIGHT, CONTRIBUTORS;
    1.10  
    1.11  - check funny base directory, e.g. "Test 中国";

     2.1 --- a/Admin/lib/Tools/update_keywords	Mon Jun 24 17:17:17 2013 +0200
     2.2 +++ b/Admin/lib/Tools/update_keywords	Mon Jun 24 23:33:14 2013 +0200
     2.3 @@ -4,13 +4,11 @@
     2.4  #
     2.5  # DESCRIPTION: update standard keyword files for Emacs Proof General
     2.6  
     2.7 -LOG="$ISABELLE_OUTPUT/log"
     2.8 +[ -e "$ISABELLE_HOME/Admin/build" ] && { "$ISABELLE_HOME/Admin/build" jars || exit $?; }
     2.9 +
    2.10 +declare -a JAVA_ARGS; eval "JAVA_ARGS=($ISABELLE_BUILD_JAVA_OPTIONS)"
    2.11  
    2.12  cd "$ISABELLE_HOME/etc"
    2.13  
    2.14 -"$ISABELLE_TOOL" keywords \
    2.15 -  "$LOG/HOLCF.gz" "$LOG/HOL-BNF.gz" "$LOG/HOL-Boogie.gz" "$LOG/HOL-Library.gz" "$LOG/HOL-Nominal.gz" \
    2.16 -  "$LOG/HOL-Statespace.gz" "$LOG/HOL-SPARK.gz" "$LOG/HOL-TPTP.gz" "$LOG/HOL-Import.gz"
    2.17 +"$ISABELLE_TOOL" java "${JAVA_ARGS[@]}" isabelle.Keywords update_keywords
    2.18  
    2.19 -"$ISABELLE_TOOL" keywords -k ZF "$LOG/ZF.gz"
    2.20 -

     3.1 --- a/NEWS	Mon Jun 24 17:17:17 2013 +0200
     3.2 +++ b/NEWS	Mon Jun 24 23:33:14 2013 +0200
     3.3 @@ -297,6 +297,10 @@
     3.4  * Toplevel executable $ISABELLE_HOME/bin/isabelle_scala_script allows
     3.5  to run Isabelle/Scala source files as standalone programs.
     3.6  
     3.7 +* Improved "isabelle keywords" tool (for old-style ProofGeneral
     3.8 +keyword tables): use Isabelle/Scala operations, which inspect outer
     3.9 +syntax without requiring to build sessions first.
    3.10 +
    3.11  
    3.12  
    3.13  New in Isabelle2013 (February 2013)

     4.1 --- a/etc/isar-keywords-ZF.el	Mon Jun 24 17:17:17 2013 +0200
     4.2 +++ b/etc/isar-keywords-ZF.el	Mon Jun 24 23:33:14 2013 +0200
     4.3 @@ -1,6 +1,5 @@
     4.4  ;;
     4.5 -;; Keyword classification tables for Isabelle/Isar.
     4.6 -;; Generated from ZF.
     4.7 +;; Generated keyword classification tables for Isabelle/Isar.
     4.8  ;; *** DO NOT EDIT *** DO NOT EDIT *** DO NOT EDIT ***
     4.9  ;;
    4.10  

     5.1 --- a/etc/isar-keywords.el	Mon Jun 24 17:17:17 2013 +0200
     5.2 +++ b/etc/isar-keywords.el	Mon Jun 24 23:33:14 2013 +0200
     5.3 @@ -1,6 +1,5 @@
     5.4  ;;
     5.5 -;; Keyword classification tables for Isabelle/Isar.
     5.6 -;; Generated from HOLCF + HOL-BNF + HOL-Boogie + HOL-Library + HOL-Nominal + HOL-Statespace + HOL-SPARK + HOL-TPTP + HOL-Import.
     5.7 +;; Generated keyword classification tables for Isabelle/Isar.
     5.8  ;; *** DO NOT EDIT *** DO NOT EDIT *** DO NOT EDIT ***
     5.9  ;;
    5.10  

     6.1 --- a/lib/Tools/keywords	Mon Jun 24 17:17:17 2013 +0200
     6.2 +++ b/lib/Tools/keywords	Mon Jun 24 23:33:14 2013 +0200
     6.3 @@ -2,7 +2,7 @@
     6.4  #
     6.5  # Author: Makarius
     6.6  #
     6.7 -# DESCRIPTION: generate outer syntax keyword files from session logs
     6.8 +# DESCRIPTION: generate keyword files for Emacs Proof General
     6.9  
    6.10  
    6.11  ## diagnostics
    6.12 @@ -12,13 +12,13 @@
    6.13  function usage()
    6.14  {
    6.15    echo
    6.16 -  echo "Usage: isabelle $PRG [OPTIONS] [LOGS ...]"
    6.17 +  echo "Usage: isabelle $PRG [OPTIONS] [SESSIONS ...]"
    6.18    echo
    6.19    echo "  Options are:"
    6.20 +  echo "    -d DIR       include session directory"
    6.21    echo "    -k NAME      specific name of keywords collection (default: empty)"
    6.22    echo
    6.23 -  echo "  Generate outer syntax keyword files from (compressed) session LOGS."
    6.24 -  echo "  Targets Emacs Proof General."
    6.25 +  echo "  Generate keyword files for Emacs Proof General from Isabelle sessions."
    6.26    echo
    6.27    exit 1
    6.28  }
    6.29 @@ -28,11 +28,15 @@
    6.30  
    6.31  # options
    6.32  
    6.33 +declare -a DIRS=()
    6.34  KEYWORDS_NAME=""
    6.35  
    6.36 -while getopts "k:" OPT
    6.37 +while getopts "d:k:" OPT
    6.38  do
    6.39    case "$OPT" in
    6.40 +    d)
    6.41 +      DIRS["${#DIRS[@]}"]="$OPTARG"
    6.42 +      ;;
    6.43      k)
    6.44        KEYWORDS_NAME="$OPTARG"
    6.45        ;;
    6.46 @@ -47,23 +51,10 @@
    6.47  
    6.48  ## main
    6.49  
    6.50 -SESSIONS=""
    6.51 -for LOG in "$@"
    6.52 -do
    6.53 -  NAME="$(basename "$LOG" .gz)"
    6.54 -  if [ -z "$SESSIONS" ]; then
    6.55 -    SESSIONS="$NAME"
    6.56 -  else
    6.57 -    SESSIONS="$SESSIONS + $NAME"
    6.58 -  fi
    6.59 -done
    6.60 +[ -e "$ISABELLE_HOME/Admin/build" ] && { "$ISABELLE_HOME/Admin/build" jars || exit $?; }
    6.61  
    6.62 -for LOG in "$@"
    6.63 -do
    6.64 -  if [ "${LOG%.gz}" = "$LOG" ]; then
    6.65 -    cat "$LOG"
    6.66 -  else
    6.67 -    gzip -dc "$LOG"
    6.68 -  fi
    6.69 -  echo
    6.70 -done | "$ISABELLE_HOME/lib/scripts/keywords" "$KEYWORDS_NAME" "$SESSIONS"
    6.71 +declare -a JAVA_ARGS; eval "JAVA_ARGS=($ISABELLE_BUILD_JAVA_OPTIONS)"
    6.72 +
    6.73 +"$ISABELLE_TOOL" java "${JAVA_ARGS[@]}" isabelle.Keywords keywords \
    6.74 +  "$KEYWORDS_NAME" "${DIRS[@]}" $'\n' "$@"
    6.75 +

     7.1 --- a/lib/scripts/keywords	Mon Jun 24 17:17:17 2013 +0200
     7.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.3 @@ -1,153 +0,0 @@
     7.4 -#!/usr/bin/env perl
     7.5 -#
     7.6 -# Author: Makarius
     7.7 -#
     7.8 -# keywords.pl - generate outer syntax keyword files from session logs
     7.9 -#
    7.10 -
    7.11 -use warnings;
    7.12 -use strict;
    7.13 -
    7.14 -
    7.15 -## arguments
    7.16 -
    7.17 -my ($keywords_name, $sessions) = @ARGV;
    7.18 -
    7.19 -
    7.20 -## keywords
    7.21 -
    7.22 -my %keywords;
    7.23 -
    7.24 -sub set_keyword {
    7.25 -  my ($name, $kind) = @_;
    7.26 -  if (defined $keywords{$name} and $keywords{$name} ne $kind and $keywords{$name} ne "minor") {
    7.27 -    if ($kind ne "minor") {
    7.28 -      print STDERR "### Inconsistent declaration of keyword \"${name}\": $keywords{$name} vs ${kind}\n";
    7.29 -      $keywords{$name} = $kind;
    7.30 -    }
    7.31 -  } else {
    7.32 -    $keywords{$name} = $kind;
    7.33 -  }
    7.34 -}
    7.35 -
    7.36 -my %convert_kinds = (
    7.37 -  "thy_begin" => "theory-begin",
    7.38 -  "thy_end" => "theory-end",
    7.39 -  "thy_heading1" => "theory-heading",
    7.40 -  "thy_heading2" => "theory-heading",
    7.41 -  "thy_heading3" => "theory-heading",
    7.42 -  "thy_heading4" => "theory-heading",
    7.43 -  "thy_load" => "theory-decl",
    7.44 -  "thy_decl" => "theory-decl",
    7.45 -  "thy_script" => "theory-script",
    7.46 -  "thy_goal" => "theory-goal",
    7.47 -  "qed_block" => "qed-block",
    7.48 -  "qed_global" => "qed-global",
    7.49 -  "prf_heading2" => "proof-heading",
    7.50 -  "prf_heading3" => "proof-heading",
    7.51 -  "prf_heading4" => "proof-heading",
    7.52 -  "prf_goal" => "proof-goal",
    7.53 -  "prf_block" => "proof-block",
    7.54 -  "prf_open" => "proof-open",
    7.55 -  "prf_close" => "proof-close",
    7.56 -  "prf_chain" => "proof-chain",
    7.57 -  "prf_decl" => "proof-decl",
    7.58 -  "prf_asm" => "proof-asm",
    7.59 -  "prf_asm_goal" => "proof-asm-goal",
    7.60 -  "prf_script" => "proof-script"
    7.61 -);
    7.62 -
    7.63 -my @emacs_kinds = (
    7.64 -  "major",
    7.65 -  "minor",
    7.66 -  "control",
    7.67 -  "diag",
    7.68 -  "theory-begin",
    7.69 -  "theory-switch",
    7.70 -  "theory-end",
    7.71 -  "theory-heading",
    7.72 -  "theory-decl",
    7.73 -  "theory-script",
    7.74 -  "theory-goal",
    7.75 -  "qed",
    7.76 -  "qed-block",
    7.77 -  "qed-global",
    7.78 -  "proof-heading",
    7.79 -  "proof-goal",
    7.80 -  "proof-block",
    7.81 -  "proof-open",
    7.82 -  "proof-close",
    7.83 -  "proof-chain",
    7.84 -  "proof-decl",
    7.85 -  "proof-asm",
    7.86 -  "proof-asm-goal",
    7.87 -  "proof-script"
    7.88 -);
    7.89 -
    7.90 -sub collect_keywords {
    7.91 -  while(<STDIN>) {
    7.92 -    if (m/^\fOuter syntax keyword "([^"]*)" :: (\S*)/) {
    7.93 -      my $name = $1;
    7.94 -      my $kind = $2;
    7.95 -      if (defined $convert_kinds{$kind}) { $kind = $convert_kinds{$kind} }
    7.96 -      &set_keyword($name, $kind);
    7.97 -    }
    7.98 -    elsif (m/^\fOuter syntax keyword "([^"]*)"/) {
    7.99 -      my $name = $1;
   7.100 -      &set_keyword($name, "minor");
   7.101 -    }
   7.102 -  }
   7.103 -}
   7.104 -
   7.105 -
   7.106 -## Emacs output
   7.107 -
   7.108 -sub emacs_output {
   7.109 -  my $file = $keywords_name eq "" ? "isar-keywords.el" : "isar-keywords-${keywords_name}.el";
   7.110 -  open (OUTPUT, "> ${file}") || die "$!";
   7.111 -  select OUTPUT;
   7.112 -
   7.113 -  print ";;\n";
   7.114 -  print ";; Keyword classification tables for Isabelle/Isar.\n";
   7.115 -  print ";; Generated from ${sessions}.\n";
   7.116 -  print ";; *** DO NOT EDIT *** DO NOT EDIT *** DO NOT EDIT ***\n";
   7.117 -  print ";;\n";
   7.118 -
   7.119 -  for my $kind (@emacs_kinds) {
   7.120 -    my @names;
   7.121 -    for my $name (keys(%keywords)) {
   7.122 -      if ($kind eq "major" ? $keywords{$name} ne "minor" : $keywords{$name} eq $kind) {
   7.123 -        if ($kind ne "minor" or $name =~ m/^[A-Za-z0-9_]+$/) {
   7.124 -          push @names, $name;
   7.125 -        }
   7.126 -      }
   7.127 -    }
   7.128 -    @names = sort(@names);
   7.129 -
   7.130 -    print "\n(defconst isar-keywords-${kind}";
   7.131 -    print "\n  '(";
   7.132 -    my $first = 1;
   7.133 -    for my $name (@names) {
   7.134 -      $name =~ s/([\.\*\+\?\[\]\^\$])/\\\\$1/g;
   7.135 -      if ($first) {
   7.136 -        print "\"${name}\"";
   7.137 -        $first = 0;
   7.138 -      }
   7.139 -      else {
   7.140 -        print "\n    \"${name}\"";
   7.141 -      }
   7.142 -    }
   7.143 -    print "))\n";
   7.144 -  }
   7.145 -  print "\n(provide 'isar-keywords)\n";
   7.146 -
   7.147 -  close OUTPUT;
   7.148 -  select;
   7.149 -  print STDERR "${file}\n";
   7.150 -}
   7.151 -
   7.152 -
   7.153 -## main
   7.154 -
   7.155 -&collect_keywords();
   7.156 -&emacs_output();

     8.1 --- a/src/Pure/Isar/outer_syntax.scala	Mon Jun 24 17:17:17 2013 +0200
     8.2 +++ b/src/Pure/Isar/outer_syntax.scala	Mon Jun 24 23:33:14 2013 +0200
     8.3 @@ -37,9 +37,6 @@
     8.4    val empty: Outer_Syntax = new Outer_Syntax()
     8.5  
     8.6    def init(): Outer_Syntax = new Outer_Syntax(completion = Completion.init())
     8.7 -
     8.8 -  def init_pure(): Outer_Syntax =
     8.9 -    init() + ("theory", Keyword.THY_BEGIN) + ("ML_file", Keyword.THY_LOAD)
    8.10  }
    8.11  
    8.12  final class Outer_Syntax private(
    8.13 @@ -76,11 +73,11 @@
    8.14  
    8.15    def add_keywords(keywords: Thy_Header.Keywords): Outer_Syntax =
    8.16      (this /: keywords) {
    8.17 -      case (syntax, ((name, Some((kind, _)), replace))) =>
    8.18 +      case (syntax, (name, Some((kind, _)), replace)) =>
    8.19          syntax +
    8.20            (Symbol.decode(name), kind, replace) +
    8.21            (Symbol.encode(name), kind, replace)
    8.22 -      case (syntax, ((name, None, replace))) =>
    8.23 +      case (syntax, (name, None, replace)) =>
    8.24          syntax +
    8.25            (Symbol.decode(name), replace) +
    8.26            (Symbol.encode(name), replace)

     9.1 --- a/src/Pure/Pure.thy	Mon Jun 24 17:17:17 2013 +0200
     9.2 +++ b/src/Pure/Pure.thy	Mon Jun 24 23:33:14 2013 +0200
     9.3 @@ -13,6 +13,8 @@
     9.4      "identifier" "if" "imports" "in" "includes" "infix" "infixl"
     9.5      "infixr" "is" "keywords" "notes" "obtains" "open" "output"
     9.6      "overloaded" "pervasive" "shows" "structure" "unchecked" "where" "|"
     9.7 +  and "theory" :: thy_begin
     9.8 +  and "ML_file" :: thy_load
     9.9    and "header" :: diag
    9.10    and "chapter" :: thy_heading1
    9.11    and "section" :: thy_heading2

    10.1 --- a/src/Pure/Tools/build.scala	Mon Jun 24 17:17:17 2013 +0200
    10.2 +++ b/src/Pure/Tools/build.scala	Mon Jun 24 23:33:14 2013 +0200
    10.3 @@ -394,6 +394,7 @@
    10.4  
    10.5    sealed case class Session_Content(
    10.6      loaded_theories: Set[String],
    10.7 +    keywords: Thy_Header.Keywords,
    10.8      syntax: Outer_Syntax,
    10.9      sources: List[(Path, SHA1.Digest)])
   10.10  
   10.11 @@ -411,7 +412,7 @@
   10.12            val (preloaded, parent_syntax) =
   10.13              info.parent match {
   10.14                case None =>
   10.15 -                (Set.empty[String], Outer_Syntax.init_pure())
   10.16 +                (Set.empty[String], Outer_Syntax.init())
   10.17                case Some(parent_name) =>
   10.18                  val parent = deps(parent_name)
   10.19                  (parent.loaded_theories, parent.syntax)
   10.20 @@ -431,6 +432,7 @@
   10.21                  map(thy => Thy_Load.path_node_name(info.dir + Thy_Load.thy_path(thy))))
   10.22  
   10.23            val loaded_theories = thy_deps.loaded_theories
   10.24 +          val keywords = thy_deps.keywords
   10.25            val syntax = thy_deps.syntax
   10.26  
   10.27            val body_files = if (inlined_files) thy_deps.load_files else Nil
   10.28 @@ -450,19 +452,31 @@
   10.29                    quote(name) + Position.here(info.pos))
   10.30              }
   10.31  
   10.32 -          deps + (name -> Session_Content(loaded_theories, syntax, sources))
   10.33 +          deps + (name -> Session_Content(loaded_theories, keywords, syntax, sources))
   10.34        }))
   10.35  
   10.36 -  def session_content(inlined_files: Boolean, dirs: List[Path], session: String): Session_Content =
   10.37 +  def session_dependencies(
   10.38 +    options: Options,
   10.39 +    inlined_files: Boolean,
   10.40 +    dirs: List[Path],
   10.41 +    sessions: List[String]): Deps =
   10.42    {
   10.43 -    val options = Options.init()
   10.44      val (_, tree) =
   10.45 -      find_sessions(options, dirs.map((false, _))).selection(false, false, Nil, List(session))
   10.46 -    dependencies(Ignore_Progress, inlined_files, false, false, tree)(session)
   10.47 +      find_sessions(options, dirs.map((false, _))).selection(false, false, Nil, sessions)
   10.48 +    dependencies(Ignore_Progress, inlined_files, false, false, tree)
   10.49    }
   10.50  
   10.51 -  def outer_syntax(session: String): Outer_Syntax =
   10.52 -    session_content(false, Nil, session).syntax
   10.53 +  def session_content(
   10.54 +    options: Options,
   10.55 +    inlined_files: Boolean,
   10.56 +    dirs: List[Path],
   10.57 +    session: String): Session_Content =
   10.58 +  {
   10.59 +    session_dependencies(options, inlined_files, dirs, List(session))(session)
   10.60 +  }
   10.61 +
   10.62 +  def outer_syntax(options: Options, session: String): Outer_Syntax =
   10.63 +    session_content(options, false, Nil, session).syntax
   10.64  
   10.65  
   10.66    /* jobs */

    11.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    11.2 +++ b/src/Pure/Tools/keywords.scala	Mon Jun 24 23:33:14 2013 +0200
    11.3 @@ -0,0 +1,163 @@
    11.4 +/*  Title:      Pure/Tools/keywords.scala
    11.5 +    Author:     Makarius
    11.6 +
    11.7 +Generate keyword files for Emacs Proof General.
    11.8 +*/
    11.9 +
   11.10 +package isabelle
   11.11 +
   11.12 +
   11.13 +import scala.collection.mutable
   11.14 +
   11.15 +
   11.16 +object Keywords
   11.17 +{
   11.18 +  /* keywords */
   11.19 +
   11.20 +  private val convert_kinds = Map(
   11.21 +    "thy_begin" -> "theory-begin",
   11.22 +    "thy_end" -> "theory-end",
   11.23 +    "thy_heading1" -> "theory-heading",
   11.24 +    "thy_heading2" -> "theory-heading",
   11.25 +    "thy_heading3" -> "theory-heading",
   11.26 +    "thy_heading4" -> "theory-heading",
   11.27 +    "thy_load" -> "theory-decl",
   11.28 +    "thy_decl" -> "theory-decl",
   11.29 +    "thy_script" -> "theory-script",
   11.30 +    "thy_goal" -> "theory-goal",
   11.31 +    "qed_block" -> "qed-block",
   11.32 +    "qed_global" -> "qed-global",
   11.33 +    "prf_heading2" -> "proof-heading",
   11.34 +    "prf_heading3" -> "proof-heading",
   11.35 +    "prf_heading4" -> "proof-heading",
   11.36 +    "prf_goal" -> "proof-goal",
   11.37 +    "prf_block" -> "proof-block",
   11.38 +    "prf_open" -> "proof-open",
   11.39 +    "prf_close" -> "proof-close",
   11.40 +    "prf_chain" -> "proof-chain",
   11.41 +    "prf_decl" -> "proof-decl",
   11.42 +    "prf_asm" -> "proof-asm",
   11.43 +    "prf_asm_goal" -> "proof-asm-goal",
   11.44 +    "prf_script" -> "proof-script"
   11.45 +  ).withDefault((s: String) => s)
   11.46 +
   11.47 +  private val emacs_kinds = List(
   11.48 +    "major",
   11.49 +    "minor",
   11.50 +    "control",
   11.51 +    "diag",
   11.52 +    "theory-begin",
   11.53 +    "theory-switch",
   11.54 +    "theory-end",
   11.55 +    "theory-heading",
   11.56 +    "theory-decl",
   11.57 +    "theory-script",
   11.58 +    "theory-goal",
   11.59 +    "qed",
   11.60 +    "qed-block",
   11.61 +    "qed-global",
   11.62 +    "proof-heading",
   11.63 +    "proof-goal",
   11.64 +    "proof-block",
   11.65 +    "proof-open",
   11.66 +    "proof-close",
   11.67 +    "proof-chain",
   11.68 +    "proof-decl",
   11.69 +    "proof-asm",
   11.70 +    "proof-asm-goal",
   11.71 +    "proof-script")
   11.72 +
   11.73 +  def keywords(
   11.74 +    options: Options,
   11.75 +    name: String = "",
   11.76 +    dirs: List[Path] = Nil,
   11.77 +    sessions: List[String] = Nil)
   11.78 +  {
   11.79 +    val deps = Build.session_dependencies(options, false, dirs, sessions).deps
   11.80 +    val keywords =
   11.81 +    {
   11.82 +      var keywords = Map.empty[String, String]
   11.83 +      for {
   11.84 +        (_, dep) <- deps
   11.85 +        (name, kind_spec, _) <- dep.keywords
   11.86 +        kind = kind_spec match { case Some(((kind, _), _)) => kind case None => "minor" }
   11.87 +        k = convert_kinds(kind)
   11.88 +      } {
   11.89 +        keywords.get(name) match {
   11.90 +          case Some(k1) if k1 != k && k1 != "minor" && k != "minor" =>
   11.91 +            error("Inconsistent declaration of keyword " + quote(name) + ": " + k1 + " vs " + k)
   11.92 +          case _ =>
   11.93 +        }
   11.94 +        keywords += (name -> k)
   11.95 +      }
   11.96 +      keywords
   11.97 +    }
   11.98 +
   11.99 +    val output =
  11.100 +    {
  11.101 +      val out = new mutable.StringBuilder
  11.102 +
  11.103 +      out ++= ";;\n"
  11.104 +      out ++= ";; Generated keyword classification tables for Isabelle/Isar.\n"
  11.105 +      out ++= ";; *** DO NOT EDIT *** DO NOT EDIT *** DO NOT EDIT ***\n"
  11.106 +      out ++= ";;\n"
  11.107 +
  11.108 +      for (kind <- emacs_kinds) {
  11.109 +        val names =
  11.110 +          (for {
  11.111 +            (name, k) <- keywords.iterator
  11.112 +            if (if (kind == "major") k != "minor" else k == kind)
  11.113 +            if kind != "minor" || Symbol.is_ascii_identifier(name)
  11.114 +          } yield name).toList.sorted
  11.115 +
  11.116 +        out ++= "\n(defconst isar-keywords-" + kind
  11.117 +        out ++= "\n  '("
  11.118 +        out ++=
  11.119 +          names.map(name => quote("""[\.\*\+\?\[\]\^\$]""".r replaceAllIn (name, """\\\\$0""")))
  11.120 +            .mkString("\n    ")
  11.121 +        out ++= "))\n"
  11.122 +      }
  11.123 +
  11.124 +      out ++= "\n(provide 'isar-keywords)\n"
  11.125 +
  11.126 +      out.toString
  11.127 +    }
  11.128 +
  11.129 +    val file = if (name == "") "isar-keywords.el" else "isar-keywords-" + name + ".el"
  11.130 +    java.lang.System.err.println(file)
  11.131 +    File.write(Path.explode(file), output)
  11.132 +  }
  11.133 +
  11.134 +
  11.135 +  /* administrative update_keywords */
  11.136 +
  11.137 +  def update_keywords(options: Options)
  11.138 +  {
  11.139 +    val tree = Build.find_sessions(options, Nil)
  11.140 +
  11.141 +    def chapter(ch: String): List[String] =
  11.142 +      for ((name, info) <- tree.topological_order if info.chapter == ch) yield name
  11.143 +
  11.144 +    keywords(options, sessions = chapter("HOL"))
  11.145 +    keywords(options, name = "ZF", sessions = chapter("ZF"))
  11.146 +  }
  11.147 +
  11.148 +
  11.149 +  /* command line entry point */
  11.150 +
  11.151 +  def main(args: Array[String])
  11.152 +  {
  11.153 +    Command_Line.tool {
  11.154 +      args.toList match {
  11.155 +        case "keywords" :: name :: Command_Line.Chunks(dirs, sessions) =>
  11.156 +          keywords(Options.init(), name, dirs.map(Path.explode), sessions)
  11.157 +          0
  11.158 +        case "update_keywords" :: Nil =>
  11.159 +          update_keywords(Options.init())
  11.160 +          0
  11.161 +        case _ => error("Bad arguments:\n" + cat_lines(args))
  11.162 +      }
  11.163 +    }
  11.164 +  }
  11.165 +}
  11.166 +

    12.1 --- a/src/Pure/build-jars	Mon Jun 24 17:17:17 2013 +0200
    12.2 +++ b/src/Pure/build-jars	Mon Jun 24 23:33:14 2013 +0200
    12.3 @@ -68,6 +68,7 @@
    12.4    Thy/thy_syntax.scala
    12.5    Tools/build.scala
    12.6    Tools/build_dialog.scala
    12.7 +  Tools/keywords.scala
    12.8    Tools/main.scala
    12.9    Tools/ml_statistics.scala
   12.10    Tools/task_statistics.scala

    13.1 --- a/src/Tools/jEdit/src/isabelle_logic.scala	Mon Jun 24 17:17:17 2013 +0200
    13.2 +++ b/src/Tools/jEdit/src/isabelle_logic.scala	Mon Jun 24 23:33:14 2013 +0200
    13.3 @@ -79,7 +79,7 @@
    13.4    {
    13.5      val dirs = session_dirs()
    13.6      val name = session_args().last
    13.7 -    Build.session_content(inlined_files, dirs, name)
    13.8 +    Build.session_content(PIDE.options.value, inlined_files, dirs, name)
    13.9    }
   13.10  }
   13.11