# HG changeset patch
# User wenzelm
# Date 1614637615 -3600
# Node ID 8204f7b5300776e40d8e0b443fa09c8c81165331
# Parent  f5c1476546613b89fd885560afd41413ed09287f
tuned --- fewer warnings;

diff -r f5c147654661 -r 8204f7b53007 src/Pure/Isar/line_structure.scala
--- 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)
diff -r f5c147654661 -r 8204f7b53007 src/Tools/jEdit/src/isabelle.scala
--- 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)
diff -r f5c147654661 -r 8204f7b53007 src/Tools/jEdit/src/text_structure.scala
--- 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")