# HG changeset patch
# User wenzelm
# Date 1606403319 -3600
# Node ID 3b804e0ffae9b65eec8e2bd2901ccf4c8da3dae0
# Parent  ade53fbc6f037e1cbe2a0a62e3fb904be3d843ca
clarified signature;

diff -r ade53fbc6f03 -r 3b804e0ffae9 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Thu Nov 26 15:59:09 2020 +0100
+++ b/src/Pure/PIDE/document.scala	Thu Nov 26 16:08:39 2020 +0100
@@ -572,7 +572,9 @@
       state1.snapshot(name = node_name)
     }
 
-    def markup_to_XML(range: Text.Range, elements: Markup.Elements): XML.Body
+    def xml_markup(
+      range: Text.Range = Text.Range.full,
+      elements: Markup.Elements = Markup.Elements.full): XML.Body
     def messages: List[(XML.Tree, Position.T)]
     def exports: List[Export.Entry]
     def exports_map: Map[String, Export.Entry]
@@ -1002,11 +1004,11 @@
         range: Text.Range, elements: Markup.Elements): Markup_Tree =
       Command.State.merge_markup(command_states(version, command), index, range, elements)
 
-    def markup_to_XML(
+    def xml_markup(
       version: Version,
       node_name: Node.Name,
-      range: Text.Range,
-      elements: Markup.Elements): XML.Body =
+      range: Text.Range = Text.Range.full,
+      elements: Markup.Elements = Markup.Elements.full): XML.Body =
     {
       val node = version.nodes(node_name)
       if (node_name.is_theory) {
@@ -1126,8 +1128,10 @@
           }
           else version.nodes.commands_loading(other_node_name).headOption
 
-        def markup_to_XML(range: Text.Range, elements: Markup.Elements): XML.Body =
-          state.markup_to_XML(version, node_name, range, elements)
+        def xml_markup(
+            range: Text.Range = Text.Range.full,
+            elements: Markup.Elements = Markup.Elements.full): XML.Body =
+          state.xml_markup(version, node_name, range = range, elements = elements)
 
         lazy val messages: List[(XML.Tree, Position.T)] =
           (for {
diff -r ade53fbc6f03 -r 3b804e0ffae9 src/Pure/Thy/presentation.scala
--- a/src/Pure/Thy/presentation.scala	Thu Nov 26 15:59:09 2020 +0100
+++ b/src/Pure/Thy/presentation.scala	Thu Nov 26 16:08:39 2020 +0100
@@ -437,7 +437,7 @@
     }
 
   def pide_document(snapshot: Document.Snapshot): XML.Body =
-    make_html(snapshot.markup_to_XML(Text.Range.full, document_elements))
+    make_html(snapshot.xml_markup(elements = document_elements))
 
 
 
diff -r ade53fbc6f03 -r 3b804e0ffae9 src/Pure/Tools/build_job.scala
--- a/src/Pure/Tools/build_job.scala	Thu Nov 26 15:59:09 2020 +0100
+++ b/src/Pure/Tools/build_job.scala	Thu Nov 26 16:08:39 2020 +0100
@@ -166,7 +166,7 @@
               val args = Protocol.Export.Args(theory_name = theory_name, name = name)
               export_consumer(session_name, args, Bytes(YXML.string_of_body(xml)))
             }
-            export(Export.MARKUP, snapshot.markup_to_XML(Text.Range.full, Markup.Elements.full))
+            export(Export.MARKUP, snapshot.xml_markup())
         }
 
       session.all_messages += Session.Consumer[Any]("build_session_output")
diff -r ade53fbc6f03 -r 3b804e0ffae9 src/Pure/Tools/dump.scala
--- a/src/Pure/Tools/dump.scala	Thu Nov 26 15:59:09 2020 +0100
+++ b/src/Pure/Tools/dump.scala	Thu Nov 26 16:08:39 2020 +0100
@@ -50,7 +50,7 @@
       Aspect("markup", "PIDE markup (YXML format)",
         { case args =>
             args.write(Path.explode(Export.MARKUP),
-              args.snapshot.markup_to_XML(Text.Range.full, Markup.Elements.full))
+              args.snapshot.xml_markup())
         }),
       Aspect("messages", "output messages (YXML format)",
         { case args =>
diff -r ade53fbc6f03 -r 3b804e0ffae9 src/Pure/Tools/update.scala
--- a/src/Pure/Tools/update.scala	Thu Nov 26 15:59:09 2020 +0100
+++ b/src/Pure/Tools/update.scala	Thu Nov 26 16:08:39 2020 +0100
@@ -45,8 +45,8 @@
         val snapshot = args.snapshot
         for ((node_name, node) <- snapshot.nodes) {
           val xml =
-            snapshot.state.markup_to_XML(snapshot.version, node_name,
-              Text.Range.full, Markup.Elements(Markup.UPDATE, Markup.LANGUAGE))
+            snapshot.state.xml_markup(snapshot.version, node_name,
+              elements = Markup.Elements(Markup.UPDATE, Markup.LANGUAGE))
 
           val source1 = Symbol.encode(XML.content(update_xml(xml)))
           if (source1 != Symbol.encode(node.source)) {