# HG changeset patch
# User wenzelm
# Date 1337871930 -7200
# Node ID 4e9df6ffcc6ef3eebefdb967ac8c6521c7aaf572
# Parent  ca7104aebb74db57f603adfedc629315413d7c24
reparse descendants after update of imports, e.g. required for 'primrec' (line 17 of "src/HOL/Power.thy");

diff -r ca7104aebb74 -r 4e9df6ffcc6e src/Pure/Thy/thy_syntax.scala
--- a/src/Pure/Thy/thy_syntax.scala	Thu May 24 15:54:38 2012 +0200
+++ b/src/Pure/Thy/thy_syntax.scala	Thu May 24 17:05:30 2012 +0200
@@ -128,7 +128,8 @@
     edits: List[Document.Edit_Text])
     : (Outer_Syntax, List[Document.Node.Name], Document.Nodes, List[Document.Edit_Command]) =
   {
-    var rebuild_syntax = previous.is_init
+    var updated_imports = false
+    var updated_keywords = false
     var nodes = previous.nodes
     val doc_edits = new mutable.ListBuffer[Document.Edit_Command]
 
@@ -142,7 +143,8 @@
           }
         if (update_header) {
           val node1 = node.update_header(header)
-          rebuild_syntax = rebuild_syntax || (node.keywords != node1.keywords)
+          updated_imports = updated_imports || (node.imports != node1.imports)
+          updated_keywords = updated_keywords || (node.keywords != node1.keywords)
           nodes += (name -> node1)
           doc_edits += (name -> Document.Node.Header(header))
         }
@@ -150,12 +152,13 @@
     }
 
     val syntax =
-      if (rebuild_syntax)
+      if (previous.is_init || updated_keywords)
         (base_syntax /: nodes.entries)({ case (syn, (_, node)) => (syn /: node.keywords)(_ + _) })
       else previous.syntax
 
     val reparse =
-      if (rebuild_syntax) nodes.descendants(doc_edits.iterator.map(_._1).toList)
+      if (updated_imports || updated_keywords)
+        nodes.descendants(doc_edits.iterator.map(_._1).toList)
       else Nil
 
     (syntax, reparse, nodes, doc_edits.toList)