src/Pure/PIDE/command_span.scala

--- a/src/Pure/PIDE/command_span.scala	Tue Oct 28 13:52:54 2014 +0100
+++ b/src/Pure/PIDE/command_span.scala	Tue Oct 28 16:19:04 2014 +0100
@@ -26,6 +26,8 @@
 
   sealed case class Span(kind: Kind, content: List[Token])
   {
+    def length: Int = (0 /: content)(_ + _.source.length)
+
     def compact_source: (String, Span) =
     {
       val source: String =