basic support for outer syntax keywords in theory header;

--- a/src/HOL/Library/Old_Recdef.thy	Thu Mar 15 11:37:56 2012 +0100
+++ b/src/HOL/Library/Old_Recdef.thy	Thu Mar 15 14:13:49 2012 +0100
@@ -6,6 +6,7 @@
 
 theory Old_Recdef
 imports Wfrec
+keywords "recdef" :: thy_decl
 uses
   ("~~/src/HOL/Tools/TFL/casesplit.ML")
   ("~~/src/HOL/Tools/TFL/utils.ML")

--- a/src/Pure/PIDE/document.scala	Thu Mar 15 11:37:56 2012 +0100
+++ b/src/Pure/PIDE/document.scala	Thu Mar 15 14:13:49 2012 +0100
@@ -122,6 +122,12 @@
     def update_commands(new_commands: Linear_Set[Command]): Node =
       new Node(header, perspective, blobs, new_commands)
 
+    def imports: List[Node.Name] =
+      header match { case Exn.Res(deps) => deps.imports case _ => Nil }
+
+    def keywords: List[Outer_Syntax.Decl] =
+      header match { case Exn.Res(deps) => deps.keywords case _ => Nil }
+
 
     /* commands */
 
@@ -184,11 +190,7 @@
     def + (entry: (Node.Name, Node)): Nodes =
     {
       val (name, node) = entry
-      val imports =
-        node.header match {
-          case Exn.Res(deps) => deps.imports
-          case _ => Nil
-        }
+      val imports = node.imports
       val graph1 =
         (graph.default_node(name, Node.empty) /: imports)((g, p) => g.default_node(p, Node.empty))
       val graph2 = (graph1 /: graph1.imm_preds(name))((g, dep) => g.del_edge(dep, name))
@@ -199,6 +201,7 @@
     def entries: Iterator[(Node.Name, Node)] =
       graph.entries.map({ case (name, (node, _)) => (name, node) })
 
+    def descendants(names: List[Node.Name]): List[Node.Name] = graph.all_succs(names)
     def topological_order: List[Node.Name] = graph.topological_order
   }
 

--- a/src/Pure/System/session.scala	Thu Mar 15 11:37:56 2012 +0100
+++ b/src/Pure/System/session.scala	Thu Mar 15 14:13:49 2012 +0100
@@ -100,8 +100,7 @@
 
         case Text_Edits(name, previous, text_edits, version_result) =>
           val prev = previous.get_finished
-          val syntax = if (prev.is_init) prover_syntax else prev.syntax
-          val (doc_edits, version) = Thy_Syntax.text_edits(syntax, prev, text_edits)
+          val (doc_edits, version) = Thy_Syntax.text_edits(prover_syntax, prev, text_edits)
           version_result.fulfill(version)
           sender ! Change_Node(name, doc_edits, prev, version)
 

--- a/src/Pure/Thy/thy_syntax.scala	Thu Mar 15 11:37:56 2012 +0100
+++ b/src/Pure/Thy/thy_syntax.scala	Thu Mar 15 14:13:49 2012 +0100
@@ -145,7 +145,7 @@
   /** text edits **/
 
   def text_edits(
-      syntax: Outer_Syntax,
+      base_syntax: Outer_Syntax,
       previous: Document.Version,
       edits: List[Document.Edit_Text])
     : (List[Document.Edit_Command], Document.Version) =
@@ -181,8 +181,10 @@
 
     /* phase 2: recover command spans */
 
-    @tailrec def recover_spans(node_name: Document.Node.Name, commands: Linear_Set[Command])
-      : Linear_Set[Command] =
+    @tailrec def recover_spans(
+      syntax: Outer_Syntax,
+      node_name: Document.Node.Name,
+      commands: Linear_Set[Command]): Linear_Set[Command] =
     {
       commands.iterator.find(cmd => !cmd.is_defined) match {
         case Some(first_unparsed) =>
@@ -211,7 +213,7 @@
           val inserted = spans2.map(span => Command(Document.new_id(), node_name, span))
           val new_commands =
             commands.delete_between(before_edit, after_edit).append_after(before_edit, inserted)
-          recover_spans(node_name, new_commands)
+          recover_spans(syntax, node_name, new_commands)
 
         case None => commands
       }
@@ -223,8 +225,34 @@
     {
       val doc_edits = new mutable.ListBuffer[Document.Edit_Command]
       var nodes = previous.nodes
+      var rebuild_syntax = previous.is_init
 
+      // structure and syntax
       edits foreach {
+        case (name, Document.Node.Header(header)) =>
+          val node = nodes(name)
+          val update_header =
+            (node.header, header) match {
+              case (Exn.Res(deps0), Exn.Res(deps)) => deps0 != deps
+              case _ => true
+            }
+          if (update_header) {
+            doc_edits += (name -> Document.Node.Header(header))
+            val node1 = node.update_header(header)
+            nodes += (name -> node1)
+            rebuild_syntax = rebuild_syntax || (node.keywords != node1.keywords)
+          }
+
+        case _ =>
+      }
+
+      val syntax =
+        if (rebuild_syntax)
+          (base_syntax /: nodes.entries)({ case (syn, (_, node)) => (syn /: node.keywords)(_ + _) })
+        else previous.syntax
+
+      // node content
+      edits foreach {  // FIXME observe rebuild_syntax!?
         case (name, Document.Node.Clear()) =>
           doc_edits += (name -> Document.Node.Clear())
           nodes += (name -> nodes(name).clear)
@@ -233,7 +261,7 @@
           val node = nodes(name)
           val commands0 = node.commands
           val commands1 = edit_text(text_edits, commands0)
-          val commands2 = recover_spans(name, commands1)   // FIXME somewhat slow
+          val commands2 = recover_spans(syntax, name, commands1)   // FIXME somewhat slow
 
           val removed_commands = commands0.iterator.filter(!commands2.contains(_)).toList
           val inserted_commands = commands2.iterator.filter(!commands0.contains(_)).toList
@@ -245,17 +273,7 @@
           doc_edits += (name -> Document.Node.Edits(cmd_edits))
           nodes += (name -> node.update_commands(commands2))
 
-        case (name, Document.Node.Header(header)) =>
-          val node = nodes(name)
-          val update_header =
-            (node.header, header) match {
-              case (Exn.Res(deps0), Exn.Res(deps)) => deps0 != deps
-              case _ => true
-            }
-          if (update_header) {
-            doc_edits += (name -> Document.Node.Header(header))
-            nodes += (name -> node.update_header(header))
-          }
+        case (name, Document.Node.Header(_)) =>
 
         case (name, Document.Node.Perspective(text_perspective)) =>
           update_perspective(nodes, name, text_perspective) match {