reparse descendants after update of imports, e.g. required for 'primrec' (line 17 of "src/HOL/Power.thy");
authorwenzelm
Thu May 24 17:05:30 2012 +0200 (2012-05-24)
changeset 479874e9df6ffcc6e
parent 47986 ca7104aebb74
child 47988 e4b69e10b990
reparse descendants after update of imports, e.g. required for 'primrec' (line 17 of "src/HOL/Power.thy");
src/Pure/Thy/thy_syntax.scala
     1.1 --- a/src/Pure/Thy/thy_syntax.scala	Thu May 24 15:54:38 2012 +0200
     1.2 +++ b/src/Pure/Thy/thy_syntax.scala	Thu May 24 17:05:30 2012 +0200
     1.3 @@ -128,7 +128,8 @@
     1.4      edits: List[Document.Edit_Text])
     1.5      : (Outer_Syntax, List[Document.Node.Name], Document.Nodes, List[Document.Edit_Command]) =
     1.6    {
     1.7 -    var rebuild_syntax = previous.is_init
     1.8 +    var updated_imports = false
     1.9 +    var updated_keywords = false
    1.10      var nodes = previous.nodes
    1.11      val doc_edits = new mutable.ListBuffer[Document.Edit_Command]
    1.12  
    1.13 @@ -142,7 +143,8 @@
    1.14            }
    1.15          if (update_header) {
    1.16            val node1 = node.update_header(header)
    1.17 -          rebuild_syntax = rebuild_syntax || (node.keywords != node1.keywords)
    1.18 +          updated_imports = updated_imports || (node.imports != node1.imports)
    1.19 +          updated_keywords = updated_keywords || (node.keywords != node1.keywords)
    1.20            nodes += (name -> node1)
    1.21            doc_edits += (name -> Document.Node.Header(header))
    1.22          }
    1.23 @@ -150,12 +152,13 @@
    1.24      }
    1.25  
    1.26      val syntax =
    1.27 -      if (rebuild_syntax)
    1.28 +      if (previous.is_init || updated_keywords)
    1.29          (base_syntax /: nodes.entries)({ case (syn, (_, node)) => (syn /: node.keywords)(_ + _) })
    1.30        else previous.syntax
    1.31  
    1.32      val reparse =
    1.33 -      if (rebuild_syntax) nodes.descendants(doc_edits.iterator.map(_._1).toList)
    1.34 +      if (updated_imports || updated_keywords)
    1.35 +        nodes.descendants(doc_edits.iterator.map(_._1).toList)
    1.36        else Nil
    1.37  
    1.38      (syntax, reparse, nodes, doc_edits.toList)