src/Pure/Thy/thy_syntax.scala
changeset 56394 bbf4d512f395
parent 56393 22f533e6a049
child 56473 5b5c750e9763
     1.1 --- a/src/Pure/Thy/thy_syntax.scala	Thu Apr 03 20:53:35 2014 +0200
     1.2 +++ b/src/Pure/Thy/thy_syntax.scala	Thu Apr 03 21:08:00 2014 +0200
     1.3 @@ -153,7 +153,7 @@
     1.4    /** header edits: structure and outer syntax **/
     1.5  
     1.6    private def header_edits(
     1.7 -    base_syntax: Prover.Syntax,
     1.8 +    resources: Resources,
     1.9      previous: Document.Version,
    1.10      edits: List[Document.Edit_Text]):
    1.11      (Prover.Syntax, Boolean, Boolean, List[Document.Node.Name], Document.Nodes,
    1.12 @@ -180,14 +180,16 @@
    1.13      }
    1.14  
    1.15      val (syntax, syntax_changed) =
    1.16 -      if (previous.is_init || updated_keywords) {
    1.17 -        val syntax =
    1.18 -          (base_syntax /: nodes.iterator) {
    1.19 -            case (syn, (_, node)) => syn.add_keywords(node.header.keywords)
    1.20 -          }
    1.21 -        (syntax, true)
    1.22 +      previous.syntax match {
    1.23 +        case Some(syntax) if !updated_keywords =>
    1.24 +          (syntax, false)
    1.25 +        case _ =>
    1.26 +          val syntax =
    1.27 +            (resources.base_syntax /: nodes.iterator) {
    1.28 +              case (syn, (_, node)) => syn.add_keywords(node.header.keywords)
    1.29 +            }
    1.30 +          (syntax, true)
    1.31        }
    1.32 -      else (previous.syntax, false)
    1.33  
    1.34      val reparse =
    1.35        if (updated_imports || updated_keywords)
    1.36 @@ -443,10 +445,10 @@
    1.37        doc_blobs.get(name) orElse previous.nodes(name).get_blob
    1.38  
    1.39      val (syntax, syntax_changed, deps_changed, reparse0, nodes0, doc_edits0) =
    1.40 -      header_edits(resources.base_syntax, previous, edits)
    1.41 +      header_edits(resources, previous, edits)
    1.42  
    1.43      val (doc_edits, version) =
    1.44 -      if (edits.isEmpty) (Nil, Document.Version.make(syntax, previous.nodes))
    1.45 +      if (edits.isEmpty) (Nil, Document.Version.make(Some(syntax), previous.nodes))
    1.46        else {
    1.47          val reparse =
    1.48            (reparse0 /: nodes0.iterator)({
    1.49 @@ -485,7 +487,7 @@
    1.50  
    1.51              nodes += (name -> node2)
    1.52          }
    1.53 -        (doc_edits.toList, Document.Version.make(syntax, nodes))
    1.54 +        (doc_edits.toList, Document.Version.make(Some(syntax), nodes))
    1.55        }
    1.56  
    1.57      Session.Change(previous, doc_blobs, syntax_changed, deps_changed, doc_edits, version)