explicit datatypes for document node edits;

--- a/src/Pure/PIDE/document.ML	Thu Aug 11 13:24:49 2011 +0200
+++ b/src/Pure/PIDE/document.ML	Thu Aug 11 18:01:28 2011 +0200
@@ -15,7 +15,8 @@
   val new_id: unit -> id
   val parse_id: string -> id
   val print_id: id -> string
-  type edit = string * ((command_id option * command_id option) list) option
+  datatype node_edit = Remove | Edits of (command_id option * command_id option) list
+  type edit = string * node_edit
   type header = string * (string * string list * string list)
   type state
   val init_state: state
@@ -75,10 +76,8 @@
 
 (* node edits and associated executions *)
 
-type edit =
-  string *
-  (*NONE: remove node, SOME: insert/remove commands*)
-  ((command_id option * command_id option) list) option;
+datatype node_edit = Remove | Edits of (command_id option * command_id option) list;
+type edit = string * node_edit;
 
 type header = string * (string * string list * string list);
 
@@ -108,12 +107,12 @@
 fun get_node version name = Graph.get_node (nodes_of version) name
   handle Graph.UNDEF _ => empty_node;
 
-fun edit_nodes (name, SOME edits) (Version nodes) =
+fun edit_nodes (name, Remove) (Version nodes) =
+      Version (perhaps (try (Graph.del_node name)) nodes)
+  | edit_nodes (name, Edits edits) (Version nodes) =
       Version (nodes
         |> Graph.default_node (name, empty_node)
-        |> Graph.map_node name (edit_node edits))
-  | edit_nodes (name, NONE) (Version nodes) =
-      Version (perhaps (try (Graph.del_node name)) nodes);
+        |> Graph.map_node name (edit_node edits));
 
 fun put_node name node (Version nodes) =
   Version (nodes

--- a/src/Pure/PIDE/document.scala	Thu Aug 11 13:24:49 2011 +0200
+++ b/src/Pure/PIDE/document.scala	Thu Aug 11 18:01:28 2011 +0200
@@ -31,16 +31,24 @@
 
   /* named nodes -- development graph */
 
-  type Edit[A] =
-   (String,  // node name
-    Option[List[A]])  // None: remove node, Some: edit content
-
+  type Edit[A] = (String, Node.Edit[A])
   type Edit_Text = Edit[Text.Edit]
   type Edit_Command = Edit[(Option[Command], Option[Command])]
   type Edit_Command_ID = Edit[(Option[Command_ID], Option[Command_ID])]
 
   object Node
   {
+    sealed abstract class Edit[A]
+    {
+      def map[B](f: A => B): Edit[B] =
+        this match {
+          case Remove() => Remove()
+          case Edits(es) => Edits(es.map(f))
+        }
+    }
+    case class Remove[A]() extends Edit[A]
+    case class Edits[A](edits: List[A]) extends Edit[A]
+
     sealed case class Header(val master_dir: Path, val thy_header: Exn.Result[Thy_Header.Header])
     val empty_header = Header(Path.current, Exn.Exn(ERROR("Bad theory header")))
 
@@ -290,10 +298,10 @@
       val stable = found_stable.get
       val latest = history.undo_list.head
 
-      // FIXME proper treatment of deleted nodes
+      // FIXME proper treatment of removed nodes
       val edits =
         (pending_edits /: history.undo_list.takeWhile(_ != stable))((edits, change) =>
-            (for ((a, Some(eds)) <- change.edits if a == name) yield eds).flatten ::: edits)
+            (for ((a, Node.Edits(es)) <- change.edits if a == name) yield es).flatten ::: edits)
       lazy val reverse_edits = edits.reverse
 
       new Snapshot

--- a/src/Pure/PIDE/isar_document.ML	Thu Aug 11 13:24:49 2011 +0200
+++ b/src/Pure/PIDE/isar_document.ML	Thu Aug 11 18:01:28 2011 +0200
@@ -18,8 +18,12 @@
         val old_id = Document.parse_id old_id_string;
         val new_id = Document.parse_id new_id_string;
         val edits = YXML.parse_body edits_yxml |>
-          let open XML.Decode
-          in list (pair string (option (list (pair (option int) (option int))))) end;
+          let open XML.Decode in
+            list (pair string
+              (variant
+               [fn ([], []) => Document.Remove,
+                fn ([], a) => Document.Edits (list (pair (option int) (option int)) a)]))
+          end;
         val headers = YXML.parse_body headers_yxml |>
           let open XML.Decode
           in list (pair string (triple string (list string) (list string))) end;

--- a/src/Pure/PIDE/isar_document.scala	Thu Aug 11 13:24:49 2011 +0200
+++ b/src/Pure/PIDE/isar_document.scala	Thu Aug 11 18:01:28 2011 +0200
@@ -144,7 +144,12 @@
   {
     val arg1 =
     { import XML.Encode._
-      list(pair(string, option(list(pair(option(long), option(long))))))(edits) }
+      def encode: T[List[Document.Edit_Command_ID]] =
+        list(pair(string,
+          variant(List(
+            { case Document.Node.Remove() => (Nil, Nil) },
+            { case Document.Node.Edits(a) => (Nil, list(pair(option(long), option(long)))(a)) }))))
+      encode(edits) }
 
     val arg2 =
     { import XML.Encode._

--- a/src/Pure/System/session.scala	Thu Aug 11 13:24:49 2011 +0200
+++ b/src/Pure/System/session.scala	Thu Aug 11 18:01:28 2011 +0200
@@ -181,7 +181,7 @@
     /* incoming edits */
 
     def handle_edits(name: String,
-        header: Document.Node.Header, edits: List[Option[List[Text.Edit]]])
+        header: Document.Node.Header, edits: List[Document.Node.Edit[Text.Edit]])
     //{{{
     {
       val syntax = current_syntax()
@@ -216,7 +216,7 @@
 
       var former_assignment = global_state().the_assignment(previous).get_finished
       for {
-        (name, Some(cmd_edits)) <- doc_edits
+        (name, Document.Node.Edits(cmd_edits)) <- doc_edits  // FIXME proper coverage!?
         (prev, None) <- cmd_edits
         removed <- previous.nodes(name).commands.get_after(prev)
       } former_assignment -= removed
@@ -231,10 +231,8 @@
       }
       val id_edits =
         doc_edits map {
-          case (name, edits) =>
-            val ids =
-              edits.map(_.map { case (c1, c2) => (c1.map(id_command), c2.map(id_command)) })
-            (name, ids)
+          case (name, edit) =>
+            (name, edit.map({ case (c1, c2) => (c1.map(id_command), c2.map(id_command)) }))
         }
 
       global_state.change(_.define_version(version, former_assignment))
@@ -331,11 +329,12 @@
 
         case Init_Node(name, header, text) if prover.isDefined =>
           // FIXME compare with existing node
-          handle_edits(name, header, List(None, Some(List(Text.Edit.insert(0, text)))))
+          handle_edits(name, header,
+            List(Document.Node.Remove(), Document.Node.Edits(List(Text.Edit.insert(0, text)))))
           reply(())
 
         case Edit_Node(name, header, text_edits) if prover.isDefined =>
-          handle_edits(name, header, List(Some(text_edits)))
+          handle_edits(name, header, List(Document.Node.Edits(text_edits)))
           reply(())
 
         case change: Change_Node if prover.isDefined =>

--- a/src/Pure/Thy/thy_syntax.scala	Thu Aug 11 13:24:49 2011 +0200
+++ b/src/Pure/Thy/thy_syntax.scala	Thu Aug 11 18:01:28 2011 +0200
@@ -195,11 +195,11 @@
       var nodes = previous.nodes
 
       edits foreach {
-        case (name, None) =>
-          doc_edits += (name -> None)
+        case (name, Document.Node.Remove()) =>
+          doc_edits += (name -> Document.Node.Remove())
           nodes -= name
 
-        case (name, Some(text_edits)) =>
+        case (name, Document.Node.Edits(text_edits)) =>
           val node = nodes(name)
           val commands0 = node.commands
           val commands1 = edit_text(text_edits, commands0)
@@ -212,7 +212,7 @@
             removed_commands.reverse.map(cmd => (commands0.prev(cmd), None)) :::
             inserted_commands.map(cmd => (commands2.prev(cmd), Some(cmd)))
 
-          doc_edits += (name -> Some(cmd_edits))
+          doc_edits += (name -> Document.Node.Edits(cmd_edits))
 
           val (new_headers, new_header) = node_header(name, node)
           header_edits ++= new_headers