more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
authorwenzelm
Tue Dec 20 22:24:16 2016 +0100 (2016-12-20)
changeset 64622529bbb8977c7
parent 64621 7116f2634e32
child 64623 83f012ce2567
more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
etc/components
src/Pure/PIDE/rendering.scala
src/Pure/build-jars
src/Tools/VSCode/etc/options
src/Tools/VSCode/src/document_model.scala
src/Tools/VSCode/src/server.scala
src/Tools/VSCode/src/vscode_rendering.scala
src/Tools/jEdit/src/jedit_rendering.scala
     1.1 --- a/etc/components	Tue Dec 20 21:35:56 2016 +0100
     1.2 +++ b/etc/components	Tue Dec 20 22:24:16 2016 +0100
     1.3 @@ -1,6 +1,7 @@
     1.4  #hard-wired components
     1.5  src/Tools/jEdit
     1.6  src/Tools/Graphview
     1.7 +src/Tools/VSCode
     1.8  src/HOL/Mirabelle
     1.9  src/HOL/Mutabelle
    1.10  src/HOL/Library/Sum_of_Squares
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/Pure/PIDE/rendering.scala	Tue Dec 20 22:24:16 2016 +0100
     2.3 @@ -0,0 +1,147 @@
     2.4 +/*  Title:      Pure/PIDE/rendering.scala
     2.5 +    Author:     Makarius
     2.6 +
     2.7 +Isabelle-specific implementation of quasi-abstract rendering and
     2.8 +markup interpretation.
     2.9 +*/
    2.10 +
    2.11 +package isabelle
    2.12 +
    2.13 +
    2.14 +object Rendering
    2.15 +{
    2.16 +  private val tooltip_descriptions =
    2.17 +    Map(
    2.18 +      Markup.CITATION -> "citation",
    2.19 +      Markup.TOKEN_RANGE -> "inner syntax token",
    2.20 +      Markup.FREE -> "free variable",
    2.21 +      Markup.SKOLEM -> "skolem variable",
    2.22 +      Markup.BOUND -> "bound variable",
    2.23 +      Markup.VAR -> "schematic variable",
    2.24 +      Markup.TFREE -> "free type variable",
    2.25 +      Markup.TVAR -> "schematic type variable")
    2.26 +
    2.27 +  private val tooltip_elements =
    2.28 +    Markup.Elements(Markup.LANGUAGE, Markup.EXPRESSION, Markup.TIMING, Markup.ENTITY,
    2.29 +      Markup.SORTING, Markup.TYPING, Markup.CLASS_PARAMETER, Markup.ML_TYPING,
    2.30 +      Markup.ML_BREAKPOINT, Markup.PATH, Markup.DOC, Markup.URL, Markup.MARKDOWN_PARAGRAPH,
    2.31 +      Markup.Markdown_List.name) ++ Markup.Elements(tooltip_descriptions.keySet)
    2.32 +
    2.33 +  private def pretty_typing(kind: String, body: XML.Body): XML.Tree =
    2.34 +    Pretty.block(XML.Text(kind) :: Pretty.brk(1) :: body)
    2.35 +}
    2.36 +
    2.37 +abstract class Rendering(
    2.38 +  val snapshot: Document.Snapshot,
    2.39 +  val options: Options,
    2.40 +  val resources: Resources)
    2.41 +{
    2.42 +  override def toString: String = "Rendering(" + snapshot.toString + ")"
    2.43 +
    2.44 +
    2.45 +  /* resources */
    2.46 +
    2.47 +  def resolve_file(name: String): String =
    2.48 +    if (Path.is_valid(name))
    2.49 +      resources.append(snapshot.node_name.master_dir, Path.explode(name))
    2.50 +    else name
    2.51 +
    2.52 +
    2.53 +  /* tooltips */
    2.54 +
    2.55 +  def tooltip_margin: Int
    2.56 +  def timing_threshold: Double
    2.57 +
    2.58 +  def tooltip(range: Text.Range): Option[Text.Info[XML.Body]] =
    2.59 +  {
    2.60 +    def add(prev: Text.Info[(Timing, Vector[(Boolean, XML.Tree)])],
    2.61 +      r0: Text.Range, p: (Boolean, XML.Tree)): Text.Info[(Timing, Vector[(Boolean, XML.Tree)])] =
    2.62 +    {
    2.63 +      val r = snapshot.convert(r0)
    2.64 +      val (t, info) = prev.info
    2.65 +      if (prev.range == r)
    2.66 +        Text.Info(r, (t, info :+ p))
    2.67 +      else Text.Info(r, (t, Vector(p)))
    2.68 +    }
    2.69 +
    2.70 +    val results =
    2.71 +      snapshot.cumulate[Text.Info[(Timing, Vector[(Boolean, XML.Tree)])]](
    2.72 +        range, Text.Info(range, (Timing.zero, Vector.empty)), Rendering.tooltip_elements, _ =>
    2.73 +        {
    2.74 +          case (Text.Info(r, (t1, info)), Text.Info(_, XML.Elem(Markup.Timing(t2), _))) =>
    2.75 +            Some(Text.Info(r, (t1 + t2, info)))
    2.76 +
    2.77 +          case (prev, Text.Info(r, XML.Elem(Markup.Entity(kind, name), _)))
    2.78 +          if kind != "" &&
    2.79 +            kind != Markup.ML_DEF &&
    2.80 +            kind != Markup.ML_OPEN &&
    2.81 +            kind != Markup.ML_STRUCTURE =>
    2.82 +            val kind1 = Word.implode(Word.explode('_', kind))
    2.83 +            val txt1 =
    2.84 +              if (name == "") kind1
    2.85 +              else if (kind1 == "") quote(name)
    2.86 +              else kind1 + " " + quote(name)
    2.87 +            val t = prev.info._1
    2.88 +            val txt2 =
    2.89 +              if (kind == Markup.COMMAND && t.elapsed.seconds >= timing_threshold)
    2.90 +                "\n" + t.message
    2.91 +              else ""
    2.92 +            Some(add(prev, r, (true, XML.Text(txt1 + txt2))))
    2.93 +
    2.94 +          case (prev, Text.Info(r, XML.Elem(Markup.Path(name), _))) =>
    2.95 +            val file = resolve_file(name)
    2.96 +            val text =
    2.97 +              if (name == file) "file " + quote(file)
    2.98 +              else "path " + quote(name) + "\nfile " + quote(file)
    2.99 +            Some(add(prev, r, (true, XML.Text(text))))
   2.100 +
   2.101 +          case (prev, Text.Info(r, XML.Elem(Markup.Doc(name), _))) =>
   2.102 +            val text = "doc " + quote(name)
   2.103 +            Some(add(prev, r, (true, XML.Text(text))))
   2.104 +
   2.105 +          case (prev, Text.Info(r, XML.Elem(Markup.Url(name), _))) =>
   2.106 +            Some(add(prev, r, (true, XML.Text("URL " + quote(name)))))
   2.107 +
   2.108 +          case (prev, Text.Info(r, XML.Elem(Markup(name, _), body)))
   2.109 +          if name == Markup.SORTING || name == Markup.TYPING =>
   2.110 +            Some(add(prev, r, (true, Rendering.pretty_typing("::", body))))
   2.111 +
   2.112 +          case (prev, Text.Info(r, XML.Elem(Markup(Markup.CLASS_PARAMETER, _), body))) =>
   2.113 +            Some(add(prev, r, (true, Pretty.block(0, body))))
   2.114 +
   2.115 +          case (prev, Text.Info(r, XML.Elem(Markup(Markup.ML_TYPING, _), body))) =>
   2.116 +            Some(add(prev, r, (false, Rendering.pretty_typing("ML:", body))))
   2.117 +
   2.118 +          case (prev, Text.Info(r, Protocol.ML_Breakpoint(breakpoint))) =>
   2.119 +            val text =
   2.120 +              if (Debugger.breakpoint_state(breakpoint)) "breakpoint (enabled)"
   2.121 +              else "breakpoint (disabled)"
   2.122 +            Some(add(prev, r, (true, XML.Text(text))))
   2.123 +
   2.124 +          case (prev, Text.Info(r, XML.Elem(Markup.Language(language, _, _, _), _))) =>
   2.125 +            val lang = Word.implode(Word.explode('_', language))
   2.126 +            Some(add(prev, r, (true, XML.Text("language: " + lang))))
   2.127 +
   2.128 +          case (prev, Text.Info(r, XML.Elem(Markup.Expression(kind), _))) =>
   2.129 +            val descr = if (kind == "") "expression" else "expression: " + kind
   2.130 +            Some(add(prev, r, (true, XML.Text(descr))))
   2.131 +
   2.132 +          case (prev, Text.Info(r, XML.Elem(Markup(Markup.MARKDOWN_PARAGRAPH, _), _))) =>
   2.133 +            Some(add(prev, r, (true, XML.Text("Markdown: paragraph"))))
   2.134 +          case (prev, Text.Info(r, XML.Elem(Markup.Markdown_List(kind), _))) =>
   2.135 +            Some(add(prev, r, (true, XML.Text("Markdown: " + kind))))
   2.136 +
   2.137 +          case (prev, Text.Info(r, XML.Elem(Markup(name, _), _))) =>
   2.138 +            Rendering.tooltip_descriptions.get(name).
   2.139 +              map(descr => add(prev, r, (true, XML.Text(descr))))
   2.140 +        }).map(_.info)
   2.141 +
   2.142 +    results.map(_.info).flatMap(res => res._2.toList) match {
   2.143 +      case Nil => None
   2.144 +      case tips =>
   2.145 +        val r = Text.Range(results.head.range.start, results.last.range.stop)
   2.146 +        val all_tips = (tips.filter(_._1) ++ tips.filter(!_._1).lastOption.toList).map(_._2)
   2.147 +        Some(Text.Info(r, Library.separate(Pretty.fbrk, all_tips)))
   2.148 +    }
   2.149 +  }
   2.150 +}
     3.1 --- a/src/Pure/build-jars	Tue Dec 20 21:35:56 2016 +0100
     3.2 +++ b/src/Pure/build-jars	Tue Dec 20 22:24:16 2016 +0100
     3.3 @@ -94,6 +94,7 @@
     3.4    PIDE/protocol_message.scala
     3.5    PIDE/prover.scala
     3.6    PIDE/query_operation.scala
     3.7 +  PIDE/rendering.scala
     3.8    PIDE/resources.scala
     3.9    PIDE/session.scala
    3.10    PIDE/text.scala
    3.11 @@ -162,6 +163,7 @@
    3.12    ../Tools/VSCode/src/protocol.scala
    3.13    ../Tools/VSCode/src/server.scala
    3.14    ../Tools/VSCode/src/uri_resources.scala
    3.15 +  ../Tools/VSCode/src/vscode_rendering.scala
    3.16  )
    3.17  
    3.18  
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/Tools/VSCode/etc/options	Tue Dec 20 22:24:16 2016 +0100
     4.3 @@ -0,0 +1,7 @@
     4.4 +(* :mode=isabelle-options: *)
     4.5 +
     4.6 +option vscode_tooltip_margin : int = 60
     4.7 +  -- "margin for tooltip pretty-printing"
     4.8 +
     4.9 +option vscode_timing_threshold : real = 0.1
    4.10 +  -- "default threshold for timing display (seconds)"
     5.1 --- a/src/Tools/VSCode/src/document_model.scala	Tue Dec 20 21:35:56 2016 +0100
     5.2 +++ b/src/Tools/VSCode/src/document_model.scala	Tue Dec 20 22:24:16 2016 +0100
     5.3 @@ -52,7 +52,10 @@
     5.4    def unchanged: Document_Model = if (changed) copy(changed = false) else this
     5.5  
     5.6  
     5.7 -  /* snapshot */
     5.8 +  /* snapshot and rendering */
     5.9  
    5.10    def snapshot(): Document.Snapshot = session.snapshot(node_name, text_edits)
    5.11 +
    5.12 +  def rendering(options: Options): VSCode_Rendering =
    5.13 +    new VSCode_Rendering(snapshot(), options, session.resources)
    5.14  }
     6.1 --- a/src/Tools/VSCode/src/server.scala	Tue Dec 20 21:35:56 2016 +0100
     6.2 +++ b/src/Tools/VSCode/src/server.scala	Tue Dec 20 22:24:16 2016 +0100
     6.3 @@ -188,125 +188,21 @@
     6.4    }
     6.5  
     6.6  
     6.7 -  /* tooltips -- see $ISABELLE_HOME/src/Tools/jEdit/rendering.scala */
     6.8 +  /* hover */
     6.9  
    6.10    def hover(uri: String, pos: Line.Position): Option[(Line.Range, List[String])] =
    6.11      for {
    6.12        model <- state.value.models.get(uri)
    6.13 -      snapshot = model.snapshot()
    6.14 +      rendering = model.rendering(options)
    6.15        offset <- model.doc.offset(pos, text_length)
    6.16 -      info <- tooltip(snapshot, Text.Range(offset, offset + 1))
    6.17 +      info <- rendering.tooltip(Text.Range(offset, offset + 1))
    6.18      } yield {
    6.19        val start = model.doc.position(info.range.start, text_length)
    6.20        val stop = model.doc.position(info.range.stop, text_length)
    6.21 -      val s = Pretty.string_of(info.info, margin = tooltip_margin.toDouble)
    6.22 +      val s = Pretty.string_of(info.info, margin = rendering.tooltip_margin)
    6.23        (Line.Range(start, stop), List("```\n" + s + "\n```"))
    6.24      }
    6.25  
    6.26 -  private val tooltip_descriptions =
    6.27 -    Map(
    6.28 -      Markup.CITATION -> "citation",
    6.29 -      Markup.TOKEN_RANGE -> "inner syntax token",
    6.30 -      Markup.FREE -> "free variable",
    6.31 -      Markup.SKOLEM -> "skolem variable",
    6.32 -      Markup.BOUND -> "bound variable",
    6.33 -      Markup.VAR -> "schematic variable",
    6.34 -      Markup.TFREE -> "free type variable",
    6.35 -      Markup.TVAR -> "schematic type variable")
    6.36 -
    6.37 -  private val tooltip_elements =
    6.38 -    Markup.Elements(Markup.LANGUAGE, Markup.EXPRESSION, Markup.TIMING, Markup.ENTITY,
    6.39 -      Markup.SORTING, Markup.TYPING, Markup.CLASS_PARAMETER, Markup.ML_TYPING,
    6.40 -      Markup.ML_BREAKPOINT, Markup.PATH, Markup.DOC, Markup.URL, Markup.MARKDOWN_PARAGRAPH,
    6.41 -      Markup.Markdown_List.name) ++ Markup.Elements(tooltip_descriptions.keySet)
    6.42 -
    6.43 -  private def pretty_typing(kind: String, body: XML.Body): XML.Tree =
    6.44 -    Pretty.block(XML.Text(kind) :: Pretty.brk(1) :: body)
    6.45 -
    6.46 -  private def timing_threshold: Double = options.real("jedit_timing_threshold")
    6.47 -
    6.48 -  def tooltip(snapshot: Document.Snapshot, range: Text.Range): Option[Text.Info[XML.Body]] =
    6.49 -  {
    6.50 -    def add(prev: Text.Info[(Timing, Vector[(Boolean, XML.Tree)])],
    6.51 -      r0: Text.Range, p: (Boolean, XML.Tree)): Text.Info[(Timing, Vector[(Boolean, XML.Tree)])] =
    6.52 -    {
    6.53 -      val r = snapshot.convert(r0)
    6.54 -      val (t, info) = prev.info
    6.55 -      if (prev.range == r)
    6.56 -        Text.Info(r, (t, info :+ p))
    6.57 -      else Text.Info(r, (t, Vector(p)))
    6.58 -    }
    6.59 -
    6.60 -    val results =
    6.61 -      snapshot.cumulate[Text.Info[(Timing, Vector[(Boolean, XML.Tree)])]](
    6.62 -        range, Text.Info(range, (Timing.zero, Vector.empty)), tooltip_elements, _ =>
    6.63 -        {
    6.64 -          case (Text.Info(r, (t1, info)), Text.Info(_, XML.Elem(Markup.Timing(t2), _))) =>
    6.65 -            Some(Text.Info(r, (t1 + t2, info)))
    6.66 -
    6.67 -          case (prev, Text.Info(r, XML.Elem(Markup.Entity(kind, name), _)))
    6.68 -          if kind != "" &&
    6.69 -            kind != Markup.ML_DEF &&
    6.70 -            kind != Markup.ML_OPEN &&
    6.71 -            kind != Markup.ML_STRUCTURE =>
    6.72 -            val kind1 = Word.implode(Word.explode('_', kind))
    6.73 -            val txt1 =
    6.74 -              if (name == "") kind1
    6.75 -              else if (kind1 == "") quote(name)
    6.76 -              else kind1 + " " + quote(name)
    6.77 -            val t = prev.info._1
    6.78 -            val txt2 =
    6.79 -              if (kind == Markup.COMMAND && t.elapsed.seconds >= timing_threshold)
    6.80 -                "\n" + t.message
    6.81 -              else ""
    6.82 -            Some(add(prev, r, (true, XML.Text(txt1 + txt2))))
    6.83 -
    6.84 -          case (prev, Text.Info(r, XML.Elem(Markup.Doc(name), _))) =>
    6.85 -            val text = "doc " + quote(name)
    6.86 -            Some(add(prev, r, (true, XML.Text(text))))
    6.87 -
    6.88 -          case (prev, Text.Info(r, XML.Elem(Markup.Url(name), _))) =>
    6.89 -            Some(add(prev, r, (true, XML.Text("URL " + quote(name)))))
    6.90 -
    6.91 -          case (prev, Text.Info(r, XML.Elem(Markup(name, _), body)))
    6.92 -          if name == Markup.SORTING || name == Markup.TYPING =>
    6.93 -            Some(add(prev, r, (true, pretty_typing("::", body))))
    6.94 -
    6.95 -          case (prev, Text.Info(r, XML.Elem(Markup(Markup.CLASS_PARAMETER, _), body))) =>
    6.96 -            Some(add(prev, r, (true, Pretty.block(0, body))))
    6.97 -
    6.98 -          case (prev, Text.Info(r, XML.Elem(Markup(Markup.ML_TYPING, _), body))) =>
    6.99 -            Some(add(prev, r, (false, pretty_typing("ML:", body))))
   6.100 -
   6.101 -          case (prev, Text.Info(r, XML.Elem(Markup.Language(language, _, _, _), _))) =>
   6.102 -            val lang = Word.implode(Word.explode('_', language))
   6.103 -            Some(add(prev, r, (true, XML.Text("language: " + lang))))
   6.104 -
   6.105 -          case (prev, Text.Info(r, XML.Elem(Markup.Expression(kind), _))) =>
   6.106 -            val descr = if (kind == "") "expression" else "expression: " + kind
   6.107 -            Some(add(prev, r, (true, XML.Text(descr))))
   6.108 -
   6.109 -          case (prev, Text.Info(r, XML.Elem(Markup(Markup.MARKDOWN_PARAGRAPH, _), _))) =>
   6.110 -            Some(add(prev, r, (true, XML.Text("Markdown: paragraph"))))
   6.111 -          case (prev, Text.Info(r, XML.Elem(Markup.Markdown_List(kind), _))) =>
   6.112 -            Some(add(prev, r, (true, XML.Text("Markdown: " + kind))))
   6.113 -
   6.114 -          case (prev, Text.Info(r, XML.Elem(Markup(name, _), _))) =>
   6.115 -            tooltip_descriptions.get(name).
   6.116 -              map(descr => add(prev, r, (true, XML.Text(descr))))
   6.117 -        }).map(_.info)
   6.118 -
   6.119 -    results.map(_.info).flatMap(res => res._2.toList) match {
   6.120 -      case Nil => None
   6.121 -      case tips =>
   6.122 -        val r = Text.Range(results.head.range.start, results.last.range.stop)
   6.123 -        val all_tips = (tips.filter(_._1) ++ tips.filter(!_._1).lastOption.toList).map(_._2)
   6.124 -        Some(Text.Info(r, Library.separate(Pretty.fbrk, all_tips)))
   6.125 -    }
   6.126 -  }
   6.127 -
   6.128 -  def tooltip_margin: Int = options.int("jedit_tooltip_margin")
   6.129 -
   6.130  
   6.131    /* main loop */
   6.132  
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/src/Tools/VSCode/src/vscode_rendering.scala	Tue Dec 20 22:24:16 2016 +0100
     7.3 @@ -0,0 +1,21 @@
     7.4 +/*  Title:      Tools/VSCode/src/vscode_rendering.scala
     7.5 +    Author:     Makarius
     7.6 +
     7.7 +Isabelle/VSCode-specific implementation of quasi-abstract rendering and
     7.8 +markup interpretation.
     7.9 +*/
    7.10 +
    7.11 +package isabelle.vscode
    7.12 +
    7.13 +
    7.14 +import isabelle._
    7.15 +
    7.16 +
    7.17 +class VSCode_Rendering(snapshot: Document.Snapshot, options: Options, resources: Resources)
    7.18 +  extends Rendering(snapshot, options, resources)
    7.19 +{
    7.20 +  /* tooltips */
    7.21 +
    7.22 +  def tooltip_margin: Int = options.int("vscode_tooltip_margin")
    7.23 +  def timing_threshold: Double = options.real("vscode_timing_threshold")
    7.24 +}
     8.1 --- a/src/Tools/jEdit/src/jedit_rendering.scala	Tue Dec 20 21:35:56 2016 +0100
     8.2 +++ b/src/Tools/jEdit/src/jedit_rendering.scala	Tue Dec 20 22:24:16 2016 +0100
     8.3 @@ -1,7 +1,7 @@
     8.4 -/*  Title:      Tools/jEdit/src/rendering.scala
     8.5 +/*  Title:      Tools/jEdit/src/jedit_rendering.scala
     8.6      Author:     Makarius
     8.7  
     8.8 -Isabelle-specific implementation of quasi-abstract rendering and
     8.9 +Isabelle/jEdit-specific implementation of quasi-abstract rendering and
    8.10  markup interpretation.
    8.11  */
    8.12  
    8.13 @@ -175,23 +175,6 @@
    8.14      Markup.Elements(Markup.WRITELN, Markup.INFORMATION, Markup.WARNING, Markup.LEGACY, Markup.ERROR,
    8.15        Markup.BAD)
    8.16  
    8.17 -  private val tooltip_descriptions =
    8.18 -    Map(
    8.19 -      Markup.CITATION -> "citation",
    8.20 -      Markup.TOKEN_RANGE -> "inner syntax token",
    8.21 -      Markup.FREE -> "free variable",
    8.22 -      Markup.SKOLEM -> "skolem variable",
    8.23 -      Markup.BOUND -> "bound variable",
    8.24 -      Markup.VAR -> "schematic variable",
    8.25 -      Markup.TFREE -> "free type variable",
    8.26 -      Markup.TVAR -> "schematic type variable")
    8.27 -
    8.28 -  private val tooltip_elements =
    8.29 -    Markup.Elements(Markup.LANGUAGE, Markup.EXPRESSION, Markup.TIMING, Markup.ENTITY,
    8.30 -      Markup.SORTING, Markup.TYPING, Markup.CLASS_PARAMETER, Markup.ML_TYPING,
    8.31 -      Markup.ML_BREAKPOINT, Markup.PATH, Markup.DOC, Markup.URL, Markup.MARKDOWN_PARAGRAPH,
    8.32 -      Markup.Markdown_List.name) ++ Markup.Elements(tooltip_descriptions.keySet)
    8.33 -
    8.34    private val gutter_elements =
    8.35      Markup.Elements(Markup.WRITELN, Markup.INFORMATION, Markup.WARNING, Markup.LEGACY, Markup.ERROR)
    8.36  
    8.37 @@ -226,11 +209,9 @@
    8.38  }
    8.39  
    8.40  
    8.41 -class JEdit_Rendering private(val snapshot: Document.Snapshot, val options: Options)
    8.42 +class JEdit_Rendering(snapshot: Document.Snapshot, options: Options)
    8.43 +  extends Rendering(snapshot, options, PIDE.resources)
    8.44  {
    8.45 -  override def toString: String = "Rendering(" + snapshot.toString + ")"
    8.46 -
    8.47 -
    8.48    /* colors */
    8.49  
    8.50    def color_value(s: String): Color = Color_Value(options.string(s))
    8.51 @@ -479,18 +460,13 @@
    8.52  
    8.53    /* hyperlinks */
    8.54  
    8.55 -  private def jedit_file(name: String): String =
    8.56 -    if (Path.is_valid(name))
    8.57 -      PIDE.resources.append(snapshot.node_name.master_dir, Path.explode(name))
    8.58 -    else name
    8.59 -
    8.60    def hyperlink(range: Text.Range): Option[Text.Info[PIDE.editor.Hyperlink]] =
    8.61    {
    8.62      snapshot.cumulate[Vector[Text.Info[PIDE.editor.Hyperlink]]](
    8.63        range, Vector.empty, JEdit_Rendering.hyperlink_elements, _ =>
    8.64          {
    8.65            case (links, Text.Info(info_range, XML.Elem(Markup.Path(name), _))) =>
    8.66 -            val link = PIDE.editor.hyperlink_file(true, jedit_file(name))
    8.67 +            val link = PIDE.editor.hyperlink_file(true, resolve_file(name))
    8.68              Some(links :+ Text.Info(snapshot.convert(info_range), link))
    8.69  
    8.70            case (links, Text.Info(info_range, XML.Elem(Markup.Doc(name), _))) =>
    8.71 @@ -580,105 +556,8 @@
    8.72  
    8.73    /* tooltips */
    8.74  
    8.75 -  private def pretty_typing(kind: String, body: XML.Body): XML.Tree =
    8.76 -    Pretty.block(XML.Text(kind) :: Pretty.brk(1) :: body)
    8.77 -
    8.78 -  private def timing_threshold: Double = options.real("jedit_timing_threshold")
    8.79 -
    8.80 -  def tooltip(range: Text.Range): Option[Text.Info[XML.Body]] =
    8.81 -  {
    8.82 -    def add(prev: Text.Info[(Timing, Vector[(Boolean, XML.Tree)])],
    8.83 -      r0: Text.Range, p: (Boolean, XML.Tree)): Text.Info[(Timing, Vector[(Boolean, XML.Tree)])] =
    8.84 -    {
    8.85 -      val r = snapshot.convert(r0)
    8.86 -      val (t, info) = prev.info
    8.87 -      if (prev.range == r)
    8.88 -        Text.Info(r, (t, info :+ p))
    8.89 -      else Text.Info(r, (t, Vector(p)))
    8.90 -    }
    8.91 -
    8.92 -    val results =
    8.93 -      snapshot.cumulate[Text.Info[(Timing, Vector[(Boolean, XML.Tree)])]](
    8.94 -        range, Text.Info(range, (Timing.zero, Vector.empty)), JEdit_Rendering.tooltip_elements, _ =>
    8.95 -        {
    8.96 -          case (Text.Info(r, (t1, info)), Text.Info(_, XML.Elem(Markup.Timing(t2), _))) =>
    8.97 -            Some(Text.Info(r, (t1 + t2, info)))
    8.98 -
    8.99 -          case (prev, Text.Info(r, XML.Elem(Markup.Entity(kind, name), _)))
   8.100 -          if kind != "" &&
   8.101 -            kind != Markup.ML_DEF &&
   8.102 -            kind != Markup.ML_OPEN &&
   8.103 -            kind != Markup.ML_STRUCTURE =>
   8.104 -            val kind1 = Word.implode(Word.explode('_', kind))
   8.105 -            val txt1 =
   8.106 -              if (name == "") kind1
   8.107 -              else if (kind1 == "") quote(name)
   8.108 -              else kind1 + " " + quote(name)
   8.109 -            val t = prev.info._1
   8.110 -            val txt2 =
   8.111 -              if (kind == Markup.COMMAND && t.elapsed.seconds >= timing_threshold)
   8.112 -                "\n" + t.message
   8.113 -              else ""
   8.114 -            Some(add(prev, r, (true, XML.Text(txt1 + txt2))))
   8.115 -
   8.116 -          case (prev, Text.Info(r, XML.Elem(Markup.Path(name), _))) =>
   8.117 -            val file = jedit_file(name)
   8.118 -            val text =
   8.119 -              if (name == file) "file " + quote(file)
   8.120 -              else "path " + quote(name) + "\nfile " + quote(file)
   8.121 -            Some(add(prev, r, (true, XML.Text(text))))
   8.122 -
   8.123 -          case (prev, Text.Info(r, XML.Elem(Markup.Doc(name), _))) =>
   8.124 -            val text = "doc " + quote(name)
   8.125 -            Some(add(prev, r, (true, XML.Text(text))))
   8.126 -
   8.127 -          case (prev, Text.Info(r, XML.Elem(Markup.Url(name), _))) =>
   8.128 -            Some(add(prev, r, (true, XML.Text("URL " + quote(name)))))
   8.129 -
   8.130 -          case (prev, Text.Info(r, XML.Elem(Markup(name, _), body)))
   8.131 -          if name == Markup.SORTING || name == Markup.TYPING =>
   8.132 -            Some(add(prev, r, (true, pretty_typing("::", body))))
   8.133 -
   8.134 -          case (prev, Text.Info(r, XML.Elem(Markup(Markup.CLASS_PARAMETER, _), body))) =>
   8.135 -            Some(add(prev, r, (true, Pretty.block(0, body))))
   8.136 -
   8.137 -          case (prev, Text.Info(r, XML.Elem(Markup(Markup.ML_TYPING, _), body))) =>
   8.138 -            Some(add(prev, r, (false, pretty_typing("ML:", body))))
   8.139 -
   8.140 -          case (prev, Text.Info(r, Protocol.ML_Breakpoint(breakpoint))) =>
   8.141 -            val text =
   8.142 -              if (Debugger.breakpoint_state(breakpoint)) "breakpoint (enabled)"
   8.143 -              else "breakpoint (disabled)"
   8.144 -            Some(add(prev, r, (true, XML.Text(text))))
   8.145 -
   8.146 -          case (prev, Text.Info(r, XML.Elem(Markup.Language(language, _, _, _), _))) =>
   8.147 -            val lang = Word.implode(Word.explode('_', language))
   8.148 -            Some(add(prev, r, (true, XML.Text("language: " + lang))))
   8.149 -
   8.150 -          case (prev, Text.Info(r, XML.Elem(Markup.Expression(kind), _))) =>
   8.151 -            val descr = if (kind == "") "expression" else "expression: " + kind
   8.152 -            Some(add(prev, r, (true, XML.Text(descr))))
   8.153 -
   8.154 -          case (prev, Text.Info(r, XML.Elem(Markup(Markup.MARKDOWN_PARAGRAPH, _), _))) =>
   8.155 -            Some(add(prev, r, (true, XML.Text("Markdown: paragraph"))))
   8.156 -          case (prev, Text.Info(r, XML.Elem(Markup.Markdown_List(kind), _))) =>
   8.157 -            Some(add(prev, r, (true, XML.Text("Markdown: " + kind))))
   8.158 -
   8.159 -          case (prev, Text.Info(r, XML.Elem(Markup(name, _), _))) =>
   8.160 -            JEdit_Rendering.tooltip_descriptions.get(name).
   8.161 -              map(descr => add(prev, r, (true, XML.Text(descr))))
   8.162 -        }).map(_.info)
   8.163 -
   8.164 -    results.map(_.info).flatMap(res => res._2.toList) match {
   8.165 -      case Nil => None
   8.166 -      case tips =>
   8.167 -        val r = Text.Range(results.head.range.start, results.last.range.stop)
   8.168 -        val all_tips = (tips.filter(_._1) ++ tips.filter(!_._1).lastOption.toList).map(_._2)
   8.169 -        Some(Text.Info(r, Library.separate(Pretty.fbrk, all_tips)))
   8.170 -    }
   8.171 -  }
   8.172 -
   8.173    def tooltip_margin: Int = options.int("jedit_tooltip_margin")
   8.174 +  def timing_threshold: Double = options.real("jedit_timing_threshold")
   8.175  
   8.176    lazy val tooltip_close_icon = JEdit_Lib.load_icon(options.string("tooltip_close_icon"))
   8.177    lazy val tooltip_detach_icon = JEdit_Lib.load_icon(options.string("tooltip_detach_icon"))