some support for inital command markup;
tuned signature;

--- a/src/Pure/General/pretty.scala	Tue Sep 18 11:49:23 2012 +0200
+++ b/src/Pure/General/pretty.scala	Tue Sep 18 13:18:45 2012 +0200
@@ -146,7 +146,7 @@
 
   def string_of(input: XML.Body, margin: Int = margin_default,
       metric: String => Double = metric_default): String =
-    formatted(input, margin, metric).iterator.flatMap(XML.content).mkString
+    XML.content(formatted(input, margin, metric)).mkString
 
 
   /* unformatted output */
@@ -164,6 +164,5 @@
     input.flatMap(standard_format).flatMap(fmt)
   }
 
-  def str_of(input: XML.Body): String =
-    unformatted(input).iterator.flatMap(XML.content).mkString
+  def str_of(input: XML.Body): String = XML.content(unformatted(input)).mkString
 }

--- a/src/Pure/PIDE/blob.scala	Tue Sep 18 11:49:23 2012 +0200
+++ b/src/Pure/PIDE/blob.scala	Tue Sep 18 13:18:45 2012 +0200
@@ -24,5 +24,5 @@
   def decode(i: Text.Offset): Text.Offset = symbol_index.decode(i)
   def decode(r: Text.Range): Text.Range = symbol_index.decode(r)
 
-  val empty_state: Blob.State = Blob.State(this)
+  val init_state: Blob.State = Blob.State(this)
 }

--- a/src/Pure/PIDE/command.scala	Tue Sep 18 11:49:23 2012 +0200
+++ b/src/Pure/PIDE/command.scala	Tue Sep 18 13:18:45 2012 +0200
@@ -79,7 +79,8 @@
 
   type Span = List[Token]
 
-  def apply(id: Document.Command_ID, node_name: Document.Node.Name, span: Span): Command =
+  def apply(id: Document.Command_ID, node_name: Document.Node.Name,
+    span: Span, markup: Markup_Tree): Command =
   {
     val source: String =
       span match {
@@ -96,13 +97,22 @@
       i += n
     }
 
-    new Command(id, node_name, span1.toList, source)
+    new Command(id, node_name, span1.toList, source, markup)
   }
 
-  def unparsed(source: String): Command =
-    Command(Document.no_id, Document.Node.Name.empty, List(Token(Token.Kind.UNPARSED, source)))
+  val empty = Command(Document.no_id, Document.Node.Name.empty, Nil, Markup_Tree.empty)
+
+  def unparsed(id: Document.Command_ID, source: String, markup: Markup_Tree): Command =
+    Command(id, Document.Node.Name.empty, List(Token(Token.Kind.UNPARSED, source)), markup)
+
+  def unparsed(source: String): Command = unparsed(Document.no_id, source, Markup_Tree.empty)
 
-  val empty = Command(Document.no_id, Document.Node.Name.empty, Nil)
+  def rich_text(id: Document.Command_ID, body: XML.Body): Command =
+  {
+    val text = XML.content(body).mkString
+    val markup = Markup_Tree.empty  // FIXME
+    unparsed(id, text, markup)
+  }
 
 
   /* perspective */
@@ -131,7 +141,8 @@
     val id: Document.Command_ID,
     val node_name: Document.Node.Name,
     val span: Command.Span,
-    val source: String)
+    val source: String,
+    val init_markup: Markup_Tree)
 {
   /* classification */
 
@@ -167,5 +178,5 @@
 
   /* accumulated results */
 
-  val empty_state: Command.State = Command.State(this)
+  val init_state: Command.State = Command.State(this, markup = init_markup)
 }

--- a/src/Pure/PIDE/document.scala	Tue Sep 18 11:49:23 2012 +0200
+++ b/src/Pure/PIDE/document.scala	Tue Sep 18 13:18:45 2012 +0200
@@ -350,7 +350,7 @@
     def define_command(command: Command): State =
     {
       val id = command.id
-      copy(commands = commands + (id -> command.empty_state))
+      copy(commands = commands + (id -> command.init_state))
     }
 
     def defined_command(id: Command_ID): Boolean = commands.isDefinedAt(id)
@@ -474,7 +474,7 @@
       catch {
         case _: State.Fail =>
           try { the_command_state(command.id) }
-          catch { case _: State.Fail => command.empty_state }
+          catch { case _: State.Fail => command.init_state }
       }
     }
 

--- a/src/Pure/Thy/thy_syntax.scala	Tue Sep 18 11:49:23 2012 +0200
+++ b/src/Pure/Thy/thy_syntax.scala	Tue Sep 18 13:18:45 2012 +0200
@@ -68,7 +68,7 @@
       /* result structure */
 
       val spans = parse_spans(syntax.scan(text))
-      spans.foreach(span => add(Command(Document.no_id, node_name, span)))
+      spans.foreach(span => add(Command(Document.no_id, node_name, span, Markup_Tree.empty)))
       result()
     }
   }
@@ -226,7 +226,7 @@
         commands
       case cmd :: _ =>
         val hook = commands.prev(cmd)
-        val inserted = spans2.map(span => Command(Document.new_id(), name, span))
+        val inserted = spans2.map(span => Command(Document.new_id(), name, span, Markup_Tree.empty))
         (commands /: cmds2)(_ - _).append_after(hook, inserted)
     }
   }

--- a/src/Tools/jEdit/src/output2_dockable.scala	Tue Sep 18 11:49:23 2012 +0200
+++ b/src/Tools/jEdit/src/output2_dockable.scala	Tue Sep 18 13:18:45 2012 +0200
@@ -31,7 +31,7 @@
   private var zoom_factor = 100
   private var show_tracing = false
   private var do_update = true
-  private var current_state = Command.empty.empty_state
+  private var current_state = Command.empty.init_state
   private var current_body: XML.Body = Nil
 
 
@@ -60,9 +60,9 @@
             val snapshot = doc_view.model.snapshot()
             snapshot.node.command_at(doc_view.text_area.getCaretPosition).map(_._1) match {
               case Some(cmd) => snapshot.state.command_state(snapshot.version, cmd)
-              case None => Command.empty.empty_state
+              case None => Command.empty.init_state
             }
-          case None => Command.empty.empty_state
+          case None => Command.empty.init_state
         }
       }
       else current_state

--- a/src/Tools/jEdit/src/output_dockable.scala	Tue Sep 18 11:49:23 2012 +0200
+++ b/src/Tools/jEdit/src/output_dockable.scala	Tue Sep 18 13:18:45 2012 +0200
@@ -31,7 +31,7 @@
   private var zoom_factor = 100
   private var show_tracing = false
   private var do_update = true
-  private var current_state = Command.empty.empty_state
+  private var current_state = Command.empty.init_state
   private var current_body: XML.Body = Nil
 
 
@@ -91,9 +91,9 @@
             val snapshot = doc_view.model.snapshot()
             snapshot.node.command_at(doc_view.text_area.getCaretPosition).map(_._1) match {
               case Some(cmd) => snapshot.state.command_state(snapshot.version, cmd)
-              case None => Command.empty.empty_state
+              case None => Command.empty.init_state
             }
-          case None => Command.empty.empty_state
+          case None => Command.empty.init_state
         }
       }
       else current_state

--- a/src/Tools/jEdit/src/pretty_text_area.scala	Tue Sep 18 11:49:23 2012 +0200
+++ b/src/Tools/jEdit/src/pretty_text_area.scala	Tue Sep 18 13:18:45 2012 +0200
@@ -22,15 +22,11 @@
 {
   def document_state(formatted_body: XML.Body): Document.State =
   {
-    val text = formatted_body.iterator.flatMap(XML.content).mkString
-    val markup: List[XML.Elem] = Nil  // FIXME
-
-    val command = Command.unparsed(text)
+    val command = Command.rich_text(Document.new_id(), formatted_body)
     val node_name = command.node_name
-    val exec_id = Document.new_id()
 
     val edits: List[Document.Edit_Text] =
-      List(node_name -> Document.Node.Edits(List(Text.Edit.insert(0, text))))
+      List(node_name -> Document.Node.Edits(List(Text.Edit.insert(0, command.source))))
 
     val state0 = Document.State.init.define_command(command)
     val version0 = state0.history.tip.version.get_finished
@@ -41,7 +37,7 @@
     val state1 =
       state0.continue_history(Future.value(version0), edits, Future.value(version1))._2
         .define_version(version1, state0.the_assignment(version0))
-        .assign(version1.id, List(command.id -> Some(exec_id)))._2
+        .assign(version1.id, List(command.id -> Some(Document.new_id())))._2
 
     state1
   }