src/Pure/PIDE/document.scala

           .assign(version1.id, Nil, List(command.id -> List(Document_ID.make())))._2
 
       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]
 
     def find_command(id: Document_ID.Generic): Option[(Node, Command)]

 
     def command_markup(version: Version, command: Command, index: Command.Markup_Index,
         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) {
         val markup_index = Command.Markup_Index.markup
         (for {

             }
             else other_node.commands.reverse.iterator.find(command => !command.is_ignored)
           }
           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 {
             (command, start) <-
               Document.Node.Commands.starts_pos(