src/Tools/VSCode/src/vscode_rendering.scala
author wenzelm
Tue Dec 20 22:24:16 2016 +0100 (2016-12-20)
changeset 64622 529bbb8977c7
child 64648 5d7f741aaccb
permissions -rw-r--r--
more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
     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 
    14 class VSCode_Rendering(snapshot: Document.Snapshot, options: Options, resources: Resources)
    15   extends Rendering(snapshot, options, resources)
    16 {
    17   /* tooltips */
    18 
    19   def tooltip_margin: Int = options.int("vscode_tooltip_margin")
    20   def timing_threshold: Double = options.real("vscode_timing_threshold")
    21 }