# HG changeset patch
# User wenzelm
# Date 1414509544 -3600
# Node ID 3cc68ec558b0358bba99e874e527d3ae3fe80d8c
# Parent  f420225a22d6fb4956220efff16e0cd340cd9aef
find command span in buffer;
tuned signature;

diff -r f420225a22d6 -r 3cc68ec558b0 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 =
diff -r f420225a22d6 -r 3cc68ec558b0 src/Tools/jEdit/src/token_markup.scala
--- a/src/Tools/jEdit/src/token_markup.scala	Tue Oct 28 13:52:54 2014 +0100
+++ b/src/Tools/jEdit/src/token_markup.scala	Tue Oct 28 16:19:04 2014 +0100
@@ -213,7 +213,8 @@
 
   /* line tokens */
 
-  def try_line_tokens(syntax: Outer_Syntax, buffer: JEditBuffer, line: Int): Option[List[Token]] =
+  private def try_line_tokens(syntax: Outer_Syntax, buffer: JEditBuffer, line: Int)
+    : Option[List[Token]] =
   {
     val line_context =
       if (line == 0) Line_Context.init
@@ -253,6 +254,35 @@
     } yield Text.Info(Text.Range(i - tok.source.length, i), tok)
 
 
+  /* command span */
+
+  def command_span(syntax: Outer_Syntax, buffer: JEditBuffer, offset: Text.Offset)
+    : Option[Text.Info[Command_Span.Span]] =
+  {
+    if (JEdit_Lib.buffer_range(buffer).contains(offset)) {
+      val start =
+        line_token_reverse_iterator(syntax, buffer, buffer.getLineOfOffset(offset), -1).
+          dropWhile(info => !info.range.contains(offset)).
+          collectFirst({ case Text.Info(range, tok) if tok.is_command => range.start }).
+          getOrElse(0)
+      val stop =
+        line_token_iterator(syntax, buffer, buffer.getLineOfOffset(start), buffer.getLineCount).
+          dropWhile(info => !info.range.contains(start)).
+          dropWhile(info => info.range.contains(start)).
+          collectFirst({ case Text.Info(range, tok) if tok.is_command => range.start }).
+          getOrElse(buffer.getLength)
+
+      val text = JEdit_Lib.try_get_text(buffer, Text.Range(start, stop)).getOrElse("")
+      val spans = syntax.parse_spans(text)
+
+      (spans.iterator.scanLeft(start)(_ + _.length) zip spans.iterator).
+        map({ case (i, span) => Text.Info(Text.Range(i, i + span.length), span) }).
+        find(_.range.contains(offset))
+    }
+    else None
+  }
+
+
   /* token marker */
 
   class Marker(mode: String) extends TokenMarker