# HG changeset patch
# User wenzelm
# Date 1344338489 -7200
# Node ID e2b512024eab208354b61456e085570590d52733
# Parent  dd32321d6eefce1a98ccbbdc1a5bb1beff99c45f
tuned signature;

diff -r dd32321d6eef -r e2b512024eab src/Pure/Isar/outer_syntax.scala
--- a/src/Pure/Isar/outer_syntax.scala	Tue Aug 07 12:35:24 2012 +0200
+++ b/src/Pure/Isar/outer_syntax.scala	Tue Aug 07 13:21:29 2012 +0200
@@ -34,8 +34,6 @@
     result.toString
   }
 
-  type Decl = (String, Option[(String, List[String])])
-
   val empty: Outer_Syntax = new Outer_Syntax()
   def init(): Outer_Syntax = new Outer_Syntax(completion = Completion.init())
 }
@@ -61,10 +59,15 @@
 
   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 add_keywords(header: Document.Node_Header): Outer_Syntax =
+    header match {
+      case Exn.Res(deps) =>
+        (this /: deps.keywords) {
+          case (syntax, ((name, Some((kind, _))))) => syntax + (name, kind)
+          case (syntax, ((name, None))) => syntax + name
+        }
+      case Exn.Exn(_) => this
     }
 
   def is_command(name: String): Boolean =
diff -r dd32321d6eef -r e2b512024eab src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Tue Aug 07 12:35:24 2012 +0200
+++ b/src/Pure/PIDE/document.scala	Tue Aug 07 13:21:29 2012 +0200
@@ -41,7 +41,7 @@
   {
     sealed case class Deps(
       imports: List[Name],
-      keywords: List[Outer_Syntax.Decl],
+      keywords: Thy_Header.Keywords,
       uses: List[(String, Boolean)])
 
     object Name
@@ -125,7 +125,7 @@
     def imports: List[Node.Name] =
       header match { case Exn.Res(deps) => deps.imports case _ => Nil }
 
-    def keywords: List[Outer_Syntax.Decl] =
+    def keywords: Thy_Header.Keywords =
       header match { case Exn.Res(deps) => deps.keywords case _ => Nil }
 
 
diff -r dd32321d6eef -r e2b512024eab src/Pure/System/build.scala
--- a/src/Pure/System/build.scala	Tue Aug 07 12:35:24 2012 +0200
+++ b/src/Pure/System/build.scala	Tue Aug 07 13:21:29 2012 +0200
@@ -358,9 +358,7 @@
                 map(thy => Document.Node.Name(info.dir + Thy_Load.thy_path(thy))))
 
           val loaded_theories = preloaded ++ thy_deps.map(_._1.theory)
-
-          val keywords = thy_deps.map({ case (_, Exn.Res(h)) => h.keywords case _ => Nil }).flatten
-          val syntax = (parent_syntax /: keywords)(_ + _)
+          val syntax = (parent_syntax /: thy_deps) { case (syn, (_, h)) => syn.add_keywords(h) }
 
           val all_files =
             thy_deps.map({ case (n, h) =>
diff -r dd32321d6eef -r e2b512024eab src/Pure/Thy/thy_header.scala
--- a/src/Pure/Thy/thy_header.scala	Tue Aug 07 12:35:24 2012 +0200
+++ b/src/Pure/Thy/thy_header.scala	Tue Aug 07 13:21:29 2012 +0200
@@ -107,12 +107,17 @@
     try { read(reader).map(Standard_System.decode_permissive_utf8) }
     finally { reader.close }
   }
+
+
+  /* keywords */
+
+  type Keywords = List[(String, Option[(String, List[String])])]
 }
 
 
 sealed case class Thy_Header(
   name: String, imports: List[String],
-  keywords: List[Outer_Syntax.Decl],
+  keywords: Thy_Header.Keywords,
   uses: List[(String, Boolean)])
 {
   def map(f: String => String): Thy_Header =
diff -r dd32321d6eef -r e2b512024eab src/Pure/Thy/thy_syntax.scala
--- a/src/Pure/Thy/thy_syntax.scala	Tue Aug 07 12:35:24 2012 +0200
+++ b/src/Pure/Thy/thy_syntax.scala	Tue Aug 07 13:21:29 2012 +0200
@@ -153,7 +153,7 @@
 
     val syntax =
       if (previous.is_init || updated_keywords)
-        (base_syntax /: nodes.entries)({ case (syn, (_, node)) => (syn /: node.keywords)(_ + _) })
+        (base_syntax /: nodes.entries) { case (syn, (_, node)) => syn.add_keywords(node.header) }
       else previous.syntax
 
     val reparse =