src/Tools/VSCode/src/vscode_rendering.scala
author wenzelm
Mon Mar 11 18:58:06 2019 +0100 (2 months ago ago)
changeset 70079 990c6e8faf2c
parent 69261 c78c95d2a3d1
permissions -rw-r--r--
tuned signature;
     1 /*  Title:      Tools/VSCode/src/vscode_rendering.scala
     2     Author:     Makarius
     3 
     4 Isabelle/VSCode-specific implementation of quasi-abstract rendering and
     5 markup interpretation.
     6 */
     7 
     8 package isabelle.vscode
     9 
    10 
    11 import isabelle._
    12 
    13 import java.io.{File => JFile}
    14 
    15 import scala.annotation.tailrec
    16 
    17 
    18 object VSCode_Rendering
    19 {
    20   /* decorations */
    21 
    22   private def color_decorations(prefix: String, types: Set[Rendering.Color.Value],
    23     colors: List[Text.Info[Rendering.Color.Value]]): List[Document_Model.Decoration] =
    24   {
    25     val color_ranges =
    26       (Map.empty[Rendering.Color.Value, List[Text.Range]] /: colors) {
    27         case (m, Text.Info(range, c)) => m + (c -> (range :: m.getOrElse(c, Nil)))
    28       }
    29     types.toList.map(c =>
    30       Document_Model.Decoration.ranges(prefix + c.toString, color_ranges.getOrElse(c, Nil).reverse))
    31   }
    32 
    33   private val background_colors =
    34     Rendering.Color.background_colors - Rendering.Color.active - Rendering.Color.active_result -
    35       Rendering.Color.entity
    36 
    37   private val dotted_colors =
    38     Set(Rendering.Color.writeln, Rendering.Color.information, Rendering.Color.warning)
    39 
    40 
    41   /* diagnostic messages */
    42 
    43   private val message_severity =
    44     Map(
    45       Markup.LEGACY -> Protocol.DiagnosticSeverity.Warning,
    46       Markup.ERROR -> Protocol.DiagnosticSeverity.Error)
    47 
    48 
    49   /* markup elements */
    50 
    51   private val diagnostics_elements =
    52     Markup.Elements(Markup.LEGACY, Markup.ERROR)
    53 
    54   private val background_elements =
    55     Rendering.background_elements - Markup.ENTITY -- Rendering.active_elements
    56 
    57   private val dotted_elements =
    58     Markup.Elements(Markup.WRITELN, Markup.INFORMATION, Markup.WARNING)
    59 
    60   val tooltip_elements =
    61     Markup.Elements(Markup.WRITELN, Markup.INFORMATION, Markup.WARNING, Markup.BAD) ++
    62     Rendering.tooltip_elements
    63 
    64   private val hyperlink_elements =
    65     Markup.Elements(Markup.ENTITY, Markup.PATH, Markup.POSITION, Markup.CITATION)
    66 }
    67 
    68 class VSCode_Rendering(snapshot: Document.Snapshot, _model: Document_Model)
    69   extends Rendering(snapshot, _model.resources.options, _model.session)
    70 {
    71   rendering =>
    72 
    73   def model: Document_Model = _model
    74   def resources: VSCode_Resources = model.resources
    75 
    76 
    77   /* bibtex */
    78 
    79   def bibtex_entries_iterator(): Iterator[Text.Info[(String, Document_Model)]] =
    80     Bibtex.entries_iterator(resources.get_models)
    81 
    82   def bibtex_completion(history: Completion.History, caret: Text.Offset): Option[Completion.Result] =
    83     Bibtex.completion(history, rendering, caret, resources.get_models)
    84 
    85 
    86   /* completion */
    87 
    88   def completion(caret_pos: Line.Position, caret: Text.Offset): List[Protocol.CompletionItem] =
    89   {
    90     val doc = model.content.doc
    91     val line = caret_pos.line
    92     doc.offset(Line.Position(line)) match {
    93       case None => Nil
    94       case Some(line_start) =>
    95         val history = Completion.History.empty
    96         val caret_range = before_caret_range(caret)
    97 
    98         val syntax = model.syntax()
    99         val syntax_completion =
   100           syntax.complete(history, unicode = false, explicit = true,
   101             line_start, doc.lines(line).text, caret - line_start,
   102             language_context(caret_range) getOrElse syntax.language_context)
   103 
   104         val (no_completion, semantic_completion) =
   105           rendering.semantic_completion_result(
   106             history, false, syntax_completion.map(_.range), caret_range)
   107 
   108         if (no_completion) Nil
   109         else {
   110           val results =
   111             Completion.Result.merge(history,
   112               semantic_completion,
   113               syntax_completion,
   114               VSCode_Spell_Checker.completion(rendering, caret),
   115               path_completion(caret),
   116               bibtex_completion(history, caret))
   117           val items =
   118             results match {
   119               case None => Nil
   120               case Some(result) =>
   121                 result.items.map(item =>
   122                   Protocol.CompletionItem(
   123                     label = item.replacement,
   124                     detail = Some(item.description.mkString(" ")),
   125                     range = Some(doc.range(item.range))))
   126             }
   127           items ::: VSCode_Spell_Checker.menu_items(rendering, caret)
   128         }
   129     }
   130   }
   131 
   132 
   133   /* diagnostics */
   134 
   135   def diagnostics: List[Text.Info[Command.Results]] =
   136     snapshot.cumulate[Command.Results](
   137       model.content.text_range, Command.Results.empty, VSCode_Rendering.diagnostics_elements,
   138         command_states =>
   139           {
   140             case (res, Text.Info(_, msg @ XML.Elem(Markup(Markup.BAD, Markup.Serial(i)), body)))
   141             if body.nonEmpty => Some(res + (i -> msg))
   142 
   143             case (res, Text.Info(_, msg)) =>
   144               Command.State.get_result_proper(command_states, msg.markup.properties).map(res + _)
   145 
   146             case _ => None
   147           }).filterNot(info => info.info.is_empty)
   148 
   149   def diagnostics_output(results: List[Text.Info[Command.Results]]): List[Protocol.Diagnostic] =
   150   {
   151     (for {
   152       Text.Info(text_range, res) <- results.iterator
   153       range = model.content.doc.range(text_range)
   154       (_, XML.Elem(Markup(name, _), body)) <- res.iterator
   155     } yield {
   156       val message = resources.output_pretty_message(body)
   157       val severity = VSCode_Rendering.message_severity.get(name)
   158       Protocol.Diagnostic(range, message, severity = severity)
   159     }).toList
   160   }
   161 
   162 
   163   /* text color */
   164 
   165   def text_color(range: Text.Range): List[Text.Info[Rendering.Color.Value]] =
   166   {
   167     snapshot.select(range, Rendering.text_color_elements, _ =>
   168       {
   169         case Text.Info(_, XML.Elem(Markup(name, props), _)) =>
   170           if (name != Markup.IMPROPER && props.contains((Markup.KIND, Markup.COMMAND))) None
   171           else Rendering.text_color.get(name)
   172       })
   173   }
   174 
   175 
   176   /* text overview color */
   177 
   178   private sealed case class Color_Info(
   179     color: Rendering.Color.Value, offset: Text.Offset, end_offset: Text.Offset, end_line: Int)
   180 
   181   def text_overview_color: List[Text.Info[Rendering.Color.Value]] =
   182   {
   183     @tailrec def loop(offset: Text.Offset, line: Int, lines: List[Line], colors: List[Color_Info])
   184       : List[Text.Info[Rendering.Color.Value]] =
   185     {
   186       if (lines.nonEmpty) {
   187         val end_offset = offset + lines.head.text.length
   188         val colors1 =
   189           (overview_color(Text.Range(offset, end_offset)), colors) match {
   190             case (Some(color), old :: rest) if color == old.color && line == old.end_line =>
   191               old.copy(end_offset = end_offset, end_line = line + 1) :: rest
   192             case (Some(color), _) =>
   193               Color_Info(color, offset, end_offset, line + 1) :: colors
   194             case (None, _) => colors
   195           }
   196         loop(end_offset + 1, line + 1, lines.tail, colors1)
   197       }
   198       else {
   199         colors.reverse.map(info =>
   200           Text.Info(Text.Range(info.offset, info.end_offset), info.color))
   201       }
   202     }
   203     loop(0, 0, model.content.doc.lines, Nil)
   204   }
   205 
   206 
   207   /* dotted underline */
   208 
   209   def dotted(range: Text.Range): List[Text.Info[Rendering.Color.Value]] =
   210     message_underline_color(VSCode_Rendering.dotted_elements, range)
   211 
   212 
   213   /* decorations */
   214 
   215   def decorations: List[Document_Model.Decoration] = // list of canonical length and order
   216     Par_List.map((f: () => List[Document_Model.Decoration]) => f(),
   217       List(
   218         () =>
   219           VSCode_Rendering.color_decorations("background_", VSCode_Rendering.background_colors,
   220             background(VSCode_Rendering.background_elements, model.content.text_range, Set.empty)),
   221         () =>
   222           VSCode_Rendering.color_decorations("foreground_", Rendering.Color.foreground_colors,
   223             foreground(model.content.text_range)),
   224         () =>
   225           VSCode_Rendering.color_decorations("text_", Rendering.Color.text_colors,
   226             text_color(model.content.text_range)),
   227         () =>
   228           VSCode_Rendering.color_decorations("text_overview_", Rendering.Color.text_overview_colors,
   229             text_overview_color),
   230         () =>
   231           VSCode_Rendering.color_decorations("dotted_", VSCode_Rendering.dotted_colors,
   232             dotted(model.content.text_range)))).flatten :::
   233     List(VSCode_Spell_Checker.decoration(rendering))
   234 
   235   def decoration_output(decoration: Document_Model.Decoration): Protocol.Decoration =
   236   {
   237     val content =
   238       for (Text.Info(text_range, msgs) <- decoration.content)
   239       yield {
   240         val range = model.content.doc.range(text_range)
   241         Protocol.DecorationOpts(range,
   242           msgs.map(msg => Protocol.MarkedString(resources.output_pretty_tooltip(msg))))
   243       }
   244     Protocol.Decoration(decoration.typ, content)
   245   }
   246 
   247 
   248   /* tooltips */
   249 
   250   override def timing_threshold: Double = options.real("vscode_timing_threshold")
   251 
   252 
   253   /* hyperlinks */
   254 
   255   def hyperlink_source_file(source_name: String, line1: Int, range: Symbol.Range)
   256     : Option[Line.Node_Range] =
   257   {
   258     for {
   259       platform_path <- resources.source_file(source_name)
   260       file <-
   261         (try { Some(File.absolute(new JFile(platform_path))) }
   262          catch { case ERROR(_) => None })
   263     }
   264     yield {
   265       Line.Node_Range(file.getPath,
   266         if (range.start > 0) {
   267           resources.get_file_content(resources.node_name(file)) match {
   268             case Some(text) =>
   269               val chunk = Symbol.Text_Chunk(text)
   270               val doc = Line.Document(text)
   271               doc.range(chunk.decode(range))
   272             case _ =>
   273               Line.Range(Line.Position((line1 - 1) max 0))
   274           }
   275         }
   276         else Line.Range(Line.Position((line1 - 1) max 0)))
   277     }
   278   }
   279 
   280   def hyperlink_command(id: Document_ID.Generic, range: Symbol.Range): Option[Line.Node_Range] =
   281   {
   282     if (snapshot.is_outdated) None
   283     else
   284       for {
   285         start <- snapshot.find_command_position(id, range.start)
   286         stop <- snapshot.find_command_position(id, range.stop)
   287       } yield Line.Node_Range(start.name, Line.Range(start.pos, stop.pos))
   288   }
   289 
   290   def hyperlink_position(pos: Position.T): Option[Line.Node_Range] =
   291     pos match {
   292       case Position.Item_File(name, line, range) => hyperlink_source_file(name, line, range)
   293       case Position.Item_Id(id, range) => hyperlink_command(id, range)
   294       case _ => None
   295     }
   296 
   297   def hyperlink_def_position(pos: Position.T): Option[Line.Node_Range] =
   298     pos match {
   299       case Position.Item_Def_File(name, line, range) => hyperlink_source_file(name, line, range)
   300       case Position.Item_Def_Id(id, range) => hyperlink_command(id, range)
   301       case _ => None
   302     }
   303 
   304   def hyperlinks(range: Text.Range): List[Line.Node_Range] =
   305   {
   306     snapshot.cumulate[List[Line.Node_Range]](
   307       range, Nil, VSCode_Rendering.hyperlink_elements, _ =>
   308         {
   309           case (links, Text.Info(_, XML.Elem(Markup.Path(name), _))) =>
   310             val file = perhaps_append_file(snapshot.node_name, name)
   311             Some(Line.Node_Range(file) :: links)
   312 
   313           case (links, Text.Info(info_range, XML.Elem(Markup(Markup.ENTITY, props), _))) =>
   314             hyperlink_def_position(props).map(_ :: links)
   315 
   316           case (links, Text.Info(info_range, XML.Elem(Markup(Markup.POSITION, props), _))) =>
   317             hyperlink_position(props).map(_ :: links)
   318 
   319           case (links, Text.Info(info_range, XML.Elem(Markup.Citation(name), _))) =>
   320             val iterator =
   321               for {
   322                 Text.Info(entry_range, (entry, model)) <- bibtex_entries_iterator()
   323                 if entry == name
   324               } yield Line.Node_Range(model.node_name.node, model.content.doc.range(entry_range))
   325             if (iterator.isEmpty) None else Some((links /: iterator)(_ :+ _))
   326 
   327           case _ => None
   328         }) match { case Text.Info(_, links) :: _ => links.reverse case _ => Nil }
   329   }
   330 }