/* Title: Tools/VSCode/src/vscode_rendering.scala
Author: Makarius
Isabelle/VSCode-specific implementation of quasi-abstract rendering and
markup interpretation.
*/
package isabelle.vscode
import isabelle._
object VSCode_Rendering
{
private val hyperlink_elements =
Markup.Elements(Markup.ENTITY, Markup.PATH, Markup.POSITION)
}
class VSCode_Rendering(
val model: Document_Model,
snapshot: Document.Snapshot,
options: Options,
text_length: Length,
resources: Resources)
extends Rendering(snapshot, options, resources)
{
/* tooltips */
def tooltip_margin: Int = options.int("vscode_tooltip_margin")
def timing_threshold: Double = options.real("vscode_timing_threshold")
/* hyperlinks */
def hyperlink_source_file(source_name: String, line1: Int, range: Symbol.Range)
: Option[Line.Node_Range] =
{
for (name <- resources.source_file(source_name))
yield {
val opt_text =
try { Some(File.read(Path.explode(name))) } // FIXME content from resources/models
catch { case ERROR(_) => None }
Line.Node_Range(File.platform_url(name),
opt_text match {
case Some(text) if range.start > 0 =>
val chunk = Symbol.Text_Chunk(text)
val doc = Line.Document(text)
def position(offset: Symbol.Offset) = doc.position(chunk.decode(offset), text_length)
Line.Range(position(range.start), position(range.stop))
case _ =>
Line.Range(Line.Position((line1 - 1) max 0))
})
}
}
def hyperlink_command(id: Document_ID.Generic, range: Symbol.Range): Option[Line.Node_Range] =
{
if (snapshot.is_outdated) None
else
for {
start <- snapshot.find_command_position(id, range.start)
stop <- snapshot.find_command_position(id, range.stop)
} yield Line.Node_Range(start.name, Line.Range(start.pos, stop.pos))
}
def hyperlink_position(pos: Position.T): Option[Line.Node_Range] =
pos match {
case Position.Item_File(name, line, range) => hyperlink_source_file(name, line, range)
case Position.Item_Id(id, range) => hyperlink_command(id, range)
case _ => None
}
def hyperlink_def_position(pos: Position.T): Option[Line.Node_Range] =
pos match {
case Position.Item_Def_File(name, line, range) => hyperlink_source_file(name, line, range)
case Position.Item_Def_Id(id, range) => hyperlink_command(id, range)
case _ => None
}
def hyperlinks(range: Text.Range): List[Line.Node_Range] =
{
snapshot.cumulate[List[Line.Node_Range]](
range, Nil, VSCode_Rendering.hyperlink_elements, _ =>
{
case (links, Text.Info(_, XML.Elem(Markup.Path(name), _))) =>
val file = resources.append_file_url(snapshot.node_name.master_dir, name)
Some(Line.Node_Range(file) :: links)
case (links, Text.Info(info_range, XML.Elem(Markup(Markup.ENTITY, props), _))) =>
hyperlink_def_position(props).map(_ :: links)
case (links, Text.Info(info_range, XML.Elem(Markup(Markup.POSITION, props), _))) =>
hyperlink_position(props).map(_ :: links)
case _ => None
}) match { case Text.Info(_, links) :: _ => links.reverse case _ => Nil }
}
}