--- 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 {