Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned;
authorwenzelm
Fri, 24 Apr 2015 19:08:43 +0200
changeset 60197 6e8014342c9d
parent 60196 e12973f1899e
child 60198 8483c2883c8c
tuned;
src/Pure/Thy/thy_syntax.scala file | annotate | diff | comparison | revisions 
--- 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
             })
isabelle