# HG changeset patch
# User wenzelm
# Date 1483799101 -3600
# Node ID bebe7a164068c11949a5de09a909b17f64712575
# Parent  67a0a563d2b36fcbe3801ec37588e516facdc5ba
obsolete;

diff -r 67a0a563d2b3 -r bebe7a164068 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Sat Jan 07 15:16:36 2017 +0100
+++ b/src/Pure/PIDE/document.scala	Sat Jan 07 15:25:01 2017 +0100
@@ -160,7 +160,6 @@
           case _ => false
         }
     }
-    case class Clear[A, B]() extends Edit[A, B]
     case class Blob[A, B](blob: Document.Blob) extends Edit[A, B]
 
     case class Edits[A, B](edits: List[A]) extends Edit[A, B]
@@ -264,8 +263,6 @@
     def load_commands_changed(doc_blobs: Blobs): Boolean =
       load_commands.exists(_.blobs_changed(doc_blobs))
 
-    def clear: Node = new Node(header = header, syntax = syntax)
-
     def init_blob(blob: Blob): Node = new Node(get_blob = Some(blob.unchanged))
 
     def update_header(new_header: Node.Header): Node =
@@ -761,14 +758,11 @@
           if a == name
         } yield edits
 
-      val is_cleared = rev_pending_changes.exists({ case Node.Clear() => true case _ => false })
       val edits =
-        if (is_cleared) Nil
-        else
-          (pending_edits /: rev_pending_changes)({
-            case (edits, Node.Edits(es)) => es ::: edits
-            case (edits, _) => edits
-          })
+        (pending_edits /: rev_pending_changes)({
+          case (edits, Node.Edits(es)) => es ::: edits
+          case (edits, _) => edits
+        })
       lazy val reverse_edits = edits.reverse
 
       new Snapshot
@@ -782,10 +776,8 @@
 
         /* local node content */
 
-        def convert(offset: Text.Offset) =
-          if (is_cleared) 0 else (offset /: edits)((i, edit) => edit.convert(i))
-        def revert(offset: Text.Offset) =
-          if (is_cleared) 0 else (offset /: reverse_edits)((i, edit) => edit.revert(i))
+        def convert(offset: Text.Offset) = (offset /: edits)((i, edit) => edit.convert(i))
+        def revert(offset: Text.Offset) = (offset /: reverse_edits)((i, edit) => edit.revert(i))
 
         def convert(range: Text.Range) = range.map(convert(_))
         def revert(range: Text.Range) = range.map(revert(_))
diff -r 67a0a563d2b3 -r bebe7a164068 src/Pure/Thy/thy_syntax.scala
--- a/src/Pure/Thy/thy_syntax.scala	Sat Jan 07 15:16:36 2017 +0100
+++ b/src/Pure/Thy/thy_syntax.scala	Sat Jan 07 15:25:01 2017 +0100
@@ -236,8 +236,6 @@
     }
 
     edit match {
-      case (_, Document.Node.Clear()) => node.clear
-
       case (_, Document.Node.Blob(blob)) => node.init_blob(blob)
 
       case (name, Document.Node.Edits(text_edits)) =>