# HG changeset patch
# User wenzelm
# Date 1281818723 -7200
# Node ID 49f1f657adc26df8e2bba4c3facd93bda23b00bd
# Parent  224efb14f258601f29b9ffcb9aa0640b2eb9b8cb
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
added convenient Markup.Int/Long objects (Scala);
simplified "assign" message format -- explicit version id;
misc tuning and simplification;

diff -r 224efb14f258 -r 49f1f657adc2 src/Pure/General/markup.ML
--- a/src/Pure/General/markup.ML	Sat Aug 14 21:25:20 2010 +0200
+++ b/src/Pure/General/markup.ML	Sat Aug 14 22:45:23 2010 +0200
@@ -6,6 +6,8 @@
 
 signature MARKUP =
 sig
+  val parse_int: string -> int
+  val print_int: int -> string
   type T = string * Properties.T
   val none: T
   val is_none: T -> bool
@@ -109,8 +111,10 @@
   val failedN: string val failed: T
   val finishedN: string val finished: T
   val disposedN: string val disposed: T
-  val assignN: string val assign: T
-  val editN: string val edit: string -> string -> T
+  val versionN: string
+  val execN: string
+  val assignN: string val assign: int -> T
+  val editN: string val edit: int -> int -> T
   val pidN: string
   val promptN: string val prompt: T
   val readyN: string val ready: T
@@ -127,6 +131,16 @@
 
 (** markup elements **)
 
+(* integers *)
+
+fun parse_int s =
+  (case Int.fromString s of
+    SOME i => i
+  | NONE => raise Fail ("Bad integer: " ^ quote s));
+
+val print_int = signed_string_of_int;
+
+
 (* basic markup *)
 
 type T = string * Properties.T;
@@ -142,7 +156,7 @@
 
 fun markup_elem elem = (elem, (elem, []): T);
 fun markup_string elem prop = (elem, fn s => (elem, [(prop, s)]): T);
-fun markup_int elem prop = (elem, fn i => (elem, [(prop, Int.toString i)]): T);
+fun markup_int elem prop = (elem, fn i => (elem, [(prop, print_int i)]): T);
 
 
 (* name *)
@@ -315,10 +329,12 @@
 
 (* interactive documents *)
 
-val (assignN, assign) = markup_elem "assign";
+val versionN = "version";
+val execN = "exec";
+val (assignN, assign) = markup_int "assign" versionN;
 
 val editN = "edit";
-fun edit id state_id : T = (editN, [(idN, id), (stateN, state_id)]);
+fun edit cmd_id exec_id : T = (editN, [(idN, print_int cmd_id), (execN, print_int exec_id)]);
 
 
 (* messages *)
diff -r 224efb14f258 -r 49f1f657adc2 src/Pure/General/markup.scala
--- a/src/Pure/General/markup.scala	Sat Aug 14 21:25:20 2010 +0200
+++ b/src/Pure/General/markup.scala	Sat Aug 14 22:45:23 2010 +0200
@@ -9,34 +9,41 @@
 
 object Markup
 {
+  /* integers */
+
+  object Int {
+    def apply(i: scala.Int): String = i.toString
+    def unapply(s: String): Option[scala.Int] =
+      try { Some(Integer.parseInt(s)) }
+      catch { case _: NumberFormatException => None }
+  }
+
+  object Long {
+    def apply(i: scala.Long): String = i.toString
+    def unapply(s: String): Option[scala.Long] =
+      try { Some(java.lang.Long.parseLong(s)) }
+      catch { case _: NumberFormatException => None }
+  }
+
+
   /* property values */
 
   def get_string(name: String, props: List[(String, String)]): Option[String] =
     props.find(p => p._1 == name).map(_._2)
 
-
-  def parse_long(s: String): Option[Long] =
-    try { Some(java.lang.Long.parseLong(s)) }
-    catch { case _: NumberFormatException => None }
-
-  def get_long(name: String, props: List[(String, String)]): Option[Long] =
+  def get_long(name: String, props: List[(String, String)]): Option[scala.Long] =
   {
     get_string(name, props) match {
       case None => None
-      case Some(value) => parse_long(value)
+      case Some(Long(i)) => Some(i)
     }
   }
 
-
-  def parse_int(s: String): Option[Int] =
-    try { Some(Integer.parseInt(s)) }
-    catch { case _: NumberFormatException => None }
-
-  def get_int(name: String, props: List[(String, String)]): Option[Int] =
+  def get_int(name: String, props: List[(String, String)]): Option[scala.Int] =
   {
     get_string(name, props) match {
       case None => None
-      case Some(value) => parse_int(value)
+      case Some(Int(i)) => Some(i)
     }
   }
 
@@ -197,7 +204,9 @@
 
   /* interactive documents */
 
-  val Assign = Markup("assign", Nil)
+  val VERSION = "version"
+  val EXEC = "exec"
+  val ASSIGN = "assign"
   val EDIT = "edit"
 
 
diff -r 224efb14f258 -r 49f1f657adc2 src/Pure/General/pretty.scala
--- a/src/Pure/General/pretty.scala	Sat Aug 14 21:25:20 2010 +0200
+++ b/src/Pure/General/pretty.scala	Sat Aug 14 22:45:23 2010 +0200
@@ -16,29 +16,26 @@
 
   object Block
   {
-    def apply(indent: Int, body: List[XML.Tree]): XML.Tree =
-      XML.Elem(Markup(Markup.BLOCK, List((Markup.INDENT, indent.toString))), body)
+    def apply(i: Int, body: List[XML.Tree]): XML.Tree =
+      XML.Elem(Markup(Markup.BLOCK, List((Markup.INDENT, Markup.Int(i)))), body)
 
     def unapply(tree: XML.Tree): Option[(Int, List[XML.Tree])] =
       tree match {
-        case XML.Elem(Markup(Markup.BLOCK, List((Markup.INDENT, indent))), body) =>
-          Markup.parse_int(indent) match {
-            case Some(i) => Some((i, body))
-            case None => None
-          }
+        case XML.Elem(
+          Markup(Markup.BLOCK, List((Markup.INDENT, Markup.Int(i)))), body) => Some((i, body))
         case _ => None
       }
   }
 
   object Break
   {
-    def apply(width: Int): XML.Tree =
-      XML.Elem(Markup(Markup.BREAK, List((Markup.WIDTH, width.toString))),
-        List(XML.Text(Symbol.spaces(width))))
+    def apply(w: Int): XML.Tree =
+      XML.Elem(
+        Markup(Markup.BREAK, List((Markup.WIDTH, Markup.Int(w)))), List(XML.Text(Symbol.spaces(w))))
 
     def unapply(tree: XML.Tree): Option[Int] =
       tree match {
-        case XML.Elem(Markup(Markup.BREAK, List((Markup.WIDTH, width))), _) => Markup.parse_int(width)
+        case XML.Elem(Markup(Markup.BREAK, List((Markup.WIDTH, Markup.Int(w)))), _) => Some(w)
         case _ => None
       }
   }
diff -r 224efb14f258 -r 49f1f657adc2 src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Sat Aug 14 21:25:20 2010 +0200
+++ b/src/Pure/PIDE/document.ML	Sat Aug 14 22:45:23 2010 +0200
@@ -29,12 +29,8 @@
 
 val no_id = 0;
 
-fun parse_id s =
-  (case Int.fromString s of
-    SOME i => i
-  | NONE => raise Fail ("Bad id: " ^ quote s));
-
-val print_id = signed_string_of_int;
+val parse_id = Markup.parse_int;
+val print_id = Markup.print_int;
 
 
 (* edits *)
diff -r 224efb14f258 -r 49f1f657adc2 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Sat Aug 14 21:25:20 2010 +0200
+++ b/src/Pure/PIDE/document.scala	Sat Aug 14 22:45:23 2010 +0200
@@ -16,15 +16,18 @@
   /* formal identifiers */
 
   type ID = Long
+
+  object ID {
+    def apply(id: ID): String = Markup.Long.apply(id)
+    def unapply(s: String): Option[ID] = Markup.Long.unapply(s)
+  }
+
   type Version_ID = ID
   type Command_ID = ID
   type Exec_ID = ID
 
   val NO_ID: ID = 0
 
-  def parse_id(s: String): ID = java.lang.Long.parseLong(s)
-  def print_id(id: ID): String = id.toString
-
 
 
   /** named document nodes **/
diff -r 224efb14f258 -r 49f1f657adc2 src/Pure/System/isar_document.ML
--- a/src/Pure/System/isar_document.ML	Sat Aug 14 21:25:20 2010 +0200
+++ b/src/Pure/System/isar_document.ML	Sat Aug 14 22:45:23 2010 +0200
@@ -240,11 +240,9 @@
   in (exec_id', (id, exec_id') :: updates) end;
 
 fun updates_status new_id updates =
-  implode (map (fn (id, exec_id) =>
-      Markup.markup (Markup.edit (Document.print_id id) (Document.print_id exec_id)) "") updates)
-  |> Markup.markup Markup.assign
-  |> Position.setmp_thread_data (Position.id_only (Document.print_id new_id)) Output.status;
-  (*FIXME avoid setmp -- direct message argument*)
+  implode (map (fn (id, exec_id) => Markup.markup (Markup.edit id exec_id) "") updates)
+  |> Markup.markup (Markup.assign new_id)
+  |> Output.status;
 
 in
 
diff -r 224efb14f258 -r 49f1f657adc2 src/Pure/System/isar_document.scala
--- a/src/Pure/System/isar_document.scala	Sat Aug 14 21:25:20 2010 +0200
+++ b/src/Pure/System/isar_document.scala	Sat Aug 14 22:45:23 2010 +0200
@@ -12,11 +12,12 @@
   /* protocol messages */
 
   object Assign {
-    def unapply(msg: XML.Tree): Option[List[(Document.Command_ID, Document.Exec_ID)]] =
+    def unapply(msg: XML.Tree)
+        : Option[(Document.Version_ID, List[(Document.Command_ID, Document.Exec_ID)])] =
       msg match {
-        case XML.Elem(Markup.Assign, edits) =>
+        case XML.Elem(Markup(Markup.ASSIGN, List((Markup.VERSION, Document.ID(id)))), edits) =>
           val id_edits = edits.map(Edit.unapply)
-          if (id_edits.forall(_.isDefined)) Some(id_edits.map(_.get))
+          if (id_edits.forall(_.isDefined)) Some((id, id_edits.map(_.get)))
           else None
         case _ => None
       }
@@ -25,11 +26,9 @@
   object Edit {
     def unapply(msg: XML.Tree): Option[(Document.Command_ID, Document.Exec_ID)] =
       msg match {
-        case XML.Elem(Markup(Markup.EDIT, List((Markup.ID, cmd_id), (Markup.STATE, state_id))), Nil) =>
-          (Markup.parse_long(cmd_id), Markup.parse_long(state_id)) match {
-            case (Some(i), Some(j)) => Some((i, j))
-            case _ => None
-          }
+        case XML.Elem(
+          Markup(Markup.EDIT,
+            List((Markup.ID, Document.ID(i)), (Markup.EXEC, Document.ID(j)))), Nil) => Some((i, j))
         case _ => None
       }
   }
@@ -44,7 +43,7 @@
   /* commands */
 
   def define_command(id: Document.Command_ID, text: String): Unit =
-    input("Isar_Document.define_command", Document.print_id(id), text)
+    input("Isar_Document.define_command", Document.ID(id), text)
 
 
   /* documents */
@@ -62,6 +61,6 @@
               XML_Data.make_pair(make_id1)(XML_Data.make_option(XML_Data.make_long))))))(edits)
 
     input("Isar_Document.edit_document",
-      Document.print_id(old_id), Document.print_id(new_id), YXML.string_of_body(arg))
+      Document.ID(old_id), Document.ID(new_id), YXML.string_of_body(arg))
   }
 }
diff -r 224efb14f258 -r 49f1f657adc2 src/Pure/System/session.scala
--- a/src/Pure/System/session.scala	Sat Aug 14 21:25:20 2010 +0200
+++ b/src/Pure/System/session.scala	Sat Aug 14 22:45:23 2010 +0200
@@ -132,27 +132,19 @@
       raw_results.event(result)
 
       Position.get_id(result.properties) match {
-        case Some(target_id) =>
+        case Some(state_id) =>
           try {
-            val (st, state) = global_state.accumulate(target_id, result.message)
+            val (st, state) = global_state.accumulate(state_id, result.message)
             global_state = state
-            indicate_command_change(st.command)  // FIXME forward Command.State (!?)
+            indicate_command_change(st.command)
           }
-          catch {
-            case _: Document.State.Fail =>
-              if (result.is_status) {
-                result.body match {
-                  case List(Isar_Document.Assign(edits)) =>
-                    try { change_state(_.assign(target_id, edits)) }
-                    catch { case _: Document.State.Fail => bad_result(result) }
-                  case _ => bad_result(result)
-                }
-              }
-              else bad_result(result)
-          }
+          catch { case _: Document.State.Fail => bad_result(result) }
         case None =>
           if (result.is_status) {
             result.body match {
+              case List(Isar_Document.Assign(doc_id, edits)) =>
+                try { change_state(_.assign(doc_id, edits)) }
+                catch { case _: Document.State.Fail => bad_result(result) }
               case List(Keyword.Command_Decl(name, kind)) => syntax += (name, kind)
               case List(Keyword.Keyword_Decl(name)) => syntax += name
               case _ => if (!result.is_ready) bad_result(result)
diff -r 224efb14f258 -r 49f1f657adc2 src/Tools/jEdit/src/jedit/isabelle_sidekick.scala
--- a/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala	Sat Aug 14 21:25:20 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala	Sat Aug 14 22:45:23 2010 +0200
@@ -139,7 +139,7 @@
               override def getIcon: Icon = null
               override def getShortString: String = content
               override def getLongString: String = node.info.toString
-              override def getName: String = Document.print_id(id)
+              override def getName: String = Markup.Long(id)
               override def setName(name: String) = ()
               override def setStart(start: Position) = ()
               override def getStart: Position = command_start + node.start