# HG changeset patch
# User wenzelm
# Date 1496949433 -7200
# Node ID f704c063e95d0f9efacb7a8ae220fa0aa05ba384
# Parent  98aaeff47795bd7dfa70a718df7dac66fdb27ae1
tuned signature;

diff -r 98aaeff47795 -r f704c063e95d src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Thu Jun 08 15:12:30 2017 +0200
+++ b/src/Pure/PIDE/document.scala	Thu Jun 08 21:17:13 2017 +0200
@@ -235,7 +235,7 @@
         (blocks.toArray, Text.Range(0, last_stop))
       }
 
-      def full_range: Text.Range = full_index._2
+      private def full_range: Text.Range = full_index._2
 
       def iterator(i: Text.Offset = 0): Iterator[(Command, Text.Offset)] =
       {
@@ -303,8 +303,6 @@
         new Node(get_blob, header, syntax, text_perspective, perspective,
           Node.Commands(new_commands))
 
-    def commands_range: Text.Range = _commands.full_range
-
     def command_iterator(i: Text.Offset = 0): Iterator[(Command, Text.Offset)] =
       _commands.iterator(i)
 
@@ -459,7 +457,7 @@
     def commands_loading_ranges(pred: Node.Name => Boolean): List[Text.Range]
     def current_command(other_node_name: Node.Name, offset: Text.Offset): Option[Command]
 
-    def markup_to_XML(restriction: Option[Text.Range], elements: Markup.Elements): XML.Body
+    def markup_to_XML(range: Text.Range, elements: Markup.Elements): XML.Body
 
     def find_command(id: Document_ID.Generic): Option[(Node, Command)]
     def find_command_position(id: Document_ID.Generic, offset: Symbol.Offset)
@@ -777,10 +775,9 @@
     def markup_to_XML(
       version: Version,
       node: Node,
-      restriction: Option[Text.Range],
+      range: Text.Range,
       elements: Markup.Elements): XML.Body =
     {
-      val range = restriction.getOrElse(node.commands_range)
       (for {
         command <- node.commands.iterator
         command_range <- command.range.try_restrict(range).iterator
@@ -858,8 +855,8 @@
           }
           else version.nodes.commands_loading(other_node_name).headOption
 
-        def markup_to_XML(restriction: Option[Text.Range], elements: Markup.Elements): XML.Body =
-          state.markup_to_XML(version, node, restriction, elements)
+        def markup_to_XML(range: Text.Range, elements: Markup.Elements): XML.Body =
+          state.markup_to_XML(version, node, range, elements)
 
 
         /* find command */
diff -r 98aaeff47795 -r f704c063e95d src/Pure/Thy/present.scala
--- a/src/Pure/Thy/present.scala	Thu Jun 08 15:12:30 2017 +0200
+++ b/src/Pure/Thy/present.scala	Thu Jun 08 21:17:13 2017 +0200
@@ -123,6 +123,6 @@
 
   def theory_document(snapshot: Document.Snapshot): XML.Body =
   {
-    make_html(snapshot.markup_to_XML(None, document_span_elements))
+    make_html(snapshot.markup_to_XML(Text.Range.full, document_span_elements))
   }
 }