src/Tools/VSCode/src/vscode_rendering.scala
author wenzelm
Tue Jan 03 14:17:03 2017 +0100 (2017-01-03)
changeset 64759 100941134718
parent 64730 76996d915894
child 64762 cd545bec3fd0
permissions -rw-r--r--
clarified master_dir: file-URL;
     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 object VSCode_Rendering
    14 {
    15   /* diagnostic messages */
    16 
    17   private val message_severity =
    18     Map(
    19       Markup.WRITELN -> Protocol.DiagnosticSeverity.Hint,
    20       Markup.INFORMATION -> Protocol.DiagnosticSeverity.Information,
    21       Markup.WARNING -> Protocol.DiagnosticSeverity.Warning,
    22       Markup.LEGACY -> Protocol.DiagnosticSeverity.Warning,
    23       Markup.ERROR -> Protocol.DiagnosticSeverity.Error,
    24       Markup.BAD -> Protocol.DiagnosticSeverity.Error)
    25 
    26 
    27   /* markup elements */
    28 
    29   private val diagnostics_elements =
    30     Markup.Elements(Markup.WRITELN, Markup.INFORMATION, Markup.WARNING, Markup.LEGACY, Markup.ERROR,
    31       Markup.BAD)
    32 
    33   private val hyperlink_elements =
    34     Markup.Elements(Markup.ENTITY, Markup.PATH, Markup.POSITION)
    35 }
    36 
    37 class VSCode_Rendering(
    38     val model: Document_Model,
    39     snapshot: Document.Snapshot,
    40     resources: VSCode_Resources)
    41   extends Rendering(snapshot, resources.options, resources)
    42 {
    43   /* diagnostics */
    44 
    45   def diagnostics: List[Text.Info[Command.Results]] =
    46     snapshot.cumulate[Command.Results](
    47       model.doc.full_range, Command.Results.empty, VSCode_Rendering.diagnostics_elements, _ =>
    48       {
    49         case (res, Text.Info(_, msg @ XML.Elem(Markup(_, Markup.Serial(i)), body)))
    50         if body.nonEmpty => Some(res + (i -> msg))
    51 
    52         case _ => None
    53       })
    54 
    55   val diagnostics_margin = options.int("vscode_diagnostics_margin")
    56 
    57   def diagnostics_output(results: List[Text.Info[Command.Results]]): List[Protocol.Diagnostic] =
    58   {
    59     (for {
    60       Text.Info(text_range, res) <- results.iterator
    61       range = model.doc.range(text_range)
    62       (_, XML.Elem(Markup(name, _), body)) <- res.iterator
    63     } yield {
    64       val message = Pretty.string_of(body, margin = diagnostics_margin)
    65       val severity = VSCode_Rendering.message_severity.get(name)
    66       Protocol.Diagnostic(range, message, severity = severity)
    67     }).toList
    68   }
    69 
    70 
    71   /* tooltips */
    72 
    73   def tooltip_margin: Int = options.int("vscode_tooltip_margin")
    74   def timing_threshold: Double = options.real("vscode_timing_threshold")
    75 
    76 
    77   /* hyperlinks */
    78 
    79   def hyperlink_source_file(source_name: String, line1: Int, range: Symbol.Range)
    80     : Option[Line.Node_Range] =
    81   {
    82     for (name <- resources.source_file(source_name))
    83     yield {
    84       val opt_text =
    85         try { Some(File.read(Path.explode(name))) } // FIXME content from resources/models
    86         catch { case ERROR(_) => None }
    87       Line.Node_Range(Url.platform_file(name),
    88         opt_text match {
    89           case Some(text) if range.start > 0 =>
    90             val chunk = Symbol.Text_Chunk(text)
    91             val doc = Line.Document(text, resources.text_length)
    92             doc.range(chunk.decode(range))
    93           case _ =>
    94             Line.Range(Line.Position((line1 - 1) max 0))
    95         })
    96     }
    97   }
    98 
    99   def hyperlink_command(id: Document_ID.Generic, range: Symbol.Range): Option[Line.Node_Range] =
   100   {
   101     if (snapshot.is_outdated) None
   102     else
   103       for {
   104         start <- snapshot.find_command_position(id, range.start)
   105         stop <- snapshot.find_command_position(id, range.stop)
   106       } yield Line.Node_Range(start.name, Line.Range(start.pos, stop.pos))
   107   }
   108 
   109   def hyperlink_position(pos: Position.T): Option[Line.Node_Range] =
   110     pos match {
   111       case Position.Item_File(name, line, range) => hyperlink_source_file(name, line, range)
   112       case Position.Item_Id(id, range) => hyperlink_command(id, range)
   113       case _ => None
   114     }
   115 
   116   def hyperlink_def_position(pos: Position.T): Option[Line.Node_Range] =
   117     pos match {
   118       case Position.Item_Def_File(name, line, range) => hyperlink_source_file(name, line, range)
   119       case Position.Item_Def_Id(id, range) => hyperlink_command(id, range)
   120       case _ => None
   121     }
   122 
   123   def hyperlinks(range: Text.Range): List[Line.Node_Range] =
   124   {
   125     snapshot.cumulate[List[Line.Node_Range]](
   126       range, Nil, VSCode_Rendering.hyperlink_elements, _ =>
   127         {
   128           case (links, Text.Info(_, XML.Elem(Markup.Path(name), _))) =>
   129             val file = resources.append_file(snapshot.node_name.master_dir, name)
   130             Some(Line.Node_Range(file) :: links)
   131 
   132           case (links, Text.Info(info_range, XML.Elem(Markup(Markup.ENTITY, props), _))) =>
   133             hyperlink_def_position(props).map(_ :: links)
   134 
   135           case (links, Text.Info(info_range, XML.Elem(Markup(Markup.POSITION, props), _))) =>
   136             hyperlink_position(props).map(_ :: links)
   137 
   138           case _ => None
   139         }) match { case Text.Info(_, links) :: _ => links.reverse case _ => Nil }
   140   }
   141 }