src/Tools/VSCode/src/vscode_rendering.scala
author wenzelm
Thu Dec 22 11:08:58 2016 +0100 (2016-12-22)
changeset 64655 ea34f36ff6a5
parent 64654 31b681e38c70
child 64659 c64b258f6801
permissions -rw-r--r--
clarified message;
     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   private val hyperlink_elements =
    16     Markup.Elements(Markup.ENTITY, Markup.PATH, Markup.POSITION)
    17 }
    18 
    19 class VSCode_Rendering(
    20     val model: Document_Model,
    21     snapshot: Document.Snapshot,
    22     options: Options,
    23     resources: Resources)
    24   extends Rendering(snapshot, options, resources)
    25 {
    26   /* tooltips */
    27 
    28   def tooltip_margin: Int = options.int("vscode_tooltip_margin")
    29   def timing_threshold: Double = options.real("vscode_timing_threshold")
    30 
    31 
    32   /* hyperlinks */
    33 
    34   def hyperlinks(range: Text.Range): List[Line.Node_Range] =
    35   {
    36     snapshot.cumulate[List[Line.Node_Range]](
    37       range, Nil, VSCode_Rendering.hyperlink_elements, _ =>
    38         {
    39           case (links, Text.Info(_, XML.Elem(Markup.Path(name), _))) =>
    40             val file = resources.append_file_url(snapshot.node_name.master_dir, name)
    41             Some(Line.Node_Range(file) :: links)
    42 
    43 /* FIXME
    44           case (links, Text.Info(info_range, XML.Elem(Markup(Markup.ENTITY, props), _)))
    45           if !props.exists(
    46             { case (Markup.KIND, Markup.ML_OPEN) => true
    47               case (Markup.KIND, Markup.ML_STRUCTURE) => true
    48               case _ => false }) =>
    49             val opt_link = PIDE.editor.hyperlink_def_position(true, snapshot, props)
    50             opt_link.map(_ :: links)
    51 
    52           case (links, Text.Info(info_range, XML.Elem(Markup(Markup.POSITION, props), _))) =>
    53             val opt_link = PIDE.editor.hyperlink_position(true, snapshot, props)
    54             opt_link.map(_ :: links)
    55 */
    56 
    57           case _ => None
    58         }) match { case Text.Info(_, links) :: _ => links.reverse case _ => Nil }
    59   }
    60 }