# HG changeset patch
# User wenzelm
# Date 1392986200 -3600
# Node ID 38f264741609c04c48687ce8718e9fdc271cfdc4
# Parent  106a57dec7af9522b046c0d16f97fbe771a1ac31
tuned signature -- avoid obscure default arguments;

diff -r 106a57dec7af -r 38f264741609 src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Fri Feb 21 12:57:14 2014 +0100
+++ b/src/Pure/PIDE/command.scala	Fri Feb 21 13:36:40 2014 +0100
@@ -15,6 +15,8 @@
 object Command
 {
   type Edit = (Option[Command], Option[Command])
+  type Blob = Exn.Result[(Document.Node.Name, Option[(SHA1.Digest, File)])]
+
 
 
   /** accumulated results from prover **/
@@ -189,15 +191,7 @@
   def name(span: List[Token]): String =
     span.find(_.is_command) match { case Some(tok) => tok.source case _ => "" }
 
-  type Blob = Exn.Result[(Document.Node.Name, Option[(SHA1.Digest, File)])]
-
-  def apply(
-    id: Document_ID.Command,
-    node_name: Document.Node.Name,
-    blobs: List[Blob],
-    span: List[Token],
-    results: Results = Results.empty,
-    markup: Markup_Tree = Markup_Tree.empty): Command =
+  private def source_span(span: List[Token]): (String, List[Token]) =
   {
     val source: String =
       span match {
@@ -213,16 +207,30 @@
       span1 += Token(kind, s1)
       i += n
     }
-
-    new Command(id, node_name, blobs, span1.toList, source, results, markup)
+    (source, span1.toList)
   }
 
-  val empty = Command(Document_ID.none, Document.Node.Name.empty, Nil, Nil)
+  def apply(
+    id: Document_ID.Command,
+    node_name: Document.Node.Name,
+    blobs: List[Blob],
+    span: List[Token]): Command =
+  {
+    val (source, span1) = source_span(span)
+    new Command(id, node_name, blobs, span1, source, Results.empty, Markup_Tree.empty)
+  }
 
-  def unparsed(id: Document_ID.Command, source: String, results: Results, markup: Markup_Tree)
-      : Command =
-    Command(id, Document.Node.Name.empty, Nil, List(Token(Token.Kind.UNPARSED, source)),
-      results, markup)
+  val empty: Command = Command(Document_ID.none, Document.Node.Name.empty, Nil, Nil)
+
+  def unparsed(
+    id: Document_ID.Command,
+    source: String,
+    results: Results,
+    markup: Markup_Tree): Command =
+  {
+    val (source1, span) = source_span(List(Token(Token.Kind.UNPARSED, source)))
+    new Command(id, Document.Node.Name.empty, Nil, span, source1, results, markup)
+  }
 
   def unparsed(source: String): Command =
     unparsed(Document_ID.none, source, Results.empty, Markup_Tree.empty)