--- a/src/Pure/Isar/line_structure.scala Mon Mar 01 23:17:47 2021 +0100
+++ b/src/Pure/Isar/line_structure.scala Mon Mar 01 23:26:55 2021 +0100
@@ -28,7 +28,7 @@
val command1 = tokens.exists(_.is_begin_or_command)
val command_depth =
- tokens.iterator.filter(_.is_proper).toStream.headOption match {
+ tokens.iterator.filter(_.is_proper).nextOption() match {
case Some(tok) =>
if (keywords.is_command(tok, Keyword.close_structure))
Some(after_span_depth - 1)
--- a/src/Tools/jEdit/src/isabelle.scala Mon Mar 01 23:17:47 2021 +0100
+++ b/src/Tools/jEdit/src/isabelle.scala Mon Mar 01 23:26:55 2021 +0100
@@ -280,7 +280,7 @@
buffer_syntax(buffer) match {
case Some(syntax) =>
val nav = new Text_Structure.Navigator(syntax, buffer, true)
- nav.iterator(line, 1).toStream.headOption match {
+ nav.iterator(line, 1).nextOption() match {
case Some(Text.Info(range, tok))
if range.stop == caret && syntax.keywords.is_indent_command(tok) =>
buffer.indentLine(line, true)
--- a/src/Tools/jEdit/src/text_structure.scala Mon Mar 01 23:17:47 2021 +0100
+++ b/src/Tools/jEdit/src/text_structure.scala Mon Mar 01 23:26:55 2021 +0100
@@ -60,7 +60,7 @@
else buffer.getCurrentIndentForLine(line, null)
def line_head(line: Int): Option[Text.Info[Token]] =
- nav.iterator(line, 1).toStream.headOption
+ nav.iterator(line, 1).nextOption()
def head_is_quasi_command(line: Int): Boolean =
line_head(line) match {
@@ -93,7 +93,7 @@
(for {
text_area <- JEdit_Lib.jedit_text_areas(buffer)
doc_view <- Document_View.get(text_area)
- } yield doc_view.get_rendering).toStream.headOption
+ } yield doc_view.get_rendering).nextOption()
}
else None
val limit = PIDE.options.value.int("jedit_indent_script_limit")