src/Pure/Thy/thy_syntax.scala
changeset 40478 4bae781b8f7c
parent 40457 3b0050718b31
child 40479 cc06f5528bb1
     1.1 --- a/src/Pure/Thy/thy_syntax.scala	Thu Nov 11 13:23:39 2010 +0100
     1.2 +++ b/src/Pure/Thy/thy_syntax.scala	Thu Nov 11 16:48:46 2010 +0100
     1.3 @@ -17,10 +17,7 @@
     1.4  
     1.5    object Structure
     1.6    {
     1.7 -    sealed abstract class Entry
     1.8 -    {
     1.9 -      def length: Int
    1.10 -    }
    1.11 +    sealed abstract class Entry { def length: Int }
    1.12      case class Block(val name: String, val body: List[Entry]) extends Entry
    1.13      {
    1.14        val length: Int = (0 /: body)(_ + _.length)
    1.15 @@ -103,7 +100,7 @@
    1.16    /** text edits **/
    1.17  
    1.18    def text_edits(session: Session, previous: Document.Version,
    1.19 -      edits: List[Document.Node_Text_Edit]): (List[Document.Edit[Command]], Document.Version) =
    1.20 +      edits: List[Document.Text_Edit]): (List[Document.Edit[Command]], Document.Version) =
    1.21    {
    1.22      /* phase 1: edit individual command source */
    1.23  
    1.24 @@ -178,20 +175,25 @@
    1.25        val doc_edits = new mutable.ListBuffer[Document.Edit[Command]]
    1.26        var nodes = previous.nodes
    1.27  
    1.28 -      for ((name, text_edits) <- edits) {
    1.29 -        val commands0 = nodes(name).commands
    1.30 -        val commands1 = edit_text(text_edits, commands0)
    1.31 -        val commands2 = recover_spans(commands1)   // FIXME somewhat slow
    1.32 +      edits foreach {
    1.33 +        case (name, None) =>
    1.34 +          doc_edits += (name -> None)
    1.35 +          nodes -= name
    1.36 +
    1.37 +        case (name, Some(text_edits)) =>
    1.38 +          val commands0 = nodes(name).commands
    1.39 +          val commands1 = edit_text(text_edits, commands0)
    1.40 +          val commands2 = recover_spans(commands1)   // FIXME somewhat slow
    1.41  
    1.42 -        val removed_commands = commands0.iterator.filter(!commands2.contains(_)).toList
    1.43 -        val inserted_commands = commands2.iterator.filter(!commands0.contains(_)).toList
    1.44 +          val removed_commands = commands0.iterator.filter(!commands2.contains(_)).toList
    1.45 +          val inserted_commands = commands2.iterator.filter(!commands0.contains(_)).toList
    1.46  
    1.47 -        val cmd_edits =
    1.48 -          removed_commands.reverse.map(cmd => (commands0.prev(cmd), None)) :::
    1.49 -          inserted_commands.map(cmd => (commands2.prev(cmd), Some(cmd)))
    1.50 +          val cmd_edits =
    1.51 +            removed_commands.reverse.map(cmd => (commands0.prev(cmd), None)) :::
    1.52 +            inserted_commands.map(cmd => (commands2.prev(cmd), Some(cmd)))
    1.53  
    1.54 -        doc_edits += (name -> Some(cmd_edits))
    1.55 -        nodes += (name -> new Document.Node(commands2))
    1.56 +          doc_edits += (name -> Some(cmd_edits))
    1.57 +          nodes += (name -> new Document.Node(commands2))
    1.58        }
    1.59        (doc_edits.toList, new Document.Version(session.new_id(), nodes))
    1.60      }