# HG changeset patch
# User wenzelm
# Date 1345560978 -7200
# Node ID 18b17f15bc62d242381f94a5fa9bbf7d7f5ff277
# Parent  6124e0d1120af591c277f2e487dfc4b4ebc81a82
more direct cumulation of (sparse) keywords;
discontinued slightly odd patching of Pure keywords;
tuned signature;

diff -r 6124e0d1120a -r 18b17f15bc62 src/Pure/Isar/outer_syntax.scala
--- a/src/Pure/Isar/outer_syntax.scala	Tue Aug 21 14:54:29 2012 +0200
+++ b/src/Pure/Isar/outer_syntax.scala	Tue Aug 21 16:56:18 2012 +0200
@@ -71,8 +71,8 @@
   def + (name: String, kind: String): Outer_Syntax = this + (name, (kind, Nil), name)
   def + (name: String): Outer_Syntax = this + (name, Keyword.MINOR)
 
-  def add_keywords(header: Document.Node.Header): Outer_Syntax =
-    (this /: header.keywords) {
+  def add_keywords(keywords: Thy_Header.Keywords): Outer_Syntax =
+    (this /: keywords) {
       case (syntax, ((name, Some((kind, _))))) =>
         syntax + (Symbol.decode(name), kind) + (Symbol.encode(name), kind)
       case (syntax, ((name, None))) =>
diff -r 6124e0d1120a -r 18b17f15bc62 src/Pure/Thy/thy_info.scala
--- a/src/Pure/Thy/thy_info.scala	Tue Aug 21 14:54:29 2012 +0200
+++ b/src/Pure/Thy/thy_info.scala	Tue Aug 21 16:56:18 2012 +0200
@@ -28,36 +28,30 @@
 
   object Dependencies
   {
-    val empty = new Dependencies(Nil, Set.empty)
+    val empty = new Dependencies(Nil, Nil, Set.empty)
   }
 
   final class Dependencies private(
     rev_deps: List[Dep],
+    val keywords: Thy_Header.Keywords,
     val seen: Set[Document.Node.Name])
   {
-    def :: (dep: Dep): Dependencies = new Dependencies(dep :: rev_deps, seen)
-    def + (name: Document.Node.Name): Dependencies = new Dependencies(rev_deps, seen = seen + name)
+    def :: (dep: Dep): Dependencies =
+      new Dependencies(dep :: rev_deps, dep._2.keywords ::: keywords, seen)
+
+    def + (name: Document.Node.Name): Dependencies =
+      new Dependencies(rev_deps, keywords, seen = seen + name)
 
     def deps: List[Dep] = rev_deps.reverse
 
     def thy_load_commands: List[String] =
-      (for ((_, h) <- rev_deps; (cmd, Some(((Keyword.THY_LOAD, _), _))) <- h.keywords) yield cmd) :::
+      (for ((cmd, Some(((Keyword.THY_LOAD, _), _))) <- keywords) yield cmd) :::
         thy_load.base_syntax.thy_load_commands
 
     def loaded_theories: Set[String] =
       (thy_load.loaded_theories /: rev_deps) { case (loaded, (name, _)) => loaded + name.theory }
 
-    def syntax: Outer_Syntax =
-      (thy_load.base_syntax /: rev_deps) { case (syn, (name, h)) =>
-        val syn1 = syn.add_keywords(h)
-        // FIXME avoid hardwired stuff!?
-        // FIXME broken?!
-        if (name.theory == "Pure")
-          syn1 +
-            ("hence", (Keyword.PRF_ASM_GOAL, Nil), "then have") +
-            ("thus", (Keyword.PRF_ASM_GOAL, Nil), "then show")
-        else syn1
-      }
+    def syntax: Outer_Syntax = thy_load.base_syntax.add_keywords(keywords)
   }
 
   private def require_thys(initiators: List[Document.Node.Name],
diff -r 6124e0d1120a -r 18b17f15bc62 src/Pure/Thy/thy_syntax.scala
--- a/src/Pure/Thy/thy_syntax.scala	Tue Aug 21 14:54:29 2012 +0200
+++ b/src/Pure/Thy/thy_syntax.scala	Tue Aug 21 16:56:18 2012 +0200
@@ -150,7 +150,9 @@
 
     val syntax =
       if (previous.is_init || updated_keywords)
-        (base_syntax /: nodes.entries) { case (syn, (_, node)) => syn.add_keywords(node.header) }
+        (base_syntax /: nodes.entries) {
+          case (syn, (_, node)) => syn.add_keywords(node.header.keywords)
+        }
       else previous.syntax
 
     val reparse =