src/Pure/Thy/thy_syntax.scala
changeset 44157 a21d3e1e64fd
parent 44156 6aa25b80e1a5
child 44160 8848867501fb
     1.1 --- a/src/Pure/Thy/thy_syntax.scala	Thu Aug 11 18:01:28 2011 +0200
     1.2 +++ b/src/Pure/Thy/thy_syntax.scala	Thu Aug 11 20:32:44 2011 +0200
     1.3 @@ -102,9 +102,8 @@
     1.4    def text_edits(
     1.5        syntax: Outer_Syntax,
     1.6        previous: Document.Version,
     1.7 -      edits: List[Document.Edit_Text],
     1.8 -      headers: List[(String, Document.Node.Header)])
     1.9 -    : (List[Document.Edit_Command], List[(String, Thy_Header.Header)], Document.Version) =
    1.10 +      edits: List[Document.Edit_Text])
    1.11 +    : (List[Document.Edit_Command], Document.Version) =
    1.12    {
    1.13      /* phase 1: edit individual command source */
    1.14  
    1.15 @@ -173,25 +172,10 @@
    1.16      }
    1.17  
    1.18  
    1.19 -    /* node header */
    1.20 -
    1.21 -    def node_header(name: String, node: Document.Node)
    1.22 -        : (List[(String, Thy_Header.Header)], Document.Node.Header) =
    1.23 -      (node.header.thy_header, headers.find(p => p._1 == name).map(_._2)) match {
    1.24 -        case (Exn.Res(thy_header0), Some(header @ Document.Node.Header(_, Exn.Res(thy_header))))
    1.25 -        if thy_header0 != thy_header =>
    1.26 -          (List((name, thy_header)), header)
    1.27 -        case (Exn.Exn(_), Some(header @ Document.Node.Header(_, Exn.Res(thy_header)))) =>
    1.28 -          (List((name, thy_header)), header)
    1.29 -        case _ => (Nil, node.header)
    1.30 -      }
    1.31 -
    1.32 -
    1.33      /* resulting document edits */
    1.34  
    1.35      {
    1.36        val doc_edits = new mutable.ListBuffer[Document.Edit_Command]
    1.37 -      val header_edits = new mutable.ListBuffer[(String, Thy_Header.Header)]
    1.38        var nodes = previous.nodes
    1.39  
    1.40        edits foreach {
    1.41 @@ -213,13 +197,19 @@
    1.42              inserted_commands.map(cmd => (commands2.prev(cmd), Some(cmd)))
    1.43  
    1.44            doc_edits += (name -> Document.Node.Edits(cmd_edits))
    1.45 -
    1.46 -          val (new_headers, new_header) = node_header(name, node)
    1.47 -          header_edits ++= new_headers
    1.48 +          nodes += (name -> node.copy(commands = commands2))
    1.49  
    1.50 -          nodes += (name -> Document.Node(new_header, node.blobs, commands2))
    1.51 +        case (name, Document.Node.Update_Header(header)) =>
    1.52 +          val node = nodes(name)
    1.53 +          val update_header =
    1.54 +            (node.header.thy_header, header) match {
    1.55 +              case (Exn.Res(thy_header0), Document.Node.Header(_, Exn.Res(thy_header)))
    1.56 +              if thy_header0 != thy_header => true
    1.57 +              case (Exn.Exn(_), Document.Node.Header(_, Exn.Res(thy_header))) => true
    1.58 +            }
    1.59 +          if (update_header) doc_edits += (name -> Document.Node.Update_Header(header))
    1.60        }
    1.61 -      (doc_edits.toList, header_edits.toList, Document.Version(Document.new_id(), nodes))
    1.62 +      (doc_edits.toList, Document.Version(Document.new_id(), nodes))
    1.63      }
    1.64    }
    1.65  }