# HG changeset patch # User wenzelm # Date 1699441229 -3600 # Node ID ecb02f28863625623bd4418593dae40ed23d0271 # Parent ff4496b25197b9a0c542e338f2263d609ccf937b tuned signature; diff -r ff4496b25197 -r ecb02f288636 src/Pure/PIDE/command.scala --- a/src/Pure/PIDE/command.scala Wed Nov 08 11:53:38 2023 +0100 +++ b/src/Pure/PIDE/command.scala Wed Nov 08 12:00:29 2023 +0100 @@ -382,7 +382,7 @@ results: Results = Results.empty, markups: Markups = Markups.empty ): Command = { - val (source1, span1) = Command_Span.unparsed(source, theory).compact_source + val (source1, span1) = Command_Span.unparsed(source, theory = theory).compact_source new Command(id, node_name, blobs_info, span1, source1, results, markups) } diff -r ff4496b25197 -r ecb02f288636 src/Pure/PIDE/command_span.scala --- a/src/Pure/PIDE/command_span.scala Wed Nov 08 11:53:38 2023 +0100 +++ b/src/Pure/PIDE/command_span.scala Wed Nov 08 12:00:29 2023 +0100 @@ -148,7 +148,7 @@ val empty: Span = Span(Ignored_Span, Nil) - def unparsed(source: String, theory: Boolean): Span = { + def unparsed(source: String, theory: Boolean = false): Span = { val kind = if (theory) Theory_Span else Malformed_Span Span(kind, List(Token(Token.Kind.UNPARSED, source))) }