specific types Text.Offset and Text.Range;
authorwenzelm
Sun Aug 15 22:48:56 2010 +0200 (2010-08-15)
changeset 384262858ec7b6dd8
parent 38425 e467db701d78
child 38427 7066fbd315ae
specific types Text.Offset and Text.Range;
minor tuning;
src/Pure/PIDE/command.scala
src/Pure/PIDE/document.scala
src/Pure/PIDE/markup_node.scala
src/Pure/PIDE/text.scala
src/Tools/jEdit/src/jedit/document_model.scala
src/Tools/jEdit/src/jedit/document_view.scala
src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala
src/Tools/jEdit/src/jedit/isabelle_sidekick.scala
     1.1 --- a/src/Pure/PIDE/command.scala	Sun Aug 15 21:42:13 2010 +0200
     1.2 +++ b/src/Pure/PIDE/command.scala	Sun Aug 15 22:48:56 2010 +0200
     1.3 @@ -64,12 +64,12 @@
     1.4          case Command.TypeInfo(_) => true
     1.5          case _ => false }).flatten
     1.6  
     1.7 -    def type_at(pos: Int): Option[String] =
     1.8 +    def type_at(pos: Text.Offset): Option[String] =
     1.9      {
    1.10 -      types.find(t => t.start <= pos && pos < t.stop) match {
    1.11 +      types.find(t => t.range.start <= pos && pos < t.range.stop) match {
    1.12          case Some(t) =>
    1.13            t.info match {
    1.14 -            case Command.TypeInfo(ty) => Some(command.source(t.start, t.stop) + " : " + ty)
    1.15 +            case Command.TypeInfo(ty) => Some(command.source(t.range) + " : " + ty)
    1.16              case _ => None
    1.17            }
    1.18          case None => None
    1.19 @@ -81,8 +81,8 @@
    1.20          case Command.RefInfo(_, _, _, _) => true
    1.21          case _ => false }).flatten
    1.22  
    1.23 -    def ref_at(pos: Int): Option[Markup_Node] =
    1.24 -      refs.find(t => t.start <= pos && pos < t.stop)
    1.25 +    def ref_at(pos: Text.Offset): Option[Markup_Node] =
    1.26 +      refs.find(t => t.range.start <= pos && pos < t.range.stop)
    1.27  
    1.28  
    1.29      /* message dispatch */
    1.30 @@ -166,7 +166,7 @@
    1.31    /* source text */
    1.32  
    1.33    val source: String = span.map(_.source).mkString
    1.34 -  def source(i: Int, j: Int): String = source.substring(i, j)
    1.35 +  def source(range: Text.Range): String = source.substring(range.start, range.stop)
    1.36    def length: Int = source.length
    1.37  
    1.38    lazy val symbol_index = new Symbol.Index(source)
    1.39 @@ -178,7 +178,7 @@
    1.40    {
    1.41      val start = symbol_index.decode(begin)
    1.42      val stop = symbol_index.decode(end)
    1.43 -    new Markup_Tree(new Markup_Node(start, stop, info), Nil)
    1.44 +    new Markup_Tree(new Markup_Node(Text.Range(start, stop), info), Nil)
    1.45    }
    1.46  
    1.47  
     2.1 --- a/src/Pure/PIDE/document.scala	Sun Aug 15 21:42:13 2010 +0200
     2.2 +++ b/src/Pure/PIDE/document.scala	Sun Aug 15 22:48:56 2010 +0200
     2.3 @@ -45,7 +45,8 @@
     2.4      val empty: Node = new Node(Linear_Set())
     2.5  
     2.6      // FIXME not scalable
     2.7 -    def command_starts(commands: Iterator[Command], offset: Int = 0): Iterator[(Command, Int)] =
     2.8 +    def command_starts(commands: Iterator[Command], offset: Text.Offset = 0)
     2.9 +      : Iterator[(Command, Text.Offset)] =
    2.10      {
    2.11        var i = offset
    2.12        for (command <- commands) yield {
    2.13 @@ -58,25 +59,25 @@
    2.14  
    2.15    class Node(val commands: Linear_Set[Command])
    2.16    {
    2.17 -    def command_starts: Iterator[(Command, Int)] =
    2.18 +    def command_starts: Iterator[(Command, Text.Offset)] =
    2.19        Node.command_starts(commands.iterator)
    2.20  
    2.21 -    def command_start(cmd: Command): Option[Int] =
    2.22 +    def command_start(cmd: Command): Option[Text.Offset] =
    2.23        command_starts.find(_._1 == cmd).map(_._2)
    2.24  
    2.25 -    def command_range(i: Int): Iterator[(Command, Int)] =
    2.26 +    def command_range(i: Text.Offset): Iterator[(Command, Text.Offset)] =
    2.27        command_starts dropWhile { case (cmd, start) => start + cmd.length <= i }
    2.28  
    2.29 -    def command_range(i: Int, j: Int): Iterator[(Command, Int)] =
    2.30 +    def command_range(i: Text.Offset, j: Text.Offset): Iterator[(Command, Text.Offset)] =
    2.31        command_range(i) takeWhile { case (_, start) => start < j }
    2.32  
    2.33 -    def command_at(i: Int): Option[(Command, Int)] =
    2.34 +    def command_at(i: Text.Offset): Option[(Command, Text.Offset)] =
    2.35      {
    2.36        val range = command_range(i)
    2.37        if (range.hasNext) Some(range.next) else None
    2.38      }
    2.39  
    2.40 -    def proper_command_at(i: Int): Option[Command] =
    2.41 +    def proper_command_at(i: Text.Offset): Option[Command] =
    2.42        command_at(i) match {
    2.43          case Some((command, _)) =>
    2.44            commands.reverse_iterator(command).find(cmd => !cmd.is_ignored)
    2.45 @@ -122,8 +123,8 @@
    2.46      val version: Version
    2.47      val node: Node
    2.48      val is_outdated: Boolean
    2.49 -    def convert(offset: Int): Int
    2.50 -    def revert(offset: Int): Int
    2.51 +    def convert(i: Text.Offset): Text.Offset
    2.52 +    def revert(i: Text.Offset): Text.Offset
    2.53      def lookup_command(id: Command_ID): Option[Command]
    2.54      def state(command: Command): Command.State
    2.55    }
    2.56 @@ -159,8 +160,10 @@
    2.57          val version = stable.current.join
    2.58          val node = version.nodes(name)
    2.59          val is_outdated = !(pending_edits.isEmpty && latest == stable)
    2.60 -        def convert(offset: Int): Int = (offset /: edits)((i, edit) => edit.convert(i))
    2.61 -        def revert(offset: Int): Int = (offset /: reverse_edits)((i, edit) => edit.revert(i))
    2.62 +
    2.63 +        def convert(offset: Text.Offset) = (offset /: edits)((i, edit) => edit.convert(i))
    2.64 +        def revert(offset: Text.Offset) = (offset /: reverse_edits)((i, edit) => edit.revert(i))
    2.65 +
    2.66          def lookup_command(id: Command_ID): Option[Command] = state_snapshot.lookup_command(id)
    2.67          def state(command: Command): Command.State =
    2.68            try { state_snapshot.command_state(version, command) }
     3.1 --- a/src/Pure/PIDE/markup_node.scala	Sun Aug 15 21:42:13 2010 +0200
     3.2 +++ b/src/Pure/PIDE/markup_node.scala	Sun Aug 15 22:48:56 2010 +0200
     3.3 @@ -12,17 +12,17 @@
     3.4  
     3.5  
     3.6  
     3.7 -case class Markup_Node(val start: Int, val stop: Int, val info: Any)
     3.8 +case class Markup_Node(val range: Text.Range, val info: Any)
     3.9  {
    3.10    def fits_into(that: Markup_Node): Boolean =
    3.11 -    that.start <= this.start && this.stop <= that.stop
    3.12 +    that.range.start <= this.range.start && this.range.stop <= that.range.stop
    3.13  }
    3.14  
    3.15  
    3.16  case class Markup_Tree(val node: Markup_Node, val branches: List[Markup_Tree])
    3.17  {
    3.18    private def add(branch: Markup_Tree) =   // FIXME avoid sort
    3.19 -    copy(branches = (branch :: branches).sortWith((a, b) => a.node.start < b.node.start))
    3.20 +    copy(branches = (branch :: branches).sortWith((a, b) => a.node.range.start < b.node.range.start))
    3.21  
    3.22    private def remove(bs: List[Markup_Tree]) =
    3.23      copy(branches = branches.filterNot(bs.contains(_)))
    3.24 @@ -55,21 +55,21 @@
    3.25  
    3.26    def flatten: List[Markup_Node] =
    3.27    {
    3.28 -    var next_x = node.start
    3.29 +    var next_x = node.range.start
    3.30      if (branches.isEmpty) List(this.node)
    3.31      else {
    3.32        val filled_gaps =
    3.33          for {
    3.34            child <- branches
    3.35            markups =
    3.36 -            if (next_x < child.node.start)
    3.37 -              new Markup_Node(next_x, child.node.start, node.info) :: child.flatten
    3.38 +            if (next_x < child.node.range.start)
    3.39 +              new Markup_Node(Text.Range(next_x, child.node.range.start), node.info) :: child.flatten
    3.40              else child.flatten
    3.41 -          update = (next_x = child.node.stop)
    3.42 +          update = (next_x = child.node.range.stop)
    3.43            markup <- markups
    3.44          } yield markup
    3.45 -      if (next_x < node.stop)
    3.46 -        filled_gaps ::: List(new Markup_Node(next_x, node.stop, node.info))
    3.47 +      if (next_x < node.range.stop)
    3.48 +        filled_gaps ::: List(new Markup_Node(Text.Range(next_x, node.range.stop), node.info))
    3.49        else filled_gaps
    3.50      }
    3.51    }
    3.52 @@ -78,7 +78,7 @@
    3.53  
    3.54  case class Markup_Text(val markup: List[Markup_Tree], val content: String)
    3.55  {
    3.56 -  private val root = new Markup_Tree(new Markup_Node(0, content.length, None), markup)  // FIXME !?
    3.57 +  private val root = new Markup_Tree(new Markup_Node(Text.Range(0, content.length), None), markup)  // FIXME !?
    3.58  
    3.59    def + (new_tree: Markup_Tree): Markup_Text =
    3.60      new Markup_Text((root + new_tree).branches, content)
     4.1 --- a/src/Pure/PIDE/text.scala	Sun Aug 15 21:42:13 2010 +0200
     4.2 +++ b/src/Pure/PIDE/text.scala	Sun Aug 15 22:48:56 2010 +0200
     4.3 @@ -10,15 +10,22 @@
     4.4  
     4.5  object Text
     4.6  {
     4.7 -  /* edits */
     4.8 +  /* offset and range */
     4.9 +
    4.10 +  type Offset = Int
    4.11 +
    4.12 +  sealed case class Range(val start: Offset, val stop: Offset)
    4.13 +
    4.14 +
    4.15 +  /* editing */
    4.16  
    4.17    object Edit
    4.18    {
    4.19 -    def insert(start: Int, text: String): Edit = new Edit(true, start, text)
    4.20 -    def remove(start: Int, text: String): Edit = new Edit(false, start, text)
    4.21 +    def insert(start: Offset, text: String): Edit = new Edit(true, start, text)
    4.22 +    def remove(start: Offset, text: String): Edit = new Edit(false, start, text)
    4.23    }
    4.24  
    4.25 -  class Edit(val is_insert: Boolean, val start: Int, val text: String)
    4.26 +  class Edit(val is_insert: Boolean, val start: Offset, val text: String)
    4.27    {
    4.28      override def toString =
    4.29        (if (is_insert) "Insert(" else "Remove(") + (start, text).toString + ")"
    4.30 @@ -26,22 +33,22 @@
    4.31  
    4.32      /* transform offsets */
    4.33  
    4.34 -    private def transform(do_insert: Boolean, offset: Int): Int =
    4.35 -      if (offset < start) offset
    4.36 -      else if (is_insert == do_insert) offset + text.length
    4.37 -      else (offset - text.length) max start
    4.38 +    private def transform(do_insert: Boolean, i: Offset): Offset =
    4.39 +      if (i < start) i
    4.40 +      else if (is_insert == do_insert) i + text.length
    4.41 +      else (i - text.length) max start
    4.42  
    4.43 -    def convert(offset: Int): Int = transform(true, offset)
    4.44 -    def revert(offset: Int): Int = transform(false, offset)
    4.45 +    def convert(i: Offset): Offset = transform(true, i)
    4.46 +    def revert(i: Offset): Offset = transform(false, i)
    4.47  
    4.48  
    4.49      /* edit strings */
    4.50  
    4.51 -    private def insert(index: Int, string: String): String =
    4.52 -      string.substring(0, index) + text + string.substring(index)
    4.53 +    private def insert(i: Offset, string: String): String =
    4.54 +      string.substring(0, i) + text + string.substring(i)
    4.55  
    4.56 -    private def remove(index: Int, count: Int, string: String): String =
    4.57 -      string.substring(0, index) + string.substring(index + count)
    4.58 +    private def remove(i: Offset, count: Int, string: String): String =
    4.59 +      string.substring(0, i) + string.substring(i + count)
    4.60  
    4.61      def can_edit(string: String, shift: Int): Boolean =
    4.62        shift <= start && start < shift + string.length
    4.63 @@ -50,12 +57,12 @@
    4.64        if (!can_edit(string, shift)) (Some(this), string)
    4.65        else if (is_insert) (None, insert(start - shift, string))
    4.66        else {
    4.67 -        val index = start - shift
    4.68 -        val count = text.length min (string.length - index)
    4.69 +        val i = start - shift
    4.70 +        val count = text.length min (string.length - i)
    4.71          val rest =
    4.72            if (count == text.length) None
    4.73            else Some(Edit.remove(start, text.substring(count)))
    4.74 -        (rest, remove(index, count, string))
    4.75 +        (rest, remove(i, count, string))
    4.76        }
    4.77    }
    4.78  }
     5.1 --- a/src/Tools/jEdit/src/jedit/document_model.scala	Sun Aug 15 21:42:13 2010 +0200
     5.2 +++ b/src/Tools/jEdit/src/jedit/document_model.scala	Sun Aug 15 22:48:56 2010 +0200
     5.3 @@ -186,7 +186,7 @@
     5.4  
     5.5    // simplify slightly odd result of TextArea.getLineEndOffset
     5.6    // NB: jEdit already normalizes \r\n and \r to \n
     5.7 -  def visible_line_end(start: Int, end: Int): Int =
     5.8 +  def visible_line_end(start: Text.Offset, end: Text.Offset): Text.Offset =
     5.9    {
    5.10      val end1 = end - 1
    5.11      if (start <= end1 && end1 < buffer.getLength &&
    5.12 @@ -243,9 +243,9 @@
    5.13      }
    5.14  
    5.15      override def preContentRemoved(buffer: JEditBuffer,
    5.16 -      start_line: Int, start: Int, num_lines: Int, removed_length: Int)
    5.17 +      start_line: Int, offset: Int, num_lines: Int, removed_length: Int)
    5.18      {
    5.19 -      pending_edits += Text.Edit.remove(start, buffer.getText(start, removed_length))
    5.20 +      pending_edits += Text.Edit.remove(offset, buffer.getText(offset, removed_length))
    5.21      }
    5.22    }
    5.23  
    5.24 @@ -272,7 +272,7 @@
    5.25          Document_View(text_area).get.set_styles()
    5.26        */
    5.27  
    5.28 -      def handle_token(style: Byte, offset: Int, length: Int) =
    5.29 +      def handle_token(style: Byte, offset: Text.Offset, length: Int) =
    5.30          handler.handleToken(line_segment, style, offset, length, context)
    5.31  
    5.32        var next_x = start
    5.33 @@ -280,8 +280,8 @@
    5.34          (command, command_start) <-
    5.35            snapshot.node.command_range(snapshot.revert(start), snapshot.revert(stop))
    5.36          markup <- snapshot.state(command).highlight.flatten
    5.37 -        val abs_start = snapshot.convert(command_start + markup.start)
    5.38 -        val abs_stop = snapshot.convert(command_start + markup.stop)
    5.39 +        val abs_start = snapshot.convert(command_start + markup.range.start)
    5.40 +        val abs_stop = snapshot.convert(command_start + markup.range.stop)
    5.41          if (abs_stop > start)
    5.42          if (abs_start < stop)
    5.43          val token_start = (abs_start - start) max 0
     6.1 --- a/src/Tools/jEdit/src/jedit/document_view.scala	Sun Aug 15 21:42:13 2010 +0200
     6.2 +++ b/src/Tools/jEdit/src/jedit/document_view.scala	Sun Aug 15 22:48:56 2010 +0200
     6.3 @@ -152,12 +152,12 @@
     6.4  
     6.5        val snapshot = model.snapshot()
     6.6  
     6.7 -      val command_range: Iterable[(Command, Int)] =
     6.8 +      val command_range: Iterable[(Command, Text.Offset)] =
     6.9        {
    6.10          val range = snapshot.node.command_range(snapshot.revert(start(0)))
    6.11          if (range.hasNext) {
    6.12            val (cmd0, start0) = range.next
    6.13 -          new Iterable[(Command, Int)] {
    6.14 +          new Iterable[(Command, Text.Offset)] {
    6.15              def iterator =
    6.16                Document.Node.command_starts(snapshot.node.commands.iterator(cmd0), start0)
    6.17            }
     7.1 --- a/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala	Sun Aug 15 21:42:13 2010 +0200
     7.2 +++ b/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala	Sun Aug 15 22:48:56 2010 +0200
     7.3 @@ -49,9 +49,9 @@
     7.4            case Some((command, command_start)) =>
     7.5              snapshot.state(command).ref_at(offset - command_start) match {
     7.6                case Some(ref) =>
     7.7 -                val begin = snapshot.convert(command_start + ref.start)
     7.8 +                val begin = snapshot.convert(command_start + ref.range.start)
     7.9                  val line = buffer.getLineOfOffset(begin)
    7.10 -                val end = snapshot.convert(command_start + ref.stop)
    7.11 +                val end = snapshot.convert(command_start + ref.range.stop)
    7.12                  ref.info match {
    7.13                    case Command.RefInfo(Some(ref_file), Some(ref_line), _, _) =>
    7.14                      new External_Hyperlink(begin, end, line, ref_file, ref_line)
     8.1 --- a/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala	Sun Aug 15 21:42:13 2010 +0200
     8.2 +++ b/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala	Sun Aug 15 22:48:56 2010 +0200
     8.3 @@ -131,7 +131,7 @@
     8.4      for ((command, command_start) <- snapshot.node.command_range(0) if !stopped) {
     8.5        root.add(snapshot.state(command).markup.swing_tree((node: Markup_Node) =>
     8.6            {
     8.7 -            val content = command.source(node.start, node.stop).replace('\n', ' ')
     8.8 +            val content = command.source(node.range).replace('\n', ' ')
     8.9              val id = command.id
    8.10  
    8.11              new DefaultMutableTreeNode(new IAsset {
    8.12 @@ -141,9 +141,9 @@
    8.13                override def getName: String = Markup.Long(id)
    8.14                override def setName(name: String) = ()
    8.15                override def setStart(start: Position) = ()
    8.16 -              override def getStart: Position = command_start + node.start
    8.17 +              override def getStart: Position = command_start + node.range.start
    8.18                override def setEnd(end: Position) = ()
    8.19 -              override def getEnd: Position = command_start + node.stop
    8.20 +              override def getEnd: Position = command_start + node.range.stop
    8.21                override def toString = id + ": " + content + "[" + getStart + " - " + getEnd + "]"
    8.22              })
    8.23            }))