--- a/src/Pure/Isar/outer_syntax.scala Wed Mar 03 22:48:46 2021 +0100
+++ b/src/Pure/Isar/outer_syntax.scala Thu Mar 04 15:41:46 2021 +0100
@@ -16,7 +16,7 @@
val empty: Outer_Syntax = new Outer_Syntax()
- def merge(syns: List[Outer_Syntax]): Outer_Syntax = (empty /: syns)(_ ++ _)
+ def merge(syns: List[Outer_Syntax]): Outer_Syntax = syns.foldLeft(empty)(_ ++ _)
/* string literals */
@@ -61,7 +61,7 @@
keywords + (name, kind, load_command), rev_abbrevs, language_context, has_tokens = true)
def add_keywords(keywords: Thy_Header.Keywords): Outer_Syntax =
- (this /: keywords) {
+ keywords.foldLeft(this) {
case (syntax, (name, spec)) =>
syntax +
(Symbol.decode(name), spec.kind, spec.load_command) +
@@ -177,8 +177,9 @@
case Some(cmd) =>
val name = cmd.source
val offset =
- (0 /: content.takeWhile(_ != cmd)) {
- case (i, tok) => i + Symbol.length(tok.source) }
+ content.takeWhile(_ != cmd).foldLeft(0) {
+ case (i, tok) => i + Symbol.length(tok.source)
+ }
val end_offset = offset + Symbol.length(name)
val range = Text.Range(offset, end_offset) + 1
Command_Span.Command_Span(name, Position.Range(range))