sharing of token source with span source;

--- a/src/Pure/PIDE/command.scala	Sat Nov 26 14:14:51 2011 +0100
+++ b/src/Pure/PIDE/command.scala	Sat Nov 26 17:10:03 2011 +0100
@@ -9,6 +9,7 @@
 
 import java.lang.System
 
+import scala.collection.mutable
 import scala.collection.immutable.SortedMap
 
 
@@ -77,14 +78,33 @@
   }
 
 
-  /* dummy commands */
+  /* make commands */
+
+  def apply(id: Document.Command_ID, node_name: Document.Node.Name, toks: List[Token]): Command =
+  {
+    val source: String =
+      toks match {
+        case List(tok) => tok.source
+        case _ => toks.map(_.source).mkString
+      }
+
+    val span = new mutable.ListBuffer[Token]
+    var i = 0
+    for (Token(kind, s) <- toks) {
+      val n = s.length
+      val s1 = source.substring(i, i + n)
+      span += Token(kind, s1)
+      i += n
+    }
+
+    new Command(id, node_name, span.toList, source)
+  }
+
+  def apply(node_name: Document.Node.Name, toks: List[Token]): Command =
+    Command(Document.no_id, node_name, toks)
 
   def unparsed(source: String): Command =
-    new Command(Document.no_id, Document.Node.Name.empty,
-      List(Token(Token.Kind.UNPARSED, source)))
-
-  def span(node_name: Document.Node.Name, toks: List[Token]): Command =
-    new Command(Document.no_id, node_name, toks)
+    Command(Document.no_id, Document.Node.Name.empty, List(Token(Token.Kind.UNPARSED, source)))
 
 
   /* perspective */
@@ -109,10 +129,11 @@
 }
 
 
-class Command(
+class Command private(
     val id: Document.Command_ID,
     val node_name: Document.Node.Name,
-    val span: List[Token])
+    val span: List[Token],
+    val source: String)
 {
   /* classification */
 
@@ -129,7 +150,6 @@
 
   /* source text */
 
-  val source: String = span.map(_.source).mkString
   def source(range: Text.Range): String = source.substring(range.start, range.stop)
   def length: Int = source.length
 

--- a/src/Pure/Thy/thy_syntax.scala	Sat Nov 26 14:14:51 2011 +0100
+++ b/src/Pure/Thy/thy_syntax.scala	Sat Nov 26 17:10:03 2011 +0100
@@ -69,7 +69,7 @@
       /* result structure */
 
       val spans = parse_spans(syntax.scan(text))
-      spans.foreach(span => add(Command.span(node_name, span)))
+      spans.foreach(span => add(Command(node_name, span)))
       result()
     }
   }
@@ -217,7 +217,7 @@
               (Some(last), spans1.take(spans1.length - 1))
             else (commands.next(last), spans1)
 
-          val inserted = spans2.map(span => new Command(Document.new_id(), node_name, span))
+          val inserted = spans2.map(span => Command(Document.new_id(), node_name, span))
           val new_commands =
             commands.delete_between(before_edit, after_edit).append_after(before_edit, inserted)
           recover_spans(node_name, new_commands)