tuned signature -- more explicit iterator terminology;
authorwenzelm
Wed Apr 02 20:41:44 2014 +0200 (2014-04-02)
changeset 563730605d90be6fc
parent 56372 fadb0fef09d7
child 56374 dfc7a46c2900
tuned signature -- more explicit iterator terminology;
src/Pure/PIDE/document.scala
src/Pure/Thy/thy_syntax.scala
src/Tools/jEdit/src/document_view.scala
src/Tools/jEdit/src/isabelle_sidekick.scala
src/Tools/jEdit/src/jedit_editor.scala
src/Tools/jEdit/src/rich_text_area.scala
     1.1 --- a/src/Pure/PIDE/document.scala	Wed Apr 02 20:22:12 2014 +0200
     1.2 +++ b/src/Pure/PIDE/document.scala	Wed Apr 02 20:41:44 2014 +0200
     1.3 @@ -212,7 +212,7 @@
     1.4  
     1.5        private def full_range: Text.Range = full_index._2
     1.6  
     1.7 -      def range(i: Text.Offset = 0): Iterator[(Command, Text.Offset)] =
     1.8 +      def iterator(i: Text.Offset = 0): Iterator[(Command, Text.Offset)] =
     1.9        {
    1.10          if (!commands.isEmpty && full_range.contains(i)) {
    1.11            val (cmd0, start0) = full_index._1(i / Commands.block_size)
    1.12 @@ -253,11 +253,11 @@
    1.13        if (new_commands eq _commands.commands) this
    1.14        else new Node(get_blob, header, perspective, Node.Commands(new_commands))
    1.15  
    1.16 -    def command_range(i: Text.Offset = 0): Iterator[(Command, Text.Offset)] =
    1.17 -      _commands.range(i)
    1.18 +    def command_iterator(i: Text.Offset = 0): Iterator[(Command, Text.Offset)] =
    1.19 +      _commands.iterator(i)
    1.20  
    1.21 -    def command_range(range: Text.Range): Iterator[(Command, Text.Offset)] =
    1.22 -      command_range(range.start) takeWhile { case (_, start) => start < range.stop }
    1.23 +    def command_iterator(range: Text.Range): Iterator[(Command, Text.Offset)] =
    1.24 +      command_iterator(range.start) takeWhile { case (_, start) => start < range.stop }
    1.25  
    1.26      def command_start(cmd: Command): Option[Text.Offset] =
    1.27        Node.Commands.starts(commands.iterator).find(_._1 == cmd).map(_._2)
    1.28 @@ -733,14 +733,14 @@
    1.29            status: Boolean = false): List[Text.Info[A]] =
    1.30          {
    1.31            val former_range = revert(range)
    1.32 -          val (file_name, command_range_iterator) =
    1.33 +          val (file_name, command_iterator) =
    1.34              load_commands match {
    1.35                case command :: _ => (node_name.node, Iterator((command, 0)))
    1.36 -              case _ => ("", node.command_range(former_range))
    1.37 +              case _ => ("", node.command_iterator(former_range))
    1.38              }
    1.39            val markup_index = Command.Markup_Index(status, file_name)
    1.40            (for {
    1.41 -            (command, command_start) <- command_range_iterator
    1.42 +            (command, command_start) <- command_iterator
    1.43              chunk <- command.chunks.get(file_name).iterator
    1.44              states = state.command_states(version, command)
    1.45              res = result(states)
     2.1 --- a/src/Pure/Thy/thy_syntax.scala	Wed Apr 02 20:22:12 2014 +0200
     2.2 +++ b/src/Pure/Thy/thy_syntax.scala	Wed Apr 02 20:41:44 2014 +0200
     2.3 @@ -141,9 +141,9 @@
     2.4        }
     2.5  
     2.6        val commands =
     2.7 -        if (overlays.is_empty) node.command_range(perspective.range)
     2.8 -        else node.command_range()
     2.9 -      check_ranges(perspective.ranges, commands.toStream)
    2.10 +        (if (overlays.is_empty) node.command_iterator(perspective.range)
    2.11 +         else node.command_iterator()).toStream
    2.12 +      check_ranges(perspective.ranges, commands)
    2.13        (Command.Perspective(visible.toList), Command.Perspective(visible_overlay.toList))
    2.14      }
    2.15    }
     3.1 --- a/src/Tools/jEdit/src/document_view.scala	Wed Apr 02 20:22:12 2014 +0200
     3.2 +++ b/src/Tools/jEdit/src/document_view.scala	Wed Apr 02 20:41:44 2014 +0200
     3.3 @@ -224,15 +224,15 @@
     3.4                      text_area.invalidateScreenLineRange(0, visible_lines)
     3.5                    else {
     3.6                      val visible_range = JEdit_Lib.visible_range(text_area).get
     3.7 -                    val visible_cmds =
     3.8 -                      snapshot.node.command_range(snapshot.revert(visible_range)).map(_._1)
     3.9 -                    if (visible_cmds.exists(changed.commands)) {
    3.10 +                    val visible_iterator =
    3.11 +                      snapshot.node.command_iterator(snapshot.revert(visible_range)).map(_._1)
    3.12 +                    if (visible_iterator.exists(changed.commands)) {
    3.13                        for {
    3.14                          line <- (0 until visible_lines).iterator
    3.15                          start = text_area.getScreenLineStartOffset(line) if start >= 0
    3.16                          end = text_area.getScreenLineEndOffset(line) if end >= 0
    3.17                          range = Text.Range(start, end)
    3.18 -                        line_cmds = snapshot.node.command_range(snapshot.revert(range)).map(_._1)
    3.19 +                        line_cmds = snapshot.node.command_iterator(snapshot.revert(range)).map(_._1)
    3.20                          if line_cmds.exists(changed.commands)
    3.21                        } text_area.invalidateScreenLineRange(line, line)
    3.22                      }
     4.1 --- a/src/Tools/jEdit/src/isabelle_sidekick.scala	Wed Apr 02 20:22:12 2014 +0200
     4.2 +++ b/src/Tools/jEdit/src/isabelle_sidekick.scala	Wed Apr 02 20:41:44 2014 +0200
     4.3 @@ -158,7 +158,7 @@
     4.4      opt_snapshot match {
     4.5        case Some(snapshot) =>
     4.6          val root = data.root
     4.7 -        for ((command, command_start) <- snapshot.node.command_range() if !stopped) {
     4.8 +        for ((command, command_start) <- snapshot.node.command_iterator() if !stopped) {
     4.9            val markup =
    4.10              snapshot.state.command_markup(
    4.11                snapshot.version, command, Command.Markup_Index.markup,
     5.1 --- a/src/Tools/jEdit/src/jedit_editor.scala	Wed Apr 02 20:22:12 2014 +0200
     5.2 +++ b/src/Tools/jEdit/src/jedit_editor.scala	Wed Apr 02 20:41:44 2014 +0200
     5.3 @@ -74,9 +74,9 @@
     5.4          val node = snapshot.version.nodes(doc_view.model.node_name)
     5.5          val caret = snapshot.revert(text_area.getCaretPosition)
     5.6          if (caret < buffer.getLength) {
     5.7 -          val caret_commands = node.command_range(caret)
     5.8 -          if (caret_commands.hasNext) {
     5.9 -            val (cmd0, _) = caret_commands.next
    5.10 +          val caret_command_iterator = node.command_iterator(caret)
    5.11 +          if (caret_command_iterator.hasNext) {
    5.12 +            val (cmd0, _) = caret_command_iterator.next
    5.13              node.commands.reverse.iterator(cmd0).find(cmd => !cmd.is_ignored)
    5.14            }
    5.15            else None
    5.16 @@ -154,11 +154,11 @@
    5.17          case None => None
    5.18          case Some((node, _)) =>
    5.19            val file_name = command.node_name.node
    5.20 -          val sources =
    5.21 +          val sources_iterator =
    5.22              node.commands.iterator.takeWhile(_ != command).map(_.source) ++
    5.23                (if (offset == 0) Iterator.empty
    5.24                 else Iterator.single(command.source(Text.Range(0, command.decode(offset)))))
    5.25 -          val (line, column) = ((1, 1) /: sources)(Symbol.advance_line_column)
    5.26 +          val (line, column) = ((1, 1) /: sources_iterator)(Symbol.advance_line_column)
    5.27            Some(new Hyperlink { def follow(view: View) { goto_file(view, file_name, line, column) } })
    5.28        }
    5.29      }
     6.1 --- a/src/Tools/jEdit/src/rich_text_area.scala	Wed Apr 02 20:22:12 2014 +0200
     6.2 +++ b/src/Tools/jEdit/src/rich_text_area.scala	Wed Apr 02 20:41:44 2014 +0200
     6.3 @@ -359,7 +359,7 @@
     6.4              r2 <- r1.try_restrict(chunk_range)
     6.5            } yield r2
     6.6  
     6.7 -        val padded_markup =
     6.8 +        val padded_markup_iterator =
     6.9            if (markup.isEmpty)
    6.10              Iterator(Text.Info(chunk_range, chunk_color))
    6.11            else
    6.12 @@ -370,7 +370,7 @@
    6.13  
    6.14          var x1 = x + w
    6.15          gfx.setFont(chunk_font)
    6.16 -        for (Text.Info(range, color) <- padded_markup if !range.is_singularity) {
    6.17 +        for (Text.Info(range, color) <- padded_markup_iterator if !range.is_singularity) {
    6.18            val str = chunk_str.substring(range.start - chunk_offset, range.stop - chunk_offset)
    6.19            gfx.setColor(color)
    6.20