# HG changeset patch
# User wenzelm
# Date 1372932131 -7200
# Node ID bc6e0144726a17372bd995fb55d1f85e2b362da7
# Parent  ecc0e00077925d937cd824d520f7df3993beec29
tuned;

diff -r ecc0e0007792 -r bc6e0144726a src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Thu Jul 04 11:55:45 2013 +0200
+++ b/src/Pure/PIDE/command.scala	Thu Jul 04 12:02:11 2013 +0200
@@ -132,8 +132,12 @@
 
   type Span = List[Token]
 
-  def apply(id: Document.Command_ID, node_name: Document.Node.Name, span: Span,
-    results: Results = Results.empty, markup: Markup_Tree = Markup_Tree.empty): Command =
+  def apply(
+    id: Document.Command_ID,
+    node_name: Document.Node.Name,
+    span: Span,
+    results: Results = Results.empty,
+    markup: Markup_Tree = Markup_Tree.empty): Command =
   {
     val source: String =
       span match {