src/Tools/VSCode/src/vscode_rendering.scala
author wenzelm
Wed Dec 21 22:52:07 2016 +0100 (2016-12-21)
changeset 64652 ad55f164ae0d
parent 64651 ea5620f7b0d8
child 64654 31b681e38c70
permissions -rw-r--r--
VSCode already detects URLs from plain text;
wenzelm@64622
     1
/*  Title:      Tools/VSCode/src/vscode_rendering.scala
wenzelm@64622
     2
    Author:     Makarius
wenzelm@64622
     3
wenzelm@64622
     4
Isabelle/VSCode-specific implementation of quasi-abstract rendering and
wenzelm@64622
     5
markup interpretation.
wenzelm@64622
     6
*/
wenzelm@64622
     7
wenzelm@64622
     8
package isabelle.vscode
wenzelm@64622
     9
wenzelm@64622
    10
wenzelm@64622
    11
import isabelle._
wenzelm@64622
    12
wenzelm@64648
    13
object VSCode_Rendering
wenzelm@64648
    14
{
wenzelm@64648
    15
  private val hyperlink_elements =
wenzelm@64652
    16
    Markup.Elements(Markup.ENTITY, Markup.PATH, Markup.POSITION)
wenzelm@64648
    17
}
wenzelm@64622
    18
wenzelm@64649
    19
class VSCode_Rendering(
wenzelm@64649
    20
    val model: Document_Model,
wenzelm@64649
    21
    snapshot: Document.Snapshot,
wenzelm@64649
    22
    options: Options,
wenzelm@64649
    23
    resources: Resources)
wenzelm@64622
    24
  extends Rendering(snapshot, options, resources)
wenzelm@64622
    25
{
wenzelm@64622
    26
  /* tooltips */
wenzelm@64622
    27
wenzelm@64622
    28
  def tooltip_margin: Int = options.int("vscode_tooltip_margin")
wenzelm@64622
    29
  def timing_threshold: Double = options.real("vscode_timing_threshold")
wenzelm@64648
    30
wenzelm@64648
    31
wenzelm@64648
    32
  /* hyperlinks */
wenzelm@64648
    33
wenzelm@64651
    34
  def hyperlinks(range: Text.Range): List[Line.Node_Range] =
wenzelm@64648
    35
  {
wenzelm@64651
    36
    snapshot.cumulate[List[Line.Node_Range]](
wenzelm@64648
    37
      range, Nil, VSCode_Rendering.hyperlink_elements, _ =>
wenzelm@64648
    38
        {
wenzelm@64648
    39
          case (links, Text.Info(_, XML.Elem(Markup.Path(name), _))) =>
wenzelm@64651
    40
            Some(Line.Node_Range(resolve_file_url(name)) :: links)
wenzelm@64648
    41
wenzelm@64648
    42
/* FIXME
wenzelm@64648
    43
          case (links, Text.Info(info_range, XML.Elem(Markup(Markup.ENTITY, props), _)))
wenzelm@64648
    44
          if !props.exists(
wenzelm@64648
    45
            { case (Markup.KIND, Markup.ML_OPEN) => true
wenzelm@64648
    46
              case (Markup.KIND, Markup.ML_STRUCTURE) => true
wenzelm@64648
    47
              case _ => false }) =>
wenzelm@64648
    48
            val opt_link = PIDE.editor.hyperlink_def_position(true, snapshot, props)
wenzelm@64648
    49
            opt_link.map(_ :: links)
wenzelm@64648
    50
wenzelm@64648
    51
          case (links, Text.Info(info_range, XML.Elem(Markup(Markup.POSITION, props), _))) =>
wenzelm@64648
    52
            val opt_link = PIDE.editor.hyperlink_position(true, snapshot, props)
wenzelm@64648
    53
            opt_link.map(_ :: links)
wenzelm@64648
    54
*/
wenzelm@64648
    55
wenzelm@64648
    56
          case _ => None
wenzelm@64648
    57
        }) match { case Text.Info(_, links) :: _ => links.reverse case _ => Nil }
wenzelm@64648
    58
  }
wenzelm@64622
    59
}