class Outer_Keyword wraps symbol interpretation, lexicon, keyword table;

--- a/src/Pure/Isar/outer_keyword.scala	Tue Dec 22 14:58:13 2009 +0100
+++ b/src/Pure/Isar/outer_keyword.scala	Tue Dec 22 15:00:03 2009 +0100
@@ -1,13 +1,16 @@
 /*  Title:      Pure/Isar/outer_keyword.scala
     Author:     Makarius
 
-Isar command keyword classification.
+Isar command keyword classification and keyword tables.
 */
 
 package isabelle
 
 
-object OuterKeyword
+import scala.util.parsing.input.{Reader, CharSequenceReader}
+
+
+object Outer_Keyword
 {
   val MINOR = "minor"
   val CONTROL = "control"
@@ -45,3 +48,43 @@
   val improper = Set(THY_SCRIPT, PRF_SCRIPT)
 }
 
+
+class Outer_Keyword(symbols: Symbol.Interpretation)
+{
+  protected val lexicon: Scan.Lexicon = Scan.Lexicon.empty
+  protected val keywords: Map[String, String] = Map((";" -> Outer_Keyword.DIAG))
+
+  def keyword(name: String, kind: String): Outer_Keyword =
+  {
+    val new_lexicon = lexicon + name
+    val new_keywords = keywords + (name -> kind)
+    new Outer_Keyword(symbols) {
+      override val lexicon = new_lexicon
+      override val keywords = new_keywords
+    }
+  }
+
+  def keyword(name: String): Outer_Keyword = keyword(name, Outer_Keyword.MINOR)
+
+  def is_command(name: String): Boolean =
+    keywords.get(name) match {
+      case Some(kind) => kind != Outer_Keyword.MINOR
+      case None => false
+    }
+
+
+  /* tokenize */
+
+  def tokenize(input: Reader[Char]): List[Outer_Lex.Token] =
+  {
+    import lexicon._
+
+    parseAll(rep(token(symbols, is_command)), input) match {
+      case Success(tokens, _) => tokens
+      case _ => error("Failed to tokenize input:\n" + input.source.toString)
+    }
+  }
+
+  def tokenize(input: CharSequence): List[Outer_Lex.Token] =
+    tokenize(new CharSequenceReader(input))
+}