always reparse nodes with thy_load commands, to update inlined files;
authorwenzelm
Tue, 19 Nov 2013 13:54:02 +0100
changeset 54518 81a9a54c57fc
parent 54517 044bee8c5e69
child 54519 5fed81762406
always reparse nodes with thy_load commands, to update inlined files;
src/Pure/Thy/thy_syntax.scala
--- a/src/Pure/Thy/thy_syntax.scala	Tue Nov 19 13:39:12 2013 +0100
+++ b/src/Pure/Thy/thy_syntax.scala	Tue Nov 19 13:54:02 2013 +0100
@@ -430,8 +430,15 @@
       edits: List[Document.Edit_Text])
     : (List[Document.Edit_Command], Document.Version) =
   {
-    val (syntax, reparse, nodes0, doc_edits0) =
+    val (syntax, reparse0, nodes0, doc_edits0) =
       header_edits(thy_load.base_syntax, previous, edits)
+
+    val reparse =
+      (reparse0 /: nodes0.entries)({
+        case (reparse, (name, node)) =>
+          if (node.thy_load_commands.isEmpty) reparse
+          else name :: reparse
+        })
     val reparse_set = reparse.toSet
 
     var nodes = nodes0