src/Tools/VSCode/src/vscode_rendering.scala
author wenzelm
Wed Dec 21 21:18:37 2016 +0100 (2016-12-21)
changeset 64648 5d7f741aaccb
parent 64622 529bbb8977c7
child 64649 d67c3094a0c2
permissions -rw-r--r--
basic support for hyperlinks / Goto Definition Request;
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@64648
    16
    Markup.Elements(Markup.ENTITY, Markup.PATH, Markup.POSITION, Markup.URL)
wenzelm@64648
    17
}
wenzelm@64622
    18
wenzelm@64622
    19
class VSCode_Rendering(snapshot: Document.Snapshot, options: Options, resources: Resources)
wenzelm@64622
    20
  extends Rendering(snapshot, options, resources)
wenzelm@64622
    21
{
wenzelm@64622
    22
  /* tooltips */
wenzelm@64622
    23
wenzelm@64622
    24
  def tooltip_margin: Int = options.int("vscode_tooltip_margin")
wenzelm@64622
    25
  def timing_threshold: Double = options.real("vscode_timing_threshold")
wenzelm@64648
    26
wenzelm@64648
    27
wenzelm@64648
    28
  /* hyperlinks */
wenzelm@64648
    29
wenzelm@64648
    30
  def hyperlinks(range: Text.Range): List[(String, Line.Range)] =
wenzelm@64648
    31
  {
wenzelm@64648
    32
    snapshot.cumulate[List[(String, Line.Range)]](
wenzelm@64648
    33
      range, Nil, VSCode_Rendering.hyperlink_elements, _ =>
wenzelm@64648
    34
        {
wenzelm@64648
    35
          case (links, Text.Info(_, XML.Elem(Markup.Path(name), _))) =>
wenzelm@64648
    36
            Some((resolve_file_url(name), Line.Range.zero) :: links)
wenzelm@64648
    37
wenzelm@64648
    38
/* FIXME
wenzelm@64648
    39
          case (links, Text.Info(_, XML.Elem(Markup.Url(name), _))) =>
wenzelm@64648
    40
            Some(PIDE.editor.hyperlink_url(name) :: links)
wenzelm@64648
    41
wenzelm@64648
    42
          case (links, Text.Info(info_range, XML.Elem(Markup(Markup.ENTITY, props), _)))
wenzelm@64648
    43
          if !props.exists(
wenzelm@64648
    44
            { case (Markup.KIND, Markup.ML_OPEN) => true
wenzelm@64648
    45
              case (Markup.KIND, Markup.ML_STRUCTURE) => true
wenzelm@64648
    46
              case _ => false }) =>
wenzelm@64648
    47
            val opt_link = PIDE.editor.hyperlink_def_position(true, snapshot, props)
wenzelm@64648
    48
            opt_link.map(_ :: links)
wenzelm@64648
    49
wenzelm@64648
    50
          case (links, Text.Info(info_range, XML.Elem(Markup(Markup.POSITION, props), _))) =>
wenzelm@64648
    51
            val opt_link = PIDE.editor.hyperlink_position(true, snapshot, props)
wenzelm@64648
    52
            opt_link.map(_ :: links)
wenzelm@64648
    53
*/
wenzelm@64648
    54
wenzelm@64648
    55
          case _ => None
wenzelm@64648
    56
        }) match { case Text.Info(_, links) :: _ => links.reverse case _ => Nil }
wenzelm@64648
    57
  }
wenzelm@64622
    58
}