# HG changeset patch
# User wenzelm
# Date 1330884208 -3600
# Node ID bb7280848c992f1970e2f307db1f2f7b84675ded
# Parent  3d55ef732cd7362b96f4f17e9e3e6187cb71640e
added Command.proper_range (still unused);

diff -r 3d55ef732cd7 -r bb7280848c99 src/Pure/PIDE/command.scala
--- 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)