# HG changeset patch
# User wenzelm
# Date 1396464104 -7200
# Node ID 0605d90be6fc0aff39d812754bddf8dbd6304d0b
# Parent  fadb0fef09d789c32922058cf2a87e0ca997e4d2
tuned signature -- more explicit iterator terminology;

diff -r fadb0fef09d7 -r 0605d90be6fc src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Wed Apr 02 20:22:12 2014 +0200
+++ b/src/Pure/PIDE/document.scala	Wed Apr 02 20:41:44 2014 +0200
@@ -212,7 +212,7 @@
 
       private def full_range: Text.Range = full_index._2
 
-      def range(i: Text.Offset = 0): Iterator[(Command, Text.Offset)] =
+      def iterator(i: Text.Offset = 0): Iterator[(Command, Text.Offset)] =
       {
         if (!commands.isEmpty && full_range.contains(i)) {
           val (cmd0, start0) = full_index._1(i / Commands.block_size)
@@ -253,11 +253,11 @@
       if (new_commands eq _commands.commands) this
       else new Node(get_blob, header, perspective, Node.Commands(new_commands))
 
-    def command_range(i: Text.Offset = 0): Iterator[(Command, Text.Offset)] =
-      _commands.range(i)
+    def command_iterator(i: Text.Offset = 0): Iterator[(Command, Text.Offset)] =
+      _commands.iterator(i)
 
-    def command_range(range: Text.Range): Iterator[(Command, Text.Offset)] =
-      command_range(range.start) takeWhile { case (_, start) => start < range.stop }
+    def command_iterator(range: Text.Range): Iterator[(Command, Text.Offset)] =
+      command_iterator(range.start) takeWhile { case (_, start) => start < range.stop }
 
     def command_start(cmd: Command): Option[Text.Offset] =
       Node.Commands.starts(commands.iterator).find(_._1 == cmd).map(_._2)
@@ -733,14 +733,14 @@
           status: Boolean = false): List[Text.Info[A]] =
         {
           val former_range = revert(range)
-          val (file_name, command_range_iterator) =
+          val (file_name, command_iterator) =
             load_commands match {
               case command :: _ => (node_name.node, Iterator((command, 0)))
-              case _ => ("", node.command_range(former_range))
+              case _ => ("", node.command_iterator(former_range))
             }
           val markup_index = Command.Markup_Index(status, file_name)
           (for {
-            (command, command_start) <- command_range_iterator
+            (command, command_start) <- command_iterator
             chunk <- command.chunks.get(file_name).iterator
             states = state.command_states(version, command)
             res = result(states)
diff -r fadb0fef09d7 -r 0605d90be6fc src/Pure/Thy/thy_syntax.scala
--- a/src/Pure/Thy/thy_syntax.scala	Wed Apr 02 20:22:12 2014 +0200
+++ b/src/Pure/Thy/thy_syntax.scala	Wed Apr 02 20:41:44 2014 +0200
@@ -141,9 +141,9 @@
       }
 
       val commands =
-        if (overlays.is_empty) node.command_range(perspective.range)
-        else node.command_range()
-      check_ranges(perspective.ranges, commands.toStream)
+        (if (overlays.is_empty) node.command_iterator(perspective.range)
+         else node.command_iterator()).toStream
+      check_ranges(perspective.ranges, commands)
       (Command.Perspective(visible.toList), Command.Perspective(visible_overlay.toList))
     }
   }
diff -r fadb0fef09d7 -r 0605d90be6fc src/Tools/jEdit/src/document_view.scala
--- a/src/Tools/jEdit/src/document_view.scala	Wed Apr 02 20:22:12 2014 +0200
+++ b/src/Tools/jEdit/src/document_view.scala	Wed Apr 02 20:41:44 2014 +0200
@@ -224,15 +224,15 @@
                     text_area.invalidateScreenLineRange(0, visible_lines)
                   else {
                     val visible_range = JEdit_Lib.visible_range(text_area).get
-                    val visible_cmds =
-                      snapshot.node.command_range(snapshot.revert(visible_range)).map(_._1)
-                    if (visible_cmds.exists(changed.commands)) {
+                    val visible_iterator =
+                      snapshot.node.command_iterator(snapshot.revert(visible_range)).map(_._1)
+                    if (visible_iterator.exists(changed.commands)) {
                       for {
                         line <- (0 until visible_lines).iterator
                         start = text_area.getScreenLineStartOffset(line) if start >= 0
                         end = text_area.getScreenLineEndOffset(line) if end >= 0
                         range = Text.Range(start, end)
-                        line_cmds = snapshot.node.command_range(snapshot.revert(range)).map(_._1)
+                        line_cmds = snapshot.node.command_iterator(snapshot.revert(range)).map(_._1)
                         if line_cmds.exists(changed.commands)
                       } text_area.invalidateScreenLineRange(line, line)
                     }
diff -r fadb0fef09d7 -r 0605d90be6fc src/Tools/jEdit/src/isabelle_sidekick.scala
--- a/src/Tools/jEdit/src/isabelle_sidekick.scala	Wed Apr 02 20:22:12 2014 +0200
+++ b/src/Tools/jEdit/src/isabelle_sidekick.scala	Wed Apr 02 20:41:44 2014 +0200
@@ -158,7 +158,7 @@
     opt_snapshot match {
       case Some(snapshot) =>
         val root = data.root
-        for ((command, command_start) <- snapshot.node.command_range() if !stopped) {
+        for ((command, command_start) <- snapshot.node.command_iterator() if !stopped) {
           val markup =
             snapshot.state.command_markup(
               snapshot.version, command, Command.Markup_Index.markup,
diff -r fadb0fef09d7 -r 0605d90be6fc src/Tools/jEdit/src/jedit_editor.scala
--- a/src/Tools/jEdit/src/jedit_editor.scala	Wed Apr 02 20:22:12 2014 +0200
+++ b/src/Tools/jEdit/src/jedit_editor.scala	Wed Apr 02 20:41:44 2014 +0200
@@ -74,9 +74,9 @@
         val node = snapshot.version.nodes(doc_view.model.node_name)
         val caret = snapshot.revert(text_area.getCaretPosition)
         if (caret < buffer.getLength) {
-          val caret_commands = node.command_range(caret)
-          if (caret_commands.hasNext) {
-            val (cmd0, _) = caret_commands.next
+          val caret_command_iterator = node.command_iterator(caret)
+          if (caret_command_iterator.hasNext) {
+            val (cmd0, _) = caret_command_iterator.next
             node.commands.reverse.iterator(cmd0).find(cmd => !cmd.is_ignored)
           }
           else None
@@ -154,11 +154,11 @@
         case None => None
         case Some((node, _)) =>
           val file_name = command.node_name.node
-          val sources =
+          val sources_iterator =
             node.commands.iterator.takeWhile(_ != command).map(_.source) ++
               (if (offset == 0) Iterator.empty
                else Iterator.single(command.source(Text.Range(0, command.decode(offset)))))
-          val (line, column) = ((1, 1) /: sources)(Symbol.advance_line_column)
+          val (line, column) = ((1, 1) /: sources_iterator)(Symbol.advance_line_column)
           Some(new Hyperlink { def follow(view: View) { goto_file(view, file_name, line, column) } })
       }
     }
diff -r fadb0fef09d7 -r 0605d90be6fc src/Tools/jEdit/src/rich_text_area.scala
--- a/src/Tools/jEdit/src/rich_text_area.scala	Wed Apr 02 20:22:12 2014 +0200
+++ b/src/Tools/jEdit/src/rich_text_area.scala	Wed Apr 02 20:41:44 2014 +0200
@@ -359,7 +359,7 @@
             r2 <- r1.try_restrict(chunk_range)
           } yield r2
 
-        val padded_markup =
+        val padded_markup_iterator =
           if (markup.isEmpty)
             Iterator(Text.Info(chunk_range, chunk_color))
           else
@@ -370,7 +370,7 @@
 
         var x1 = x + w
         gfx.setFont(chunk_font)
-        for (Text.Info(range, color) <- padded_markup if !range.is_singularity) {
+        for (Text.Info(range, color) <- padded_markup_iterator if !range.is_singularity) {
           val str = chunk_str.substring(range.start - chunk_offset, range.stop - chunk_offset)
           gfx.setColor(color)