# HG changeset patch
# User wenzelm
# Date 1331802981 -3600
# Node ID a40be2f10ca90de461fa5915a642153a15212ce6
# Parent  5b67ac48b384682c808e39c54951ac69b04d176c
explicit Outer_Syntax.Decl;

diff -r 5b67ac48b384 -r a40be2f10ca9 src/Pure/Isar/outer_syntax.scala
--- a/src/Pure/Isar/outer_syntax.scala	Thu Mar 15 09:55:42 2012 +0100
+++ b/src/Pure/Isar/outer_syntax.scala	Thu Mar 15 10:16:21 2012 +0100
@@ -34,6 +34,7 @@
     result.toString
   }
 
+  type Decl = (String, Option[(String, List[String])])
   def init(): Outer_Syntax = new Outer_Syntax()
 }
 
@@ -51,8 +52,12 @@
       if (Keyword.control(kind)) completion else completion + (name, replace))
 
   def + (name: String, kind: String): Outer_Syntax = this + (name, kind, name)
-
   def + (name: String): Outer_Syntax = this + (name, Keyword.MINOR)
+  def + (decl: Outer_Syntax.Decl): Outer_Syntax =
+    decl match {
+      case ((name, Some((kind, _)))) => this + (name, kind)
+      case ((name, None)) => this + name
+    }
 
   def is_command(name: String): Boolean =
     keyword_kind(name) match {
diff -r 5b67ac48b384 -r a40be2f10ca9 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Thu Mar 15 09:55:42 2012 +0100
+++ b/src/Pure/PIDE/document.scala	Thu Mar 15 10:16:21 2012 +0100
@@ -41,7 +41,7 @@
   {
     sealed case class Deps(
       imports: List[Name],
-      keywords: List[(String, Option[(String, List[String])])],
+      keywords: List[Outer_Syntax.Decl],
       uses: List[(String, Boolean)])
 
     object Name
diff -r 5b67ac48b384 -r a40be2f10ca9 src/Pure/Thy/thy_header.scala
--- a/src/Pure/Thy/thy_header.scala	Thu Mar 15 09:55:42 2012 +0100
+++ b/src/Pure/Thy/thy_header.scala	Thu Mar 15 10:16:21 2012 +0100
@@ -113,7 +113,7 @@
 
 sealed case class Thy_Header(
   name: String, imports: List[String],
-  keywords: List[(String, Option[(String, List[String])])],
+  keywords: List[Outer_Syntax.Decl],
   uses: List[(String, Boolean)])
 {
   def map(f: String => String): Thy_Header =