# HG changeset patch
# User wenzelm
# Date 1606402749 -3600
# Node ID ade53fbc6f037e1cbe2a0a62e3fb904be3d843ca
# Parent  79f5e843e5ecf1ee36ff14daa98ac186e0f2f5ca
clarified signature: initial markup is_empty, not init_markup;

diff -r 79f5e843e5ec -r ade53fbc6f03 src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Thu Nov 26 15:49:27 2020 +0100
+++ b/src/Pure/PIDE/command.scala	Thu Nov 26 15:59:09 2020 +0100
@@ -418,7 +418,7 @@
     span: Command_Span.Span): Command =
   {
     val (source, span1) = span.compact_source
-    new Command(id, node_name, blobs_info, span1, source, Results.empty, Markup_Tree.empty)
+    new Command(id, node_name, blobs_info, span1, source, Results.empty, Markups.empty)
   }
 
   val empty: Command =
@@ -430,16 +430,17 @@
     id: Document_ID.Command = Document_ID.none,
     node_name: Document.Node.Name = Document.Node.Name.empty,
     results: Results = Results.empty,
-    markup: Markup_Tree = Markup_Tree.empty): Command =
+    markups: Markups = Markups.empty): Command =
   {
     val (source1, span1) = Command_Span.unparsed(source, theory).compact_source
-    new Command(id, node_name, no_blobs, span1, source1, results, markup)
+    new Command(id, node_name, no_blobs, span1, source1, results, markups)
   }
 
   def text(source: String): Command = unparsed(source)
 
   def rich_text(id: Document_ID.Command, results: Results, body: XML.Body): Command =
-    unparsed(XML.content(body), id = id, results = results, markup = Markup_Tree.from_XML(body))
+    unparsed(XML.content(body), id = id, results = results,
+      markups = Markups.init(Markup_Tree.from_XML(body)))
 
 
   /* perspective */
@@ -554,7 +555,7 @@
     val span: Command_Span.Span,
     val source: String,
     val init_results: Command.Results,
-    val init_markup: Markup_Tree)
+    val init_markups: Command.Markups)
 {
   override def toString: String = id + "/" + span.kind.toString
 
@@ -669,7 +670,7 @@
   /* accumulated results */
 
   val init_state: Command.State =
-    Command.State(this, results = init_results, markups = Command.Markups.init(init_markup))
+    Command.State(this, results = init_results, markups = init_markups)
 
   val empty_state: Command.State = Command.State(this)
 }
diff -r 79f5e843e5ec -r ade53fbc6f03 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Thu Nov 26 15:49:27 2020 +0100
+++ b/src/Pure/PIDE/document.scala	Thu Nov 26 15:59:09 2020 +0100
@@ -822,7 +822,7 @@
           val node_name = command.node_name
           val command1 =
             Command.unparsed(command.source, theory = true, id = command.id, node_name = node_name,
-              results = st.results, markup = st.markup(Command.Markup_Index.markup))
+              results = st.results, markups = st.markups)
           val state1 = copy(theories = theories - command1.id)
           val snapshot = state1.snapshot(name = node_name).command_snippet(command1)
           (snapshot, state1)