# HG changeset patch
# User wenzelm
# Date 1429895323 -7200
# Node ID 6e8014342c9d2999dd784f7368e208370a3c20c2
# Parent  e12973f1899e15cfc5de2a8e11463080a9d90747
tuned;

diff -r e12973f1899e -r 6e8014342c9d src/Pure/Thy/thy_syntax.scala
--- a/src/Pure/Thy/thy_syntax.scala	Fri Apr 24 16:12:20 2015 +0200
+++ b/src/Pure/Thy/thy_syntax.scala	Fri Apr 24 19:08:43 2015 +0200
@@ -83,7 +83,8 @@
         if (update_header) {
           val node1 = node.update_header(header)
           if (node.header.imports.map(_._1) != node1.header.imports.map(_._1) ||
-              node.header.keywords != node1.header.keywords) syntax_changed0 += name
+              node.header.keywords != node1.header.keywords ||
+              node.header.errors != node1.header.errors) syntax_changed0 += name
           nodes += (name -> node1)
           doc_edits += (name -> Document.Node.Deps(header))
         }
@@ -304,7 +305,7 @@
         val reparse =
           (syntax_changed /: nodes0.iterator)({
             case (reparse, (name, node)) =>
-              if (node.load_commands.exists(_.blobs_changed(doc_blobs)))
+              if (node.load_commands.exists(_.blobs_changed(doc_blobs)) && !reparse.contains(name))
                 name :: reparse
               else reparse
             })