more frugal edits;
authorwenzelm
Wed Jul 23 16:56:03 2014 +0200 (2014-07-23)
changeset 57621caa37976801f
parent 57620 c30ab960875e
child 57622 2da79fca5708
more frugal edits;
src/Pure/PIDE/document.scala
src/Tools/jEdit/src/document_model.scala
     1.1 --- a/src/Pure/PIDE/document.scala	Wed Jul 23 16:20:07 2014 +0200
     1.2 +++ b/src/Pure/PIDE/document.scala	Wed Jul 23 16:56:03 2014 +0200
     1.3 @@ -156,6 +156,12 @@
     1.4            case _ =>
     1.5          }
     1.6        }
     1.7 +
     1.8 +      def is_void: Boolean =
     1.9 +        this match {
    1.10 +          case Edits(Nil) => true
    1.11 +          case _ => false
    1.12 +        }
    1.13      }
    1.14      case class Clear[A, B]() extends Edit[A, B]
    1.15      case class Blob[A, B](blob: Document.Blob) extends Edit[A, B]
     2.1 --- a/src/Tools/jEdit/src/document_model.scala	Wed Jul 23 16:20:07 2014 +0200
     2.2 +++ b/src/Tools/jEdit/src/document_model.scala	Wed Jul 23 16:56:03 2014 +0200
     2.3 @@ -164,22 +164,26 @@
     2.4        clear: Boolean,
     2.5        text_edits: List[Text.Edit],
     2.6        perspective: Document.Node.Perspective_Text): List[Document.Edit_Text] =
     2.7 -    get_blob() match {
     2.8 -      case None =>
     2.9 -        val header_edit = session.header_edit(node_name, node_header())
    2.10 -        if (clear)
    2.11 -          List(header_edit,
    2.12 -            node_name -> Document.Node.Clear(),
    2.13 -            node_name -> Document.Node.Edits(text_edits),
    2.14 -            node_name -> perspective)
    2.15 -        else
    2.16 -          List(header_edit,
    2.17 -            node_name -> Document.Node.Edits(text_edits),
    2.18 -            node_name -> perspective)
    2.19 -      case Some(blob) =>
    2.20 -        List(node_name -> Document.Node.Blob(blob),
    2.21 -          node_name -> Document.Node.Edits(text_edits))
    2.22 -    }
    2.23 +  {
    2.24 +    val edits: List[Document.Edit_Text] =
    2.25 +      get_blob() match {
    2.26 +        case None =>
    2.27 +          val header_edit = session.header_edit(node_name, node_header())
    2.28 +          if (clear)
    2.29 +            List(header_edit,
    2.30 +              node_name -> Document.Node.Clear(),
    2.31 +              node_name -> Document.Node.Edits(text_edits),
    2.32 +              node_name -> perspective)
    2.33 +          else
    2.34 +            List(header_edit,
    2.35 +              node_name -> Document.Node.Edits(text_edits),
    2.36 +              node_name -> perspective)
    2.37 +        case Some(blob) =>
    2.38 +          List(node_name -> Document.Node.Blob(blob),
    2.39 +            node_name -> Document.Node.Edits(text_edits))
    2.40 +      }
    2.41 +    edits.filterNot(_._2.is_void)
    2.42 +  }
    2.43  
    2.44  
    2.45    /* pending edits */