--- a/src/Pure/PIDE/command.scala Sun Aug 15 21:42:13 2010 +0200
+++ b/src/Pure/PIDE/command.scala Sun Aug 15 22:48:56 2010 +0200
@@ -64,12 +64,12 @@
case Command.TypeInfo(_) => true
case _ => false }).flatten
- def type_at(pos: Int): Option[String] =
+ def type_at(pos: Text.Offset): Option[String] =
{
- types.find(t => t.start <= pos && pos < t.stop) match {
+ types.find(t => t.range.start <= pos && pos < t.range.stop) match {
case Some(t) =>
t.info match {
- case Command.TypeInfo(ty) => Some(command.source(t.start, t.stop) + " : " + ty)
+ case Command.TypeInfo(ty) => Some(command.source(t.range) + " : " + ty)
case _ => None
}
case None => None
@@ -81,8 +81,8 @@
case Command.RefInfo(_, _, _, _) => true
case _ => false }).flatten
- def ref_at(pos: Int): Option[Markup_Node] =
- refs.find(t => t.start <= pos && pos < t.stop)
+ def ref_at(pos: Text.Offset): Option[Markup_Node] =
+ refs.find(t => t.range.start <= pos && pos < t.range.stop)
/* message dispatch */
@@ -166,7 +166,7 @@
/* source text */
val source: String = span.map(_.source).mkString
- def source(i: Int, j: Int): String = source.substring(i, j)
+ def source(range: Text.Range): String = source.substring(range.start, range.stop)
def length: Int = source.length
lazy val symbol_index = new Symbol.Index(source)
@@ -178,7 +178,7 @@
{
val start = symbol_index.decode(begin)
val stop = symbol_index.decode(end)
- new Markup_Tree(new Markup_Node(start, stop, info), Nil)
+ new Markup_Tree(new Markup_Node(Text.Range(start, stop), info), Nil)
}
--- a/src/Pure/PIDE/document.scala Sun Aug 15 21:42:13 2010 +0200
+++ b/src/Pure/PIDE/document.scala Sun Aug 15 22:48:56 2010 +0200
@@ -45,7 +45,8 @@
val empty: Node = new Node(Linear_Set())
// FIXME not scalable
- def command_starts(commands: Iterator[Command], offset: Int = 0): Iterator[(Command, Int)] =
+ def command_starts(commands: Iterator[Command], offset: Text.Offset = 0)
+ : Iterator[(Command, Text.Offset)] =
{
var i = offset
for (command <- commands) yield {
@@ -58,25 +59,25 @@
class Node(val commands: Linear_Set[Command])
{
- def command_starts: Iterator[(Command, Int)] =
+ def command_starts: Iterator[(Command, Text.Offset)] =
Node.command_starts(commands.iterator)
- def command_start(cmd: Command): Option[Int] =
+ def command_start(cmd: Command): Option[Text.Offset] =
command_starts.find(_._1 == cmd).map(_._2)
- def command_range(i: Int): Iterator[(Command, Int)] =
+ def command_range(i: Text.Offset): Iterator[(Command, Text.Offset)] =
command_starts dropWhile { case (cmd, start) => start + cmd.length <= i }
- def command_range(i: Int, j: Int): Iterator[(Command, Int)] =
+ def command_range(i: Text.Offset, j: Text.Offset): Iterator[(Command, Text.Offset)] =
command_range(i) takeWhile { case (_, start) => start < j }
- def command_at(i: Int): Option[(Command, Int)] =
+ def command_at(i: Text.Offset): Option[(Command, Text.Offset)] =
{
val range = command_range(i)
if (range.hasNext) Some(range.next) else None
}
- def proper_command_at(i: Int): Option[Command] =
+ def proper_command_at(i: Text.Offset): Option[Command] =
command_at(i) match {
case Some((command, _)) =>
commands.reverse_iterator(command).find(cmd => !cmd.is_ignored)
@@ -122,8 +123,8 @@
val version: Version
val node: Node
val is_outdated: Boolean
- def convert(offset: Int): Int
- def revert(offset: Int): Int
+ def convert(i: Text.Offset): Text.Offset
+ def revert(i: Text.Offset): Text.Offset
def lookup_command(id: Command_ID): Option[Command]
def state(command: Command): Command.State
}
@@ -159,8 +160,10 @@
val version = stable.current.join
val node = version.nodes(name)
val is_outdated = !(pending_edits.isEmpty && latest == stable)
- def convert(offset: Int): Int = (offset /: edits)((i, edit) => edit.convert(i))
- def revert(offset: Int): Int = (offset /: reverse_edits)((i, edit) => edit.revert(i))
+
+ def convert(offset: Text.Offset) = (offset /: edits)((i, edit) => edit.convert(i))
+ def revert(offset: Text.Offset) = (offset /: reverse_edits)((i, edit) => edit.revert(i))
+
def lookup_command(id: Command_ID): Option[Command] = state_snapshot.lookup_command(id)
def state(command: Command): Command.State =
try { state_snapshot.command_state(version, command) }
--- a/src/Pure/PIDE/markup_node.scala Sun Aug 15 21:42:13 2010 +0200
+++ b/src/Pure/PIDE/markup_node.scala Sun Aug 15 22:48:56 2010 +0200
@@ -12,17 +12,17 @@
-case class Markup_Node(val start: Int, val stop: Int, val info: Any)
+case class Markup_Node(val range: Text.Range, val info: Any)
{
def fits_into(that: Markup_Node): Boolean =
- that.start <= this.start && this.stop <= that.stop
+ that.range.start <= this.range.start && this.range.stop <= that.range.stop
}
case class Markup_Tree(val node: Markup_Node, val branches: List[Markup_Tree])
{
private def add(branch: Markup_Tree) = // FIXME avoid sort
- copy(branches = (branch :: branches).sortWith((a, b) => a.node.start < b.node.start))
+ copy(branches = (branch :: branches).sortWith((a, b) => a.node.range.start < b.node.range.start))
private def remove(bs: List[Markup_Tree]) =
copy(branches = branches.filterNot(bs.contains(_)))
@@ -55,21 +55,21 @@
def flatten: List[Markup_Node] =
{
- var next_x = node.start
+ var next_x = node.range.start
if (branches.isEmpty) List(this.node)
else {
val filled_gaps =
for {
child <- branches
markups =
- if (next_x < child.node.start)
- new Markup_Node(next_x, child.node.start, node.info) :: child.flatten
+ if (next_x < child.node.range.start)
+ new Markup_Node(Text.Range(next_x, child.node.range.start), node.info) :: child.flatten
else child.flatten
- update = (next_x = child.node.stop)
+ update = (next_x = child.node.range.stop)
markup <- markups
} yield markup
- if (next_x < node.stop)
- filled_gaps ::: List(new Markup_Node(next_x, node.stop, node.info))
+ if (next_x < node.range.stop)
+ filled_gaps ::: List(new Markup_Node(Text.Range(next_x, node.range.stop), node.info))
else filled_gaps
}
}
@@ -78,7 +78,7 @@
case class Markup_Text(val markup: List[Markup_Tree], val content: String)
{
- private val root = new Markup_Tree(new Markup_Node(0, content.length, None), markup) // FIXME !?
+ private val root = new Markup_Tree(new Markup_Node(Text.Range(0, content.length), None), markup) // FIXME !?
def + (new_tree: Markup_Tree): Markup_Text =
new Markup_Text((root + new_tree).branches, content)
--- a/src/Pure/PIDE/text.scala Sun Aug 15 21:42:13 2010 +0200
+++ b/src/Pure/PIDE/text.scala Sun Aug 15 22:48:56 2010 +0200
@@ -10,15 +10,22 @@
object Text
{
- /* edits */
+ /* offset and range */
+
+ type Offset = Int
+
+ sealed case class Range(val start: Offset, val stop: Offset)
+
+
+ /* editing */
object Edit
{
- def insert(start: Int, text: String): Edit = new Edit(true, start, text)
- def remove(start: Int, text: String): Edit = new Edit(false, start, text)
+ def insert(start: Offset, text: String): Edit = new Edit(true, start, text)
+ def remove(start: Offset, text: String): Edit = new Edit(false, start, text)
}
- class Edit(val is_insert: Boolean, val start: Int, val text: String)
+ class Edit(val is_insert: Boolean, val start: Offset, val text: String)
{
override def toString =
(if (is_insert) "Insert(" else "Remove(") + (start, text).toString + ")"
@@ -26,22 +33,22 @@
/* transform offsets */
- private def transform(do_insert: Boolean, offset: Int): Int =
- if (offset < start) offset
- else if (is_insert == do_insert) offset + text.length
- else (offset - text.length) max start
+ private def transform(do_insert: Boolean, i: Offset): Offset =
+ if (i < start) i
+ else if (is_insert == do_insert) i + text.length
+ else (i - text.length) max start
- def convert(offset: Int): Int = transform(true, offset)
- def revert(offset: Int): Int = transform(false, offset)
+ def convert(i: Offset): Offset = transform(true, i)
+ def revert(i: Offset): Offset = transform(false, i)
/* edit strings */
- private def insert(index: Int, string: String): String =
- string.substring(0, index) + text + string.substring(index)
+ private def insert(i: Offset, string: String): String =
+ string.substring(0, i) + text + string.substring(i)
- private def remove(index: Int, count: Int, string: String): String =
- string.substring(0, index) + string.substring(index + count)
+ private def remove(i: Offset, count: Int, string: String): String =
+ string.substring(0, i) + string.substring(i + count)
def can_edit(string: String, shift: Int): Boolean =
shift <= start && start < shift + string.length
@@ -50,12 +57,12 @@
if (!can_edit(string, shift)) (Some(this), string)
else if (is_insert) (None, insert(start - shift, string))
else {
- val index = start - shift
- val count = text.length min (string.length - index)
+ val i = start - shift
+ val count = text.length min (string.length - i)
val rest =
if (count == text.length) None
else Some(Edit.remove(start, text.substring(count)))
- (rest, remove(index, count, string))
+ (rest, remove(i, count, string))
}
}
}
--- a/src/Tools/jEdit/src/jedit/document_model.scala Sun Aug 15 21:42:13 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/document_model.scala Sun Aug 15 22:48:56 2010 +0200
@@ -186,7 +186,7 @@
// simplify slightly odd result of TextArea.getLineEndOffset
// NB: jEdit already normalizes \r\n and \r to \n
- def visible_line_end(start: Int, end: Int): Int =
+ def visible_line_end(start: Text.Offset, end: Text.Offset): Text.Offset =
{
val end1 = end - 1
if (start <= end1 && end1 < buffer.getLength &&
@@ -243,9 +243,9 @@
}
override def preContentRemoved(buffer: JEditBuffer,
- start_line: Int, start: Int, num_lines: Int, removed_length: Int)
+ start_line: Int, offset: Int, num_lines: Int, removed_length: Int)
{
- pending_edits += Text.Edit.remove(start, buffer.getText(start, removed_length))
+ pending_edits += Text.Edit.remove(offset, buffer.getText(offset, removed_length))
}
}
@@ -272,7 +272,7 @@
Document_View(text_area).get.set_styles()
*/
- def handle_token(style: Byte, offset: Int, length: Int) =
+ def handle_token(style: Byte, offset: Text.Offset, length: Int) =
handler.handleToken(line_segment, style, offset, length, context)
var next_x = start
@@ -280,8 +280,8 @@
(command, command_start) <-
snapshot.node.command_range(snapshot.revert(start), snapshot.revert(stop))
markup <- snapshot.state(command).highlight.flatten
- val abs_start = snapshot.convert(command_start + markup.start)
- val abs_stop = snapshot.convert(command_start + markup.stop)
+ val abs_start = snapshot.convert(command_start + markup.range.start)
+ val abs_stop = snapshot.convert(command_start + markup.range.stop)
if (abs_stop > start)
if (abs_start < stop)
val token_start = (abs_start - start) max 0
--- a/src/Tools/jEdit/src/jedit/document_view.scala Sun Aug 15 21:42:13 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/document_view.scala Sun Aug 15 22:48:56 2010 +0200
@@ -152,12 +152,12 @@
val snapshot = model.snapshot()
- val command_range: Iterable[(Command, Int)] =
+ val command_range: Iterable[(Command, Text.Offset)] =
{
val range = snapshot.node.command_range(snapshot.revert(start(0)))
if (range.hasNext) {
val (cmd0, start0) = range.next
- new Iterable[(Command, Int)] {
+ new Iterable[(Command, Text.Offset)] {
def iterator =
Document.Node.command_starts(snapshot.node.commands.iterator(cmd0), start0)
}
--- a/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala Sun Aug 15 21:42:13 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala Sun Aug 15 22:48:56 2010 +0200
@@ -49,9 +49,9 @@
case Some((command, command_start)) =>
snapshot.state(command).ref_at(offset - command_start) match {
case Some(ref) =>
- val begin = snapshot.convert(command_start + ref.start)
+ val begin = snapshot.convert(command_start + ref.range.start)
val line = buffer.getLineOfOffset(begin)
- val end = snapshot.convert(command_start + ref.stop)
+ val end = snapshot.convert(command_start + ref.range.stop)
ref.info match {
case Command.RefInfo(Some(ref_file), Some(ref_line), _, _) =>
new External_Hyperlink(begin, end, line, ref_file, ref_line)
--- a/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala Sun Aug 15 21:42:13 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala Sun Aug 15 22:48:56 2010 +0200
@@ -131,7 +131,7 @@
for ((command, command_start) <- snapshot.node.command_range(0) if !stopped) {
root.add(snapshot.state(command).markup.swing_tree((node: Markup_Node) =>
{
- val content = command.source(node.start, node.stop).replace('\n', ' ')
+ val content = command.source(node.range).replace('\n', ' ')
val id = command.id
new DefaultMutableTreeNode(new IAsset {
@@ -141,9 +141,9 @@
override def getName: String = Markup.Long(id)
override def setName(name: String) = ()
override def setStart(start: Position) = ()
- override def getStart: Position = command_start + node.start
+ override def getStart: Position = command_start + node.range.start
override def setEnd(end: Position) = ()
- override def getEnd: Position = command_start + node.stop
+ override def getEnd: Position = command_start + node.range.stop
override def toString = id + ": " + content + "[" + getStart + " - " + getEnd + "]"
})
}))