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