diff --git a/src/Pure/General/file_watcher.scala b/src/Pure/General/file_watcher.scala
--- a/src/Pure/General/file_watcher.scala
+++ b/src/Pure/General/file_watcher.scala
@@ -1,136 +1,135 @@
 /*  Title:      Pure/General/file_watcher.scala
     Author:     Makarius
 
 Watcher for file-system events.
 */
 
 package isabelle
 
 
 import java.io.{File => JFile}
 import java.nio.file.FileSystems
 import java.nio.file.{WatchKey, WatchEvent, Path => JPath}
 import java.nio.file.StandardWatchEventKinds.{ENTRY_CREATE, ENTRY_DELETE, ENTRY_MODIFY}
 
-import scala.collection.JavaConverters
+import scala.jdk.CollectionConverters._
 
 
 class File_Watcher private[File_Watcher]  // dummy template
 {
   def register(dir: JFile): Unit = {}
   def register_parent(file: JFile): Unit = {}
   def deregister(dir: JFile): Unit = {}
   def purge(retain: Set[JFile]): Unit = {}
   def shutdown(): Unit = {}
 }
 
 object File_Watcher
 {
   val none: File_Watcher = new File_Watcher
   {
     override def toString: String = "File_Watcher.none"
   }
 
   def apply(handle: Set[JFile] => Unit, delay: => Time = Time.seconds(0.5)): File_Watcher =
     if (Platform.is_windows) none else new Impl(handle, delay)
 
 
   /* proper implementation */
 
   sealed case class State(
     dirs: Map[JFile, WatchKey] = Map.empty,
     changed: Set[JFile] = Set.empty)
 
   class Impl private[File_Watcher](handle: Set[JFile] => Unit, delay: Time) extends File_Watcher
   {
     private val state = Synchronized(File_Watcher.State())
     private val watcher = FileSystems.getDefault.newWatchService()
 
     override def toString: String =
       state.value.dirs.keySet.mkString("File_Watcher(", ", ", ")")
 
 
     /* registered directories */
 
     override def register(dir: JFile): Unit =
       state.change(st =>
         st.dirs.get(dir) match {
           case Some(key) if key.isValid => st
           case _ =>
             val key = dir.toPath.register(watcher, ENTRY_CREATE, ENTRY_DELETE, ENTRY_MODIFY)
             st.copy(dirs = st.dirs + (dir -> key))
         })
 
     override def register_parent(file: JFile): Unit =
     {
       val dir = file.getParentFile
       if (dir != null && dir.isDirectory) register(dir)
     }
 
     override def deregister(dir: JFile): Unit =
       state.change(st =>
         st.dirs.get(dir) match {
           case None => st
           case Some(key) =>
             key.cancel
             st.copy(dirs = st.dirs - dir)
         })
 
     override def purge(retain: Set[JFile]): Unit =
       state.change(st =>
         st.copy(dirs = st.dirs --
           (for ((dir, key) <- st.dirs.iterator if !retain(dir)) yield { key.cancel; dir })))
 
 
     /* changed directory entries */
 
     private val delay_changed = Delay.last(delay)
     {
       val changed = state.change_result(st => (st.changed, st.copy(changed = Set.empty)))
       handle(changed)
     }
 
     private val watcher_thread = Isabelle_Thread.fork(name = "file_watcher", daemon = true)
     {
       try {
         while (true) {
           val key = watcher.take
           val has_changed =
             state.change_result(st =>
               {
                 val (remove, changed) =
                   st.dirs.collectFirst({ case (dir, key1) if key == key1 => dir }) match {
                     case Some(dir) =>
-                      val events =
-                        JavaConverters.collectionAsScalaIterable(
-                          key.pollEvents.asInstanceOf[java.util.List[WatchEvent[JPath]]])
+                      val events: Iterable[WatchEvent[JPath]] =
+                        key.pollEvents.asInstanceOf[java.util.List[WatchEvent[JPath]]].asScala
                       val remove = if (key.reset) None else Some(dir)
                       val changed =
                         (Set.empty[JFile] /: events.iterator) {
                           case (set, event) => set + dir.toPath.resolve(event.context).toFile
                         }
                       (remove, changed)
                     case None =>
                       key.pollEvents
                       key.reset
                       (None, Set.empty[JFile])
                   }
                 (changed.nonEmpty, st.copy(dirs = st.dirs -- remove, changed = st.changed ++ changed))
               })
           if (has_changed) delay_changed.invoke()
         }
       }
       catch { case Exn.Interrupt() => }
     }
 
 
     /* shutdown */
 
     override def shutdown(): Unit =
     {
       watcher_thread.interrupt
       watcher_thread.join
       delay_changed.revoke
     }
   }
 }
diff --git a/src/Tools/jEdit/src/fold_handling.scala b/src/Tools/jEdit/src/fold_handling.scala
--- a/src/Tools/jEdit/src/fold_handling.scala
+++ b/src/Tools/jEdit/src/fold_handling.scala
@@ -1,80 +1,79 @@
 /*  Title:      Tools/jEdit/src/fold_handling.scala
     Author:     Makarius
 
 Handling of folds within the text structure.
 */
 
 package isabelle.jedit
 
 
 import isabelle._
 
 import javax.swing.text.Segment
 
-import scala.collection.JavaConverters
+import scala.jdk.CollectionConverters._
 
 import org.gjt.sp.jedit.buffer.{JEditBuffer, FoldHandler}
 
 
 object Fold_Handling
 {
   /* input: dynamic line context  */
 
   class Fold_Handler extends FoldHandler("isabelle")
   {
     override def equals(other: Any): Boolean =
       other match {
         case that: Fold_Handler => true
         case _ => false
       }
 
     override def getFoldLevel(buffer: JEditBuffer, line: Int, seg: Segment): Int =
       Token_Markup.Line_Context.after(buffer, line).structure.depth max 0
 
     override def getPrecedingFoldLevels(
       buffer: JEditBuffer, line: Int, seg: Segment, level: Int): java.util.List[Integer] =
     {
       val structure = Token_Markup.Line_Context.after(buffer, line).structure
       val result =
         if (line > 0 && structure.command)
           Range.inclusive(line - 1, 0, -1).iterator.
             map(i => Token_Markup.Line_Context.after(buffer, i).structure).
             takeWhile(_.improper).map(_ => structure.depth max 0).toList
         else Nil
 
-      if (result.isEmpty) null
-      else JavaConverters.seqAsJavaList(result.map(Integer.valueOf))
+      if (result.isEmpty) null else result.map(Integer.valueOf).asJava
     }
   }
 
 
   /* output: static document rendering */
 
   class Document_Fold_Handler(private val rendering: JEdit_Rendering)
     extends FoldHandler("isabelle-document")
   {
     override def equals(other: Any): Boolean =
       other match {
         case that: Document_Fold_Handler => this.rendering == that.rendering
         case _ => false
       }
 
     override def getFoldLevel(buffer: JEditBuffer, line: Int, seg: Segment): Int =
     {
       def depth(i: Text.Offset): Int =
         if (i < 0) 0
         else {
           rendering.fold_depth(Text.Range(i, i + 1)) match {
             case Text.Info(_, d) :: _ => d
             case _ => 0
           }
         }
 
       if (line <= 0) 0
       else {
         val range = JEdit_Lib.line_range(buffer, line - 1)
         buffer.getFoldLevel(line - 1) - depth(range.start - 1) + depth(range.stop - 1)
       }
     }
   }
 }
diff --git a/src/Tools/jEdit/src/keymap_merge.scala b/src/Tools/jEdit/src/keymap_merge.scala
--- a/src/Tools/jEdit/src/keymap_merge.scala
+++ b/src/Tools/jEdit/src/keymap_merge.scala
@@ -1,259 +1,259 @@
 /*  Title:      Tools/jEdit/src/keymap_merge.scala
     Author:     Makarius
 
 Merge of Isabelle shortcuts vs. jEdit keymap.
 */
 
 package isabelle.jedit
 
 
 import isabelle._
 
 import java.awt.{Color, Dimension, BorderLayout}
 import javax.swing.{JPanel, JTable, JScrollPane, JOptionPane}
 import javax.swing.table.AbstractTableModel
 
-import scala.collection.JavaConverters
+import scala.jdk.CollectionConverters._
 
 import org.gjt.sp.jedit.{jEdit, View}
 import org.gjt.sp.util.GenericGUIUtilities
 import org.jedit.keymap.{KeymapManager, Keymap}
 
 
 object Keymap_Merge
 {
   /** shortcuts **/
 
   private def is_shortcut(property: String): Boolean =
     (property.endsWith(".shortcut") || property.endsWith(".shortcut2")) &&
     !property.startsWith("options.shortcuts.")
 
   class Shortcut(val property: String, val binding: String)
   {
     override def toString: String = property + "=" + binding
 
     def primary: Boolean = property.endsWith(".shortcut")
 
     val action: String =
       Library.try_unsuffix(".shortcut", property) orElse
       Library.try_unsuffix(".shortcut2", property) getOrElse
       error("Bad shortcut property: " + quote(property))
 
     val label: String =
       GenericGUIUtilities.prettifyMenuLabel(jEdit.getProperty(action + ".label", ""))
 
 
     /* ignore wrt. keymap */
 
     private def prop_ignore: String = property + ".ignore"
 
     def ignored_keymaps(): List[String] =
       space_explode(',', jEdit.getProperty(prop_ignore, ""))
 
     def is_ignored(keymap_name: String): Boolean =
       ignored_keymaps().contains(keymap_name)
 
     def ignore(keymap_name: String): Unit =
       jEdit.setProperty(prop_ignore,
         Library.insert(keymap_name)(ignored_keymaps()).sorted.mkString(","))
 
     def set(keymap: Keymap): Unit = keymap.setShortcut(property, binding)
     def reset(keymap: Keymap): Unit = keymap.setShortcut(property, null)
   }
 
 
   /* content wrt. keymap */
 
   def convert_properties(props: java.util.Properties): List[Shortcut] =
     if (props == null) Nil
     else {
       var result = List.empty[Shortcut]
-      for (entry <- JavaConverters.mapAsScalaMap(props)) {
+      for (entry <- props.asScala) {
         entry match {
           case (a: String, b: String) if is_shortcut(a) =>
             result ::= new Shortcut(a, b)
           case _ =>
         }
       }
       result.sortBy(_.property)
     }
 
   def get_shortcut_conflicts(keymap_name: String, keymap: Keymap): List[(Shortcut, List[Shortcut])] =
   {
     val keymap_shortcuts =
       if (keymap == null) Nil
       else convert_properties(Untyped.get[java.util.Properties](keymap, "props"))
 
     for (s <- convert_properties(jEdit.getProperties) if !s.is_ignored(keymap_name)) yield {
       val conflicts =
         keymap_shortcuts.filter(s1 =>
           s.property == s1.property && s.binding != s1.binding ||
           s.property != s1.property && s.binding == s1.binding && s1.binding != "")
       (s, conflicts)
     }
   }
 
 
 
   /** table **/
 
   private def conflict_color: Color =
     PIDE.options.color_value("error_color")
 
   private sealed case class Table_Entry(shortcut: Shortcut, head: Option[Int], tail: List[Int])
   {
     override def toString: String =
       if (head.isEmpty) "<html>" + HTML.output(shortcut.toString) + "</html>"
       else
         "<html><font style='color: #" + Color_Value.print(conflict_color) + ";'>" +
           HTML.output("--- " + shortcut.toString) +
         "</font></html>"
   }
 
   private class Table_Model(entries: List[Table_Entry]) extends AbstractTableModel
   {
     private val entries_count = entries.length
     private def has_entry(row: Int): Boolean = 0 <= row && row <= entries_count
     private def get_entry(row: Int): Option[Table_Entry] =
       if (has_entry(row)) Some(entries(row)) else None
 
     private val selected =
       Synchronized[Set[Int]](
         (for ((e, i) <- entries.iterator.zipWithIndex if e.head.isEmpty) yield i).toSet)
 
     private def is_selected(row: Int): Boolean =
       selected.value.contains(row)
 
     private def select(head: Int, tail: List[Int], b: Boolean): Unit =
       selected.change(set => if (b) set + head -- tail else set - head ++ tail)
 
     def apply(keymap_name: String, keymap: Keymap): Unit =
     {
       GUI_Thread.require {}
 
       for ((entry, row) <- entries.iterator.zipWithIndex if entry.head.isEmpty) {
         val b = is_selected(row)
         if (b) {
           entry.tail.foreach(i => entries(i).shortcut.reset(keymap))
           entry.shortcut.set(keymap)
         }
         else
           entry.shortcut.ignore(keymap_name)
       }
     }
 
     override def getColumnCount: Int = 2
 
     override def getColumnClass(i: Int): Class[_ <: Object] =
       if (i == 0) classOf[java.lang.Boolean] else classOf[Object]
 
     override def getColumnName(i: Int): String =
       if (i == 0) " " else if (i == 1) "Keyboard shortcut" else "???"
 
     override def getRowCount: Int = entries_count
 
     override def getValueAt(row: Int, column: Int): AnyRef =
     {
       get_entry(row) match {
         case Some(entry) if column == 0 => java.lang.Boolean.valueOf(is_selected(row))
         case Some(entry) if column == 1 => entry
         case _ => null
       }
     }
 
     override def isCellEditable(row: Int, column: Int): Boolean =
       has_entry(row) && column == 0
 
     override def setValueAt(value: AnyRef, row: Int, column: Int): Unit =
     {
       value match {
         case obj: java.lang.Boolean if has_entry(row) && column == 0 =>
           val b = obj.booleanValue
           val entry = entries(row)
           entry.head match {
             case None => select(row, entry.tail, b)
             case Some(head_row) =>
               val head_entry = entries(head_row)
               select(head_row, head_entry.tail, !b)
           }
           GUI_Thread.later { fireTableDataChanged() }
         case _ =>
       }
     }
   }
 
   private class Table(table_model: Table_Model) extends JPanel(new BorderLayout)
   {
     private val cell_size = GenericGUIUtilities.defaultTableCellSize()
     private val table_size = new Dimension(cell_size.width * 2, cell_size.height * 15)
 
     val table = new JTable(table_model)
     table.setShowGrid(false)
     table.setIntercellSpacing(new Dimension(0, 0))
     table.setRowHeight(cell_size.height + 2)
     table.setPreferredScrollableViewportSize(table_size)
     table.setFillsViewportHeight(true)
     table.getTableHeader.setReorderingAllowed(false)
 
 		table.getColumnModel.getColumn(0).setPreferredWidth(30)
 		table.getColumnModel.getColumn(0).setMinWidth(30)
 		table.getColumnModel.getColumn(0).setMaxWidth(30)
 		table.getColumnModel.getColumn(0).setResizable(false)
 		table.getColumnModel.getColumn(1).setPreferredWidth(table_size.width - 30)
 
     val scroller = new JScrollPane(table)
 		scroller.getViewport.setBackground(table.getBackground)
 		scroller.setPreferredSize(table_size)
 
     add(scroller, BorderLayout.CENTER)
   }
 
 
 
   /** check with optional dialog **/
 
   def check_dialog(view: View): Unit =
   {
     GUI_Thread.require {}
 
     val keymap_manager = jEdit.getKeymapManager
     val keymap_name = jEdit.getProperty("keymap.current", KeymapManager.DEFAULT_KEYMAP_NAME)
     val keymap =
       keymap_manager.getKeymap(keymap_name) match {
         case null => keymap_manager.getKeymap(KeymapManager.DEFAULT_KEYMAP_NAME)
         case keymap => keymap
       }
 
     val all_shortcut_conflicts = get_shortcut_conflicts(keymap_name, keymap)
     val no_shortcut_conflicts = for ((s, cs) <- all_shortcut_conflicts if cs.isEmpty) yield s
     val shortcut_conflicts = all_shortcut_conflicts.filter(_._2.nonEmpty)
 
     val table_entries =
       for {
         ((shortcut, conflicts), i) <- shortcut_conflicts zip
           shortcut_conflicts.scanLeft(0)({ case (i, (_, cs)) => i + 1 + cs.length })
         entry <-
           Table_Entry(shortcut, None, ((i + 1) to (i + conflicts.length)).toList) ::
           conflicts.map(Table_Entry(_, Some(i), Nil))
       } yield entry
 
     val table_model = new Table_Model(table_entries)
 
     if (table_entries.nonEmpty &&
         GUI.confirm_dialog(view,
           "Pending Isabelle/jEdit keymap changes",
           JOptionPane.OK_CANCEL_OPTION,
           "The following Isabelle keymap changes are in conflict with the current",
           "jEdit keymap " + quote(keymap_name) + ":",
           new Table(table_model),
           "Selected shortcuts will be applied, unselected changes will be ignored.",
           "Results are stored in $JEDIT_SETTINGS/properties and $JEDIT_SETTINGS/keymaps/.") == 0)
     { table_model.apply(keymap_name, keymap) }
 
     no_shortcut_conflicts.foreach(_.set(keymap))
 
     keymap.save()
     jEdit.saveSettings()
     jEdit.propertiesChanged()
   }
 }
diff --git a/src/Tools/jEdit/src/token_markup.scala b/src/Tools/jEdit/src/token_markup.scala
--- a/src/Tools/jEdit/src/token_markup.scala
+++ b/src/Tools/jEdit/src/token_markup.scala
@@ -1,314 +1,312 @@
 /*  Title:      Tools/jEdit/src/token_markup.scala
     Author:     Makarius
 
 Outer syntax token markup.
 */
 
 package isabelle.jedit
 
 
 import isabelle._
 
 import javax.swing.text.Segment
 
-import scala.collection.JavaConverters
-
 import org.gjt.sp.jedit.{Mode, Buffer}
 import org.gjt.sp.jedit.syntax.{Token => JEditToken, TokenMarker, TokenHandler, DummyTokenHandler,
   ParserRuleSet, ModeProvider, XModeHandler}
 import org.gjt.sp.jedit.indent.IndentRule
 import org.gjt.sp.jedit.buffer.JEditBuffer
 
 
 object Token_Markup
 {
   /* line context */
 
   object Line_Context
   {
     def init(mode: String): Line_Context =
       new Line_Context(mode, Some(Scan.Finished), Line_Structure.init)
 
     def before(buffer: JEditBuffer, line: Int): Line_Context =
       if (line == 0) init(JEdit_Lib.buffer_mode(buffer))
       else after(buffer, line - 1)
 
     def after(buffer: JEditBuffer, line: Int): Line_Context =
     {
       val line_mgr = JEdit_Lib.buffer_line_manager(buffer)
       def context =
         line_mgr.getLineContext(line) match {
           case c: Line_Context => Some(c)
           case _ => None
         }
       context getOrElse {
         buffer.markTokens(line, DummyTokenHandler.INSTANCE)
         context getOrElse init(JEdit_Lib.buffer_mode(buffer))
       }
     }
   }
 
   class Line_Context(
       val mode: String,
       val context: Option[Scan.Line_Context],
       val structure: Line_Structure)
     extends TokenMarker.LineContext(new ParserRuleSet(mode, "MAIN"), null)
   {
     def get_context: Scan.Line_Context = context.getOrElse(Scan.Finished)
 
     override def hashCode: Int = (mode, context, structure).hashCode
     override def equals(that: Any): Boolean =
       that match {
         case other: Line_Context =>
           mode == other.mode && context == other.context && structure == other.structure
         case _ => false
       }
   }
 
 
   /* tokens from line (inclusive) */
 
   private def try_line_tokens(syntax: Outer_Syntax, buffer: JEditBuffer, line: Int)
     : Option[List[Token]] =
   {
     val line_context = Line_Context.before(buffer, line)
     for {
       ctxt <- line_context.context
       text <- JEdit_Lib.get_text(buffer, JEdit_Lib.line_range(buffer, line))
     } yield Token.explode_line(syntax.keywords, text, ctxt)._1
   }
 
   def line_token_iterator(
       syntax: Outer_Syntax,
       buffer: JEditBuffer,
       start_line: Int,
       end_line: Int): Iterator[Text.Info[Token]] =
     for {
       line <- Range(start_line max 0, end_line min buffer.getLineCount).iterator
       tokens <- try_line_tokens(syntax, buffer, line).iterator
       starts =
         tokens.iterator.scanLeft(buffer.getLineStartOffset(line))(
           (i, tok) => i + tok.source.length)
       (i, tok) <- starts zip tokens.iterator
     } yield Text.Info(Text.Range(i, i + tok.source.length), tok)
 
   def line_token_reverse_iterator(
       syntax: Outer_Syntax,
       buffer: JEditBuffer,
       start_line: Int,
       end_line: Int): Iterator[Text.Info[Token]] =
     for {
       line <- Range(start_line min (buffer.getLineCount - 1), end_line max -1, -1).iterator
       tokens <- try_line_tokens(syntax, buffer, line).iterator
       stops =
         tokens.reverseIterator.scanLeft(buffer.getLineEndOffset(line) min buffer.getLength)(
           (i, tok) => i - tok.source.length)
       (i, tok) <- stops zip tokens.reverseIterator
     } yield Text.Info(Text.Range(i - tok.source.length, i), tok)
 
 
   /* tokens from offset (inclusive) */
 
   def token_iterator(syntax: Outer_Syntax, buffer: JEditBuffer, offset: Text.Offset):
       Iterator[Text.Info[Token]] =
     if (JEdit_Lib.buffer_range(buffer).contains(offset))
       line_token_iterator(syntax, buffer, buffer.getLineOfOffset(offset), buffer.getLineCount).
         dropWhile(info => !info.range.contains(offset))
     else Iterator.empty
 
   def token_reverse_iterator(syntax: Outer_Syntax, buffer: JEditBuffer, offset: Text.Offset):
       Iterator[Text.Info[Token]] =
     if (JEdit_Lib.buffer_range(buffer).contains(offset))
       line_token_reverse_iterator(syntax, buffer, buffer.getLineOfOffset(offset), -1).
         dropWhile(info => !info.range.contains(offset))
     else Iterator.empty
 
 
   /* command spans */
 
   def command_span(syntax: Outer_Syntax, buffer: JEditBuffer, offset: Text.Offset)
     : Option[Text.Info[Command_Span.Span]] =
   {
     val keywords = syntax.keywords
 
     def maybe_command_start(i: Text.Offset): Option[Text.Info[Token]] =
       token_reverse_iterator(syntax, buffer, i).
         find(info => keywords.is_before_command(info.info) || info.info.is_command)
 
     def maybe_command_stop(i: Text.Offset): Option[Text.Info[Token]] =
       token_iterator(syntax, buffer, i).
         find(info => keywords.is_before_command(info.info) || info.info.is_command)
 
     if (JEdit_Lib.buffer_range(buffer).contains(offset)) {
       val start_info =
       {
         val info1 = maybe_command_start(offset)
         info1 match {
           case Some(Text.Info(range1, tok1)) if tok1.is_command =>
             val info2 = maybe_command_start(range1.start - 1)
             info2 match {
               case Some(Text.Info(_, tok2)) if keywords.is_before_command(tok2) => info2
               case _ => info1
             }
           case _ => info1
         }
       }
       val (start_before_command, start, start_next) =
         start_info match {
           case Some(Text.Info(range, tok)) =>
             (keywords.is_before_command(tok), range.start, range.stop)
           case None => (false, 0, 0)
         }
 
       val stop_info =
       {
         val info1 = maybe_command_stop(start_next)
         info1 match {
           case Some(Text.Info(range1, tok1)) if tok1.is_command && start_before_command =>
             maybe_command_stop(range1.stop)
           case _ => info1
         }
       }
       val stop =
         stop_info match {
           case Some(Text.Info(range, _)) => range.start
           case None => buffer.getLength
         }
 
       val text = JEdit_Lib.get_text(buffer, Text.Range(start, stop)).getOrElse("")
       val spans = syntax.parse_spans(text)
 
       (spans.iterator.scanLeft(start)(_ + _.length) zip spans.iterator).
         map({ case (i, span) => Text.Info(Text.Range(i, i + span.length), span) }).
         find(_.range.contains(offset))
     }
     else None
   }
 
   private def _command_span_iterator(
       syntax: Outer_Syntax,
       buffer: JEditBuffer,
       offset: Text.Offset,
       next_offset: Text.Range => Text.Offset): Iterator[Text.Info[Command_Span.Span]] =
     new Iterator[Text.Info[Command_Span.Span]]
     {
       private var next_span = command_span(syntax, buffer, offset)
       def hasNext: Boolean = next_span.isDefined
       def next(): Text.Info[Command_Span.Span] =
       {
         val span = next_span.getOrElse(Iterator.empty.next())
         next_span = command_span(syntax, buffer, next_offset(span.range))
         span
       }
     }
 
   def command_span_iterator(syntax: Outer_Syntax, buffer: JEditBuffer, offset: Text.Offset)
       : Iterator[Text.Info[Command_Span.Span]] =
     _command_span_iterator(syntax, buffer, offset max 0, range => range.stop)
 
   def command_span_reverse_iterator(syntax: Outer_Syntax, buffer: JEditBuffer, offset: Text.Offset)
       : Iterator[Text.Info[Command_Span.Span]] =
     _command_span_iterator(syntax, buffer,
       (offset min buffer.getLength) - 1, range => range.start - 1)
 
 
   /* token marker */
 
   class Marker(
     protected val mode: String,
     protected val opt_buffer: Option[Buffer]) extends TokenMarker
   {
     override def hashCode: Int = (mode, opt_buffer).hashCode
     override def equals(that: Any): Boolean =
       that match {
         case other: Marker => mode == other.mode && opt_buffer == other.opt_buffer
         case _ => false
       }
 
     override def toString: String =
       opt_buffer match {
         case None => "Marker(" + mode + ")"
         case Some(buffer) => "Marker(" + mode + "," + JEdit_Lib.buffer_name(buffer) + ")"
       }
 
     override def markTokens(context: TokenMarker.LineContext,
         handler: TokenHandler, raw_line: Segment): TokenMarker.LineContext =
     {
       val line = if (raw_line == null) new Segment else raw_line
       val line_context =
         context match { case c: Line_Context => c case _ => Line_Context.init(mode) }
       val structure = line_context.structure
 
       val context1 =
       {
         val opt_syntax =
           opt_buffer match {
             case Some(buffer) => Isabelle.buffer_syntax(buffer)
             case None => Isabelle.mode_syntax(mode)
           }
         val (styled_tokens, context1) =
           (line_context.context, opt_syntax) match {
             case (Some(ctxt), _) if mode == "isabelle-ml" || mode == "sml" =>
               val (tokens, ctxt1) = ML_Lex.tokenize_line(mode == "sml", line, ctxt)
               val styled_tokens =
                 tokens.map(tok => (JEdit_Rendering.ml_token_markup(tok), tok.source))
               (styled_tokens, new Line_Context(line_context.mode, Some(ctxt1), structure))
 
             case (Some(ctxt), Some(syntax)) if syntax.has_tokens =>
               val (tokens, ctxt1) = Token.explode_line(syntax.keywords, line, ctxt)
               val structure1 = structure.update(syntax.keywords, tokens)
               val styled_tokens =
                 tokens.map(tok => (JEdit_Rendering.token_markup(syntax, tok), tok.source))
               (styled_tokens, new Line_Context(line_context.mode, Some(ctxt1), structure1))
 
             case _ =>
               val styled_token = (JEditToken.NULL, line.subSequence(0, line.count).toString)
               (List(styled_token), new Line_Context(line_context.mode, None, structure))
           }
 
         val extended = Syntax_Style.extended(line)
         def special(i: Int): Boolean = extended.isDefinedAt(i) || line.charAt(i) == '\t'
 
         var offset = 0
         for ((style, token) <- styled_tokens) {
           val length = token.length
           if ((offset until (offset + length)).exists(special)) {
             for ((c, i) <- Codepoint.iterator_offset(token)) {
               val style1 =
                 extended.get(offset + i) match {
                   case None => style
                   case Some(ext) => ext(style)
                 }
               handler.handleToken(line, style1, offset + i, Character.charCount(c), context1)
             }
           }
           else handler.handleToken(line, style, offset, length, context1)
           offset += length
         }
         handler.handleToken(line, JEditToken.END, line.count, 0, context1)
         context1
       }
 
       val context2 = context1.intern
       handler.setLineContext(context2)
       context2
     }
   }
 
 
   /* mode provider */
 
   class Mode_Provider(orig_provider: ModeProvider) extends ModeProvider
   {
     for (mode <- orig_provider.getModes) addMode(mode)
 
     override def loadMode(mode: Mode, xmh: XModeHandler): Unit =
     {
       super.loadMode(mode, xmh)
       Isabelle.mode_token_marker(mode.getName).foreach(mode.setTokenMarker _)
       Isabelle.indent_rule(mode.getName).foreach(indent_rule =>
         Untyped.set[java.util.List[IndentRule]](
-          mode, "indentRules", JavaConverters.seqAsJavaList(List(indent_rule))))
+          mode, "indentRules", java.util.List.of(indent_rule)))
     }
   }
 }