--- a/src/Pure/PIDE/command.scala Sun Mar 04 18:15:45 2012 +0100
+++ b/src/Pure/PIDE/command.scala Sun Mar 04 19:03:28 2012 +0100
@@ -34,7 +34,7 @@
(this /: msgs)((state, msg) =>
msg match {
case elem @ XML.Elem(markup, Nil) =>
- state.add_status(markup).add_markup(Text.Info(command.range, elem))
+ state.add_status(markup).add_markup(Text.Info(command.range, elem)) // FIXME proper_range??
case _ => System.err.println("Ignored status message: " + msg); state
})
@@ -142,15 +142,18 @@
/* source text */
+ def length: Int = source.length
+ val range: Text.Range = Text.Range(0, length)
+
+ val proper_range: Text.Range =
+ Text.Range(0, (length /: span.reverse.iterator.takeWhile(_.is_ignored))(_ - _.source.length))
+
def source(range: Text.Range): String = source.substring(range.start, range.stop)
- def length: Int = source.length
val newlines =
(0 /: Symbol.iterator(source)) {
case (n, s) => if (Symbol.is_physical_newline(s)) n + 1 else n }
- val range: Text.Range = Text.Range(0, length)
-
lazy val symbol_index = new Symbol.Index(source)
def decode(i: Text.Offset): Text.Offset = symbol_index.decode(i)
def decode(r: Text.Range): Text.Range = symbol_index.decode(r)