src/Pure/Thy/thy_syntax.scala
changeset 54518 81a9a54c57fc
parent 54517 044bee8c5e69
child 54519 5fed81762406
     1.1 --- a/src/Pure/Thy/thy_syntax.scala	Tue Nov 19 13:39:12 2013 +0100
     1.2 +++ b/src/Pure/Thy/thy_syntax.scala	Tue Nov 19 13:54:02 2013 +0100
     1.3 @@ -430,8 +430,15 @@
     1.4        edits: List[Document.Edit_Text])
     1.5      : (List[Document.Edit_Command], Document.Version) =
     1.6    {
     1.7 -    val (syntax, reparse, nodes0, doc_edits0) =
     1.8 +    val (syntax, reparse0, nodes0, doc_edits0) =
     1.9        header_edits(thy_load.base_syntax, previous, edits)
    1.10 +
    1.11 +    val reparse =
    1.12 +      (reparse0 /: nodes0.entries)({
    1.13 +        case (reparse, (name, node)) =>
    1.14 +          if (node.thy_load_commands.isEmpty) reparse
    1.15 +          else name :: reparse
    1.16 +        })
    1.17      val reparse_set = reparse.toSet
    1.18  
    1.19      var nodes = nodes0