# HG changeset patch
# User wenzelm
# Date 1384865642 -3600
# Node ID 81a9a54c57fcf26a8a60abf443f34986d35a1c03
# Parent  044bee8c5e693914fb3f697ae151ab79f690f9d6
always reparse nodes with thy_load commands, to update inlined files;

diff -r 044bee8c5e69 -r 81a9a54c57fc 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