# HG changeset patch
# User wenzelm
# Date 1334946584 -7200
# Node ID 645163d3b96401fd31e9c358a786fb2a95538db0
# Parent  3275758d274e00fa7cf63e228c8b20d86538afef
simplified internal actor protocol;

diff -r 3275758d274e -r 645163d3b964 src/Pure/System/session.scala
--- a/src/Pure/System/session.scala	Fri Apr 20 20:21:22 2012 +0200
+++ b/src/Pure/System/session.scala	Fri Apr 20 20:29:44 2012 +0200
@@ -87,7 +87,6 @@
 
   //{{{
   private case class Text_Edits(
-    name: Document.Node.Name,
     previous: Future[Document.Version],
     text_edits: List[Document.Edit_Text],
     version_result: Promise[Document.Version])
@@ -99,11 +98,11 @@
       receive {
         case Stop => finished = true; reply(())
 
-        case Text_Edits(name, previous, text_edits, version_result) =>
+        case Text_Edits(previous, text_edits, version_result) =>
           val prev = previous.get_finished
           val (doc_edits, version) = Thy_Syntax.text_edits(prover_syntax, prev, text_edits)
           version_result.fulfill(version)
-          sender ! Change_Node(name, doc_edits, prev, version)
+          sender ! Change(doc_edits, prev, version)
 
         case bad => System.err.println("change_parser: ignoring bad message " + bad)
       }
@@ -169,12 +168,8 @@
 
   private case class Start(timeout: Time, args: List[String])
   private case object Cancel_Execution
-  private case class Init_Node(name: Document.Node.Name,
-    header: Document.Node_Header, perspective: Text.Perspective, text: String)
-  private case class Edit_Node(name: Document.Node.Name,
-    header: Document.Node_Header, perspective: Text.Perspective, edits: List[Text.Edit])
-  private case class Change_Node(
-    name: Document.Node.Name,
+  private case class Edit(edits: List[Document.Edit_Text])
+  private case class Change(
     doc_edits: List[Document.Edit_Command],
     previous: Document.Version,
     version: Document.Version)
@@ -267,48 +262,13 @@
     }
 
 
-    /* incoming edits */
-
-    def handle_edits(name: Document.Node.Name,
-        header: Document.Node_Header, edits: List[Document.Node.Edit[Text.Edit, Text.Perspective]])
-    //{{{
-    {
-      val previous = global_state().history.tip.version
-
-      prover.get.discontinue_execution()
-
-      val text_edits = header_edit(name, header) :: edits.map(edit => (name, edit))
-      val version = Future.promise[Document.Version]
-      val change = global_state >>> (_.continue_history(previous, text_edits, version))
-
-      change_parser ! Text_Edits(name, previous, text_edits, version)
-    }
-    //}}}
-
-
-    /* exec state assignment */
-
-    def handle_assign(id: Document.Version_ID, assign: Document.Assign)
-    {
-      val cmds = global_state >>> (_.assign(id, assign))
-      delay_commands_changed.invoke(true, cmds)
-    }
-
-
-    /* removed versions */
-
-    def handle_removed(removed: List[Document.Version_ID]): Unit =
-      global_state >> (_.removed_versions(removed))
-
-
     /* resulting changes */
 
-    def handle_change(change: Change_Node)
+    def handle_change(change: Change)
     //{{{
     {
       val previous = change.previous
       val version = change.version
-      val name = change.name
       val doc_edits = change.doc_edits
 
       def id_command(command: Command)
@@ -355,7 +315,10 @@
         case Isabelle_Markup.Assign_Execs if output.is_protocol =>
           XML.content(output.body).mkString match {
             case Protocol.Assign(id, assign) =>
-              try { handle_assign(id, assign) }
+              try {
+                val cmds = global_state >>> (_.assign(id, assign))
+                delay_commands_changed.invoke(true, cmds)
+              }
               catch { case _: Document.State.Fail => bad_output(output) }
             case _ => bad_output(output)
           }
@@ -369,7 +332,9 @@
         case Isabelle_Markup.Removed_Versions if output.is_protocol =>
           XML.content(output.body).mkString match {
             case Protocol.Removed(removed) =>
-              try { handle_removed(removed) }
+              try {
+                global_state >> (_.removed_versions(removed))
+              }
               catch { case _: Document.State.Fail => bad_output(output) }
             case _ => bad_output(output)
           }
@@ -435,17 +400,14 @@
         case Cancel_Execution if prover.isDefined =>
           prover.get.cancel_execution()
 
-        case Init_Node(name, header, perspective, text) if prover.isDefined =>
-          // FIXME compare with existing node
-          handle_edits(name, header,
-            List(Document.Node.Clear(),
-              Document.Node.Edits(List(Text.Edit.insert(0, text))),
-              Document.Node.Perspective(perspective)))
-          reply(())
+        case Edit(edits) if prover.isDefined =>
+          prover.get.discontinue_execution()
 
-        case Edit_Node(name, header, perspective, text_edits) if prover.isDefined =>
-          handle_edits(name, header,
-            List(Document.Node.Edits(text_edits), Document.Node.Perspective(perspective)))
+          val previous = global_state().history.tip.version
+          val version = Future.promise[Document.Version]
+          val change = global_state >>> (_.continue_history(previous, edits, version))
+          change_parser ! Text_Edits(previous, edits, version)
+
           reply(())
 
         case Messages(msgs) =>
@@ -460,11 +422,11 @@
               all_messages.event(output)
           }
 
-        case change: Change_Node
+        case change: Change
         if prover.isDefined && global_state().is_assigned(change.previous) =>
           handle_change(change)
 
-        case bad if !bad.isInstanceOf[Change_Node] =>
+        case bad if !bad.isInstanceOf[Change] =>
           System.err.println("session_actor: ignoring bad message " + bad)
       }
     }
@@ -483,11 +445,23 @@
 
   def cancel_execution() { session_actor ! Cancel_Execution }
 
+  def edit(edits: List[Document.Edit_Text])
+  { session_actor !? Edit(edits) }
+
   def init_node(name: Document.Node.Name,
     header: Document.Node_Header, perspective: Text.Perspective, text: String)
-  { session_actor !? Init_Node(name, header, perspective, text) }
+  {
+    edit(List(header_edit(name, header),
+      name -> Document.Node.Clear(),    // FIXME diff wrt. existing node
+      name -> Document.Node.Edits(List(Text.Edit.insert(0, text))),
+      name -> Document.Node.Perspective(perspective)))
+  }
 
   def edit_node(name: Document.Node.Name,
-    header: Document.Node_Header, perspective: Text.Perspective, edits: List[Text.Edit])
-  { session_actor !? Edit_Node(name, header, perspective, edits) }
+    header: Document.Node_Header, perspective: Text.Perspective, text_edits: List[Text.Edit])
+  {
+    edit(List(header_edit(name, header),
+      name -> Document.Node.Edits(text_edits),
+      name -> Document.Node.Perspective(perspective)))
+  }
 }