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 }))