# HG changeset patch # User wenzelm # Date 1281905336 -7200 # Node ID 2858ec7b6dd847e9c60ed2aff9a5bc5268a2af53 # Parent e467db701d781f39fba50e34445db410bde91b88 specific types Text.Offset and Text.Range; minor tuning; diff -r e467db701d78 -r 2858ec7b6dd8 src/Pure/PIDE/command.scala --- 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) } diff -r e467db701d78 -r 2858ec7b6dd8 src/Pure/PIDE/document.scala --- 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) } diff -r e467db701d78 -r 2858ec7b6dd8 src/Pure/PIDE/markup_node.scala --- 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) diff -r e467db701d78 -r 2858ec7b6dd8 src/Pure/PIDE/text.scala --- 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)) } } } diff -r e467db701d78 -r 2858ec7b6dd8 src/Tools/jEdit/src/jedit/document_model.scala --- 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 diff -r e467db701d78 -r 2858ec7b6dd8 src/Tools/jEdit/src/jedit/document_view.scala --- 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) } diff -r e467db701d78 -r 2858ec7b6dd8 src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala --- 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) diff -r e467db701d78 -r 2858ec7b6dd8 src/Tools/jEdit/src/jedit/isabelle_sidekick.scala --- 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 + "]" }) }))