clarified node edits sent to prover -- Clear/Blob only required for text edits within editor;

--- a/src/Pure/PIDE/document.ML	Fri Nov 22 20:54:26 2013 +0100
+++ b/src/Pure/PIDE/document.ML	Fri Nov 22 21:13:44 2013 +0100
@@ -11,7 +11,6 @@
   type node_header = string * Thy_Header.header * string list
   type overlay = Document_ID.command * (string * string list)
   datatype node_edit =
-    Clear |    (* FIXME unused !? *)
     Edits of (Document_ID.command option * Document_ID.command option) list |
     Deps of node_header |
     Perspective of bool * Document_ID.command list * overlay list
@@ -76,7 +75,6 @@
 val no_perspective = make_perspective (false, [], []);
 
 val empty_node = make_node (no_header, no_perspective, Entries.empty, NONE);
-val clear_node = map_node (fn (header, _, _, _) => (header, no_perspective, Entries.empty, NONE));
 
 
 (* basic components *)
@@ -145,7 +143,6 @@
 type overlay = Document_ID.command * (string * string list);
 
 datatype node_edit =
-  Clear |
   Edits of (Document_ID.command option * Document_ID.command option) list |
   Deps of node_header |
   Perspective of bool * Document_ID.command list * overlay list;
@@ -193,8 +190,7 @@
 fun edit_nodes (name, node_edit) (Version nodes) =
   Version
     (case node_edit of
-      Clear => update_node name clear_node nodes
-    | Edits edits => update_node name (edit_node edits) nodes
+      Edits edits => update_node name (edit_node edits) nodes
     | Deps (master, header, errors) =>
         let
           val imports = map fst (#imports header);

--- a/src/Pure/PIDE/document.scala	Fri Nov 22 20:54:26 2013 +0100
+++ b/src/Pure/PIDE/document.scala	Fri Nov 22 21:13:44 2013 +0100
@@ -127,10 +127,11 @@
       }
     }
     case class Clear[A, B]() extends Edit[A, B]
+    case class Blob[A, B]() extends Edit[A, B]
+
     case class Edits[A, B](edits: List[A]) extends Edit[A, B]
     case class Deps[A, B](header: Header) extends Edit[A, B]
     case class Perspective[A, B](required: Boolean, visible: B, overlays: Overlays) extends Edit[A, B]
-    case class Blob[A, B]() extends Edit[A, B]
     type Perspective_Text = Perspective[Text.Edit, Text.Perspective]
     type Perspective_Command = Perspective[Command.Edit, Command.Perspective]
 

--- a/src/Pure/PIDE/protocol.ML	Fri Nov 22 20:54:26 2013 +0100
+++ b/src/Pure/PIDE/protocol.ML	Fri Nov 22 21:13:44 2013 +0100
@@ -62,8 +62,7 @@
             let open XML.Decode in
               list (pair string
                 (variant
-                 [fn ([], []) => Document.Clear,  (* FIXME unused !? *)
-                  fn ([], a) => Document.Edits (list (pair (option int) (option int)) a),
+                 [fn ([], a) => Document.Edits (list (pair (option int) (option int)) a),
                   fn ([], a) =>
                     let
                       val (master, (name, (imports, (keywords, errors)))) =

--- a/src/Pure/PIDE/protocol.scala	Fri Nov 22 20:54:26 2013 +0100
+++ b/src/Pure/PIDE/protocol.scala	Fri Nov 22 21:13:44 2013 +0100
@@ -352,8 +352,6 @@
       def encode_edit(name: Document.Node.Name)
           : T[Document.Node.Edit[Command.Edit, Command.Perspective]] =
         variant(List(
-          // FIXME Document.Node.Blob (!??)
-          { case Document.Node.Clear() => (Nil, Nil) },  // FIXME unused !?
           { case Document.Node.Edits(a) => (Nil, list(pair(option(id), option(id)))(a)) },
           { case Document.Node.Deps(header) =>
               val master_dir = Isabelle_System.posix_path(name.master_dir)

--- a/src/Pure/Thy/thy_syntax.scala	Fri Nov 22 20:54:26 2013 +0100
+++ b/src/Pure/Thy/thy_syntax.scala	Fri Nov 22 21:13:44 2013 +0100
@@ -397,6 +397,8 @@
     edit match {
       case (_, Document.Node.Clear()) => node.clear
 
+      case (_, Document.Node.Blob()) => node
+
       case (name, Document.Node.Edits(text_edits)) =>
         val commands0 = node.commands
         val commands1 = edit_text(text_edits, commands0)
@@ -415,8 +417,6 @@
           node.update_perspective(perspective).update_commands(
             consolidate_spans(thy_load, syntax, doc_blobs, reparse_limit,
               name, visible, node.commands))
-
-      case (_, Document.Node.Blob()) => node
     }
   }