# 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)