src/Tools/VSCode/src/vscode_rendering.scala

 import java.io.{File => JFile}
 
 import scala.annotation.tailrec
 
 
-object VSCode_Rendering
-{
+object VSCode_Rendering {
   /* decorations */
 
-  private def color_decorations(prefix: String, types: Set[Rendering.Color.Value],
-    colors: List[Text.Info[Rendering.Color.Value]]): List[VSCode_Model.Decoration] =
-  {
+  private def color_decorations(
+    prefix: String,
+    types: Set[Rendering.Color.Value],
+    colors: List[Text.Info[Rendering.Color.Value]]
+  ): List[VSCode_Model.Decoration] = {
     val color_ranges =
       colors.foldLeft(Map.empty[Rendering.Color.Value, List[Text.Range]]) {
         case (m, Text.Info(range, c)) => m + (c -> (range :: m.getOrElse(c, Nil)))
       }
     types.toList.map(c =>

   private val hyperlink_elements =
     Markup.Elements(Markup.ENTITY, Markup.PATH, Markup.POSITION, Markup.CITATION)
 }
 
 class VSCode_Rendering(snapshot: Document.Snapshot, val model: VSCode_Model)
-  extends Rendering(snapshot, model.resources.options, model.session)
-{
+extends Rendering(snapshot, model.resources.options, model.session) {
   rendering =>
 
   def resources: VSCode_Resources = model.resources
 
   override def get_text(range: Text.Range): Option[String] = model.get_text(range)

     Bibtex.completion(history, rendering, caret, resources.get_models)
 
 
   /* completion */
 
-  def completion(node_pos: Line.Node_Position, caret: Text.Offset): List[LSP.CompletionItem] =
-  {
+  def completion(node_pos: Line.Node_Position, caret: Text.Offset): List[LSP.CompletionItem] = {
     val doc = model.content.doc
     val line = node_pos.pos.line
     val unicode = node_pos.name.endsWith(".thy")
     doc.offset(Line.Position(line)) match {
       case None => Nil

               Command.State.get_result_proper(command_states, msg.markup.properties).map(res + _)
 
             case _ => None
           }).filterNot(info => info.info.is_empty)
 
-  def diagnostics_output(results: List[Text.Info[Command.Results]]): List[LSP.Diagnostic] =
-  {
+  def diagnostics_output(results: List[Text.Info[Command.Results]]): List[LSP.Diagnostic] = {
     (for {
       Text.Info(text_range, res) <- results.iterator
       range = model.content.doc.range(text_range)
       (_, XML.Elem(Markup(name, _), body)) <- res.iterator
     } yield {

   }
 
 
   /* text color */
 
-  def text_color(range: Text.Range): List[Text.Info[Rendering.Color.Value]] =
-  {
+  def text_color(range: Text.Range): List[Text.Info[Rendering.Color.Value]] = {
     snapshot.select(range, Rendering.text_color_elements, _ =>
       {
         case Text.Info(_, XML.Elem(Markup(name, props), _)) =>
           if (name != Markup.IMPROPER && props.contains((Markup.KIND, Markup.COMMAND))) None
           else Rendering.text_color.get(name)

   /* text overview color */
 
   private sealed case class Color_Info(
     color: Rendering.Color.Value, offset: Text.Offset, end_offset: Text.Offset, end_line: Int)
 
-  def text_overview_color: List[Text.Info[Rendering.Color.Value]] =
-  {
-    @tailrec def loop(offset: Text.Offset, line: Int, lines: List[Line], colors: List[Color_Info])
-      : List[Text.Info[Rendering.Color.Value]] =
-    {
+  def text_overview_color: List[Text.Info[Rendering.Color.Value]] = {
+    @tailrec def loop(
+      offset: Text.Offset,
+      line: Int,
+      lines: List[Line],
+      colors: List[Color_Info]
+    ): List[Text.Info[Rendering.Color.Value]] = {
       if (lines.nonEmpty) {
         val end_offset = offset + lines.head.text.length
         val colors1 =
           (overview_color(Text.Range(offset, end_offset)), colors) match {
             case (Some(color), old :: rest) if color == old.color && line == old.end_line =>

         () =>
           VSCode_Rendering.color_decorations("dotted_", VSCode_Rendering.dotted_colors,
             dotted(model.content.text_range)))).flatten :::
     List(VSCode_Spell_Checker.decoration(rendering))
 
-  def decoration_output(decoration: List[VSCode_Model.Decoration]): LSP.Decoration =
-  {
+  def decoration_output(decoration: List[VSCode_Model.Decoration]): LSP.Decoration = {
     val entries =
       for (deco <- decoration)
       yield {
         val decopts = for(Text.Info(text_range, msgs) <- deco.content)
           yield {

   override def timing_threshold: Double = options.real("vscode_timing_threshold")
 
 
   /* hyperlinks */
 
-  def hyperlink_source_file(source_name: String, line1: Int, range: Symbol.Range)
-    : Option[Line.Node_Range] =
-  {
+  def hyperlink_source_file(
+    source_name: String,
+    line1: Int,
+    range: Symbol.Range
+  ): Option[Line.Node_Range] = {
     for {
       platform_path <- resources.source_file(source_name)
       file <-
         (try { Some(File.absolute(new JFile(platform_path))) }
          catch { case ERROR(_) => None })

         }
         else Line.Range(Line.Position((line1 - 1) max 0)))
     }
   }
 
-  def hyperlink_command(id: Document_ID.Generic, range: Symbol.Range): Option[Line.Node_Range] =
-  {
+  def hyperlink_command(id: Document_ID.Generic, range: Symbol.Range): Option[Line.Node_Range] = {
     if (snapshot.is_outdated) None
     else
       for {
         start <- snapshot.find_command_position(id, range.start)
         stop <- snapshot.find_command_position(id, range.stop)

       case Position.Item_Def_File(name, line, range) => hyperlink_source_file(name, line, range)
       case Position.Item_Def_Id(id, range) => hyperlink_command(id, range)
       case _ => None
     }
 
-  def hyperlinks(range: Text.Range): List[Line.Node_Range] =
-  {
+  def hyperlinks(range: Text.Range): List[Line.Node_Range] = {
     snapshot.cumulate[List[Line.Node_Range]](
       range, Nil, VSCode_Rendering.hyperlink_elements, _ =>
         {
           case (links, Text.Info(_, XML.Elem(Markup.Path(name), _))) =>
             val file = perhaps_append_file(snapshot.node_name, name)