src/Tools/VSCode/src/vscode_rendering.scala
author wenzelm
Wed, 21 Dec 2016 21:18:37 +0100
changeset 64648 5d7f741aaccb
parent 64622 529bbb8977c7
child 64649 d67c3094a0c2
permissions -rw-r--r--
basic support for hyperlinks / Goto Definition Request;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
64622
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
     1
/*  Title:      Tools/VSCode/src/vscode_rendering.scala
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
     3
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
     4
Isabelle/VSCode-specific implementation of quasi-abstract rendering and
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
     5
markup interpretation.
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
     6
*/
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
     7
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
     8
package isabelle.vscode
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
     9
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
    10
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
    11
import isabelle._
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
    12
64648
5d7f741aaccb basic support for hyperlinks / Goto Definition Request;
wenzelm
parents: 64622
diff changeset
    13
object VSCode_Rendering
5d7f741aaccb basic support for hyperlinks / Goto Definition Request;
wenzelm
parents: 64622
diff changeset
    14
{
5d7f741aaccb basic support for hyperlinks / Goto Definition Request;
wenzelm
parents: 64622
diff changeset
    15
  private val hyperlink_elements =
5d7f741aaccb basic support for hyperlinks / Goto Definition Request;
wenzelm
parents: 64622
diff changeset
    16
    Markup.Elements(Markup.ENTITY, Markup.PATH, Markup.POSITION, Markup.URL)
5d7f741aaccb basic support for hyperlinks / Goto Definition Request;
wenzelm
parents: 64622
diff changeset
    17
}
64622
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
    18
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
    19
class VSCode_Rendering(snapshot: Document.Snapshot, options: Options, resources: Resources)
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
    20
  extends Rendering(snapshot, options, resources)
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
    21
{
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
    22
  /* tooltips */
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
    23
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
    24
  def tooltip_margin: Int = options.int("vscode_tooltip_margin")
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
    25
  def timing_threshold: Double = options.real("vscode_timing_threshold")
64648
5d7f741aaccb basic support for hyperlinks / Goto Definition Request;
wenzelm
parents: 64622
diff changeset
    26
5d7f741aaccb basic support for hyperlinks / Goto Definition Request;
wenzelm
parents: 64622
diff changeset
    27
5d7f741aaccb basic support for hyperlinks / Goto Definition Request;
wenzelm
parents: 64622
diff changeset
    28
  /* hyperlinks */
5d7f741aaccb basic support for hyperlinks / Goto Definition Request;
wenzelm
parents: 64622
diff changeset
    29
5d7f741aaccb basic support for hyperlinks / Goto Definition Request;
wenzelm
parents: 64622
diff changeset
    30
  def hyperlinks(range: Text.Range): List[(String, Line.Range)] =
5d7f741aaccb basic support for hyperlinks / Goto Definition Request;
wenzelm
parents: 64622
diff changeset
    31
  {
5d7f741aaccb basic support for hyperlinks / Goto Definition Request;
wenzelm
parents: 64622
diff changeset
    32
    snapshot.cumulate[List[(String, Line.Range)]](
5d7f741aaccb basic support for hyperlinks / Goto Definition Request;
wenzelm
parents: 64622
diff changeset
    33
      range, Nil, VSCode_Rendering.hyperlink_elements, _ =>
5d7f741aaccb basic support for hyperlinks / Goto Definition Request;
wenzelm
parents: 64622
diff changeset
    34
        {
5d7f741aaccb basic support for hyperlinks / Goto Definition Request;
wenzelm
parents: 64622
diff changeset
    35
          case (links, Text.Info(_, XML.Elem(Markup.Path(name), _))) =>
5d7f741aaccb basic support for hyperlinks / Goto Definition Request;
wenzelm
parents: 64622
diff changeset
    36
            Some((resolve_file_url(name), Line.Range.zero) :: links)
5d7f741aaccb basic support for hyperlinks / Goto Definition Request;
wenzelm
parents: 64622
diff changeset
    37
5d7f741aaccb basic support for hyperlinks / Goto Definition Request;
wenzelm
parents: 64622
diff changeset
    38
/* FIXME
5d7f741aaccb basic support for hyperlinks / Goto Definition Request;
wenzelm
parents: 64622
diff changeset
    39
          case (links, Text.Info(_, XML.Elem(Markup.Url(name), _))) =>
5d7f741aaccb basic support for hyperlinks / Goto Definition Request;
wenzelm
parents: 64622
diff changeset
    40
            Some(PIDE.editor.hyperlink_url(name) :: links)
5d7f741aaccb basic support for hyperlinks / Goto Definition Request;
wenzelm
parents: 64622
diff changeset
    41
5d7f741aaccb basic support for hyperlinks / Goto Definition Request;
wenzelm
parents: 64622
diff changeset
    42
          case (links, Text.Info(info_range, XML.Elem(Markup(Markup.ENTITY, props), _)))
5d7f741aaccb basic support for hyperlinks / Goto Definition Request;
wenzelm
parents: 64622
diff changeset
    43
          if !props.exists(
5d7f741aaccb basic support for hyperlinks / Goto Definition Request;
wenzelm
parents: 64622
diff changeset
    44
            { case (Markup.KIND, Markup.ML_OPEN) => true
5d7f741aaccb basic support for hyperlinks / Goto Definition Request;
wenzelm
parents: 64622
diff changeset
    45
              case (Markup.KIND, Markup.ML_STRUCTURE) => true
5d7f741aaccb basic support for hyperlinks / Goto Definition Request;
wenzelm
parents: 64622
diff changeset
    46
              case _ => false }) =>
5d7f741aaccb basic support for hyperlinks / Goto Definition Request;
wenzelm
parents: 64622
diff changeset
    47
            val opt_link = PIDE.editor.hyperlink_def_position(true, snapshot, props)
5d7f741aaccb basic support for hyperlinks / Goto Definition Request;
wenzelm
parents: 64622
diff changeset
    48
            opt_link.map(_ :: links)
5d7f741aaccb basic support for hyperlinks / Goto Definition Request;
wenzelm
parents: 64622
diff changeset
    49
5d7f741aaccb basic support for hyperlinks / Goto Definition Request;
wenzelm
parents: 64622
diff changeset
    50
          case (links, Text.Info(info_range, XML.Elem(Markup(Markup.POSITION, props), _))) =>
5d7f741aaccb basic support for hyperlinks / Goto Definition Request;
wenzelm
parents: 64622
diff changeset
    51
            val opt_link = PIDE.editor.hyperlink_position(true, snapshot, props)
5d7f741aaccb basic support for hyperlinks / Goto Definition Request;
wenzelm
parents: 64622
diff changeset
    52
            opt_link.map(_ :: links)
5d7f741aaccb basic support for hyperlinks / Goto Definition Request;
wenzelm
parents: 64622
diff changeset
    53
*/
5d7f741aaccb basic support for hyperlinks / Goto Definition Request;
wenzelm
parents: 64622
diff changeset
    54
5d7f741aaccb basic support for hyperlinks / Goto Definition Request;
wenzelm
parents: 64622
diff changeset
    55
          case _ => None
5d7f741aaccb basic support for hyperlinks / Goto Definition Request;
wenzelm
parents: 64622
diff changeset
    56
        }) match { case Text.Info(_, links) :: _ => links.reverse case _ => Nil }
5d7f741aaccb basic support for hyperlinks / Goto Definition Request;
wenzelm
parents: 64622
diff changeset
    57
  }
64622
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
    58
}