concentrate protocol message formats in Isar_Document;

--- a/src/Pure/Isar/toplevel.scala	Fri Aug 20 11:47:33 2010 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,33 +0,0 @@
-/*  Title:      Pure/Isar/toplevel.scala
-    Author:     Makarius
-
-Isabelle/Isar toplevel transactions.
-*/
-
-package isabelle
-
-
-object Toplevel
-{
-  sealed abstract class Status
-  case class Forked(forks: Int) extends Status
-  case object Unprocessed extends Status
-  case object Finished extends Status
-  case object Failed extends Status
-
-  def command_status(markup: XML.Body): Status =
-  {
-    val forks = (0 /: markup) {
-      case (i, XML.Elem(Markup(Markup.FORKED, _), _)) => i + 1
-      case (i, XML.Elem(Markup(Markup.JOINED, _), _)) => i - 1
-      case (i, _) => i
-    }
-    if (forks != 0) Forked(forks)
-    else if (markup.exists { case XML.Elem(Markup(Markup.FAILED, _), _) => true case _ => false })
-      Failed
-    else if (markup.exists { case XML.Elem(Markup(Markup.FINISHED, _), _) => true case _ => false })
-      Finished
-    else Unprocessed
-  }
-}
-

--- a/src/Pure/PIDE/isar_document.ML	Fri Aug 20 11:47:33 2010 +0200
+++ b/src/Pure/PIDE/isar_document.ML	Fri Aug 20 11:57:43 2010 +0200
@@ -1,7 +1,7 @@
 (*  Title:      Pure/PIDE/isar_document.ML
     Author:     Makarius
 
-Protocol commands for interactive Isar documents.
+Protocol message formats for interactive Isar documents.
 *)
 
 structure Isar_Document: sig end =

--- a/src/Pure/PIDE/isar_document.scala	Fri Aug 20 11:47:33 2010 +0200
+++ b/src/Pure/PIDE/isar_document.scala	Fri Aug 20 11:57:43 2010 +0200
@@ -1,7 +1,7 @@
 /*  Title:      Pure/PIDE/isar_document.scala
     Author:     Makarius
 
-Protocol commands for interactive Isar documents.
+Protocol message formats for interactive Isar documents.
 */
 
 package isabelle
@@ -9,7 +9,7 @@
 
 object Isar_Document
 {
-  /* protocol messages */
+  /* document editing */
 
   object Assign {
     def unapply(msg: XML.Tree)
@@ -32,6 +32,30 @@
         case _ => None
       }
   }
+
+
+  /* toplevel transactions */
+
+  sealed abstract class Status
+  case class Forked(forks: Int) extends Status
+  case object Unprocessed extends Status
+  case object Finished extends Status
+  case object Failed extends Status
+
+  def command_status(markup: XML.Body): Status =
+  {
+    val forks = (0 /: markup) {
+      case (i, XML.Elem(Markup(Markup.FORKED, _), _)) => i + 1
+      case (i, XML.Elem(Markup(Markup.JOINED, _), _)) => i - 1
+      case (i, _) => i
+    }
+    if (forks != 0) Forked(forks)
+    else if (markup.exists { case XML.Elem(Markup(Markup.FAILED, _), _) => true case _ => false })
+      Failed
+    else if (markup.exists { case XML.Elem(Markup(Markup.FINISHED, _), _) => true case _ => false })
+      Finished
+    else Unprocessed
+  }
 }
 
 

--- a/src/Pure/build-jars	Fri Aug 20 11:47:33 2010 +0200
+++ b/src/Pure/build-jars	Fri Aug 20 11:57:43 2010 +0200
@@ -37,7 +37,6 @@
   Isar/keyword.scala
   Isar/outer_syntax.scala
   Isar/parse.scala
-  Isar/toplevel.scala
   Isar/token.scala
   PIDE/command.scala
   PIDE/document.scala

--- a/src/Tools/jEdit/src/jedit/document_view.scala	Fri Aug 20 11:47:33 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/document_view.scala	Fri Aug 20 11:57:43 2010 +0200
@@ -29,11 +29,11 @@
     val state = snapshot.state(command)
     if (snapshot.is_outdated) new Color(240, 240, 240)
     else
-      Toplevel.command_status(state.status) match {
-        case Toplevel.Forked(i) if i > 0 => new Color(255, 228, 225)
-        case Toplevel.Finished => new Color(234, 248, 255)
-        case Toplevel.Failed => new Color(255, 193, 193)
-        case Toplevel.Unprocessed => new Color(255, 228, 225)
+      Isar_Document.command_status(state.status) match {
+        case Isar_Document.Forked(i) if i > 0 => new Color(255, 228, 225)
+        case Isar_Document.Finished => new Color(234, 248, 255)
+        case Isar_Document.Failed => new Color(255, 193, 193)
+        case Isar_Document.Unprocessed => new Color(255, 228, 225)
         case _ => Color.red
       }
   }