diff -r 922273b7bf8a -r c0c5652e796e src/Pure/Isar/outer_syntax.scala
--- a/src/Pure/Isar/outer_syntax.scala	Mon Aug 11 22:59:38 2014 +0200
+++ b/src/Pure/Isar/outer_syntax.scala	Tue Aug 12 00:08:32 2014 +0200
@@ -152,6 +152,41 @@
   }
 
 
+  /* parse_spans */
+
+  def parse_spans(toks: List[Token]): List[Command_Span.Span] =
+  {
+    val result = new mutable.ListBuffer[Command_Span.Span]
+    val content = new mutable.ListBuffer[Token]
+    val improper = new mutable.ListBuffer[Token]
+
+    def ship(span: List[Token])
+    {
+      val kind =
+        if (!span.isEmpty && span.head.is_command && !span.exists(_.is_error))
+          Command_Span.Command_Span(span.head.source)
+        else if (span.forall(_.is_improper)) Command_Span.Ignored_Span
+        else Command_Span.Malformed_Span
+      result += Command_Span.Span(kind, span)
+    }
+
+    def flush()
+    {
+      if (!content.isEmpty) { ship(content.toList); content.clear }
+      if (!improper.isEmpty) { ship(improper.toList); improper.clear }
+    }
+
+    for (tok <- toks) {
+      if (tok.is_command) { flush(); content += tok }
+      else if (tok.is_improper) improper += tok
+      else { content ++= improper; improper.clear; content += tok }
+    }
+    flush()
+
+    result.toList
+  }
+
+
   /* language context */
 
   def set_language_context(context: Completion.Language_Context): Outer_Syntax =