--- a/etc/components Tue Dec 20 21:35:56 2016 +0100
+++ b/etc/components Tue Dec 20 22:24:16 2016 +0100
@@ -1,6 +1,7 @@
#hard-wired components
src/Tools/jEdit
src/Tools/Graphview
+src/Tools/VSCode
src/HOL/Mirabelle
src/HOL/Mutabelle
src/HOL/Library/Sum_of_Squares
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/PIDE/rendering.scala Tue Dec 20 22:24:16 2016 +0100
@@ -0,0 +1,147 @@
+/* Title: Pure/PIDE/rendering.scala
+ Author: Makarius
+
+Isabelle-specific implementation of quasi-abstract rendering and
+markup interpretation.
+*/
+
+package isabelle
+
+
+object Rendering
+{
+ private val tooltip_descriptions =
+ Map(
+ Markup.CITATION -> "citation",
+ Markup.TOKEN_RANGE -> "inner syntax token",
+ Markup.FREE -> "free variable",
+ Markup.SKOLEM -> "skolem variable",
+ Markup.BOUND -> "bound variable",
+ Markup.VAR -> "schematic variable",
+ Markup.TFREE -> "free type variable",
+ Markup.TVAR -> "schematic type variable")
+
+ private val tooltip_elements =
+ Markup.Elements(Markup.LANGUAGE, Markup.EXPRESSION, Markup.TIMING, Markup.ENTITY,
+ Markup.SORTING, Markup.TYPING, Markup.CLASS_PARAMETER, Markup.ML_TYPING,
+ Markup.ML_BREAKPOINT, Markup.PATH, Markup.DOC, Markup.URL, Markup.MARKDOWN_PARAGRAPH,
+ Markup.Markdown_List.name) ++ Markup.Elements(tooltip_descriptions.keySet)
+
+ private def pretty_typing(kind: String, body: XML.Body): XML.Tree =
+ Pretty.block(XML.Text(kind) :: Pretty.brk(1) :: body)
+}
+
+abstract class Rendering(
+ val snapshot: Document.Snapshot,
+ val options: Options,
+ val resources: Resources)
+{
+ override def toString: String = "Rendering(" + snapshot.toString + ")"
+
+
+ /* resources */
+
+ def resolve_file(name: String): String =
+ if (Path.is_valid(name))
+ resources.append(snapshot.node_name.master_dir, Path.explode(name))
+ else name
+
+
+ /* tooltips */
+
+ def tooltip_margin: Int
+ def timing_threshold: Double
+
+ def tooltip(range: Text.Range): Option[Text.Info[XML.Body]] =
+ {
+ def add(prev: Text.Info[(Timing, Vector[(Boolean, XML.Tree)])],
+ r0: Text.Range, p: (Boolean, XML.Tree)): Text.Info[(Timing, Vector[(Boolean, XML.Tree)])] =
+ {
+ val r = snapshot.convert(r0)
+ val (t, info) = prev.info
+ if (prev.range == r)
+ Text.Info(r, (t, info :+ p))
+ else Text.Info(r, (t, Vector(p)))
+ }
+
+ val results =
+ snapshot.cumulate[Text.Info[(Timing, Vector[(Boolean, XML.Tree)])]](
+ range, Text.Info(range, (Timing.zero, Vector.empty)), Rendering.tooltip_elements, _ =>
+ {
+ case (Text.Info(r, (t1, info)), Text.Info(_, XML.Elem(Markup.Timing(t2), _))) =>
+ Some(Text.Info(r, (t1 + t2, info)))
+
+ case (prev, Text.Info(r, XML.Elem(Markup.Entity(kind, name), _)))
+ if kind != "" &&
+ kind != Markup.ML_DEF &&
+ kind != Markup.ML_OPEN &&
+ kind != Markup.ML_STRUCTURE =>
+ val kind1 = Word.implode(Word.explode('_', kind))
+ val txt1 =
+ if (name == "") kind1
+ else if (kind1 == "") quote(name)
+ else kind1 + " " + quote(name)
+ val t = prev.info._1
+ val txt2 =
+ if (kind == Markup.COMMAND && t.elapsed.seconds >= timing_threshold)
+ "\n" + t.message
+ else ""
+ Some(add(prev, r, (true, XML.Text(txt1 + txt2))))
+
+ case (prev, Text.Info(r, XML.Elem(Markup.Path(name), _))) =>
+ val file = resolve_file(name)
+ val text =
+ if (name == file) "file " + quote(file)
+ else "path " + quote(name) + "\nfile " + quote(file)
+ Some(add(prev, r, (true, XML.Text(text))))
+
+ case (prev, Text.Info(r, XML.Elem(Markup.Doc(name), _))) =>
+ val text = "doc " + quote(name)
+ Some(add(prev, r, (true, XML.Text(text))))
+
+ case (prev, Text.Info(r, XML.Elem(Markup.Url(name), _))) =>
+ Some(add(prev, r, (true, XML.Text("URL " + quote(name)))))
+
+ case (prev, Text.Info(r, XML.Elem(Markup(name, _), body)))
+ if name == Markup.SORTING || name == Markup.TYPING =>
+ Some(add(prev, r, (true, Rendering.pretty_typing("::", body))))
+
+ case (prev, Text.Info(r, XML.Elem(Markup(Markup.CLASS_PARAMETER, _), body))) =>
+ Some(add(prev, r, (true, Pretty.block(0, body))))
+
+ case (prev, Text.Info(r, XML.Elem(Markup(Markup.ML_TYPING, _), body))) =>
+ Some(add(prev, r, (false, Rendering.pretty_typing("ML:", body))))
+
+ case (prev, Text.Info(r, Protocol.ML_Breakpoint(breakpoint))) =>
+ val text =
+ if (Debugger.breakpoint_state(breakpoint)) "breakpoint (enabled)"
+ else "breakpoint (disabled)"
+ Some(add(prev, r, (true, XML.Text(text))))
+
+ case (prev, Text.Info(r, XML.Elem(Markup.Language(language, _, _, _), _))) =>
+ val lang = Word.implode(Word.explode('_', language))
+ Some(add(prev, r, (true, XML.Text("language: " + lang))))
+
+ case (prev, Text.Info(r, XML.Elem(Markup.Expression(kind), _))) =>
+ val descr = if (kind == "") "expression" else "expression: " + kind
+ Some(add(prev, r, (true, XML.Text(descr))))
+
+ case (prev, Text.Info(r, XML.Elem(Markup(Markup.MARKDOWN_PARAGRAPH, _), _))) =>
+ Some(add(prev, r, (true, XML.Text("Markdown: paragraph"))))
+ case (prev, Text.Info(r, XML.Elem(Markup.Markdown_List(kind), _))) =>
+ Some(add(prev, r, (true, XML.Text("Markdown: " + kind))))
+
+ case (prev, Text.Info(r, XML.Elem(Markup(name, _), _))) =>
+ Rendering.tooltip_descriptions.get(name).
+ map(descr => add(prev, r, (true, XML.Text(descr))))
+ }).map(_.info)
+
+ results.map(_.info).flatMap(res => res._2.toList) match {
+ case Nil => None
+ case tips =>
+ val r = Text.Range(results.head.range.start, results.last.range.stop)
+ val all_tips = (tips.filter(_._1) ++ tips.filter(!_._1).lastOption.toList).map(_._2)
+ Some(Text.Info(r, Library.separate(Pretty.fbrk, all_tips)))
+ }
+ }
+}
--- a/src/Pure/build-jars Tue Dec 20 21:35:56 2016 +0100
+++ b/src/Pure/build-jars Tue Dec 20 22:24:16 2016 +0100
@@ -94,6 +94,7 @@
PIDE/protocol_message.scala
PIDE/prover.scala
PIDE/query_operation.scala
+ PIDE/rendering.scala
PIDE/resources.scala
PIDE/session.scala
PIDE/text.scala
@@ -162,6 +163,7 @@
../Tools/VSCode/src/protocol.scala
../Tools/VSCode/src/server.scala
../Tools/VSCode/src/uri_resources.scala
+ ../Tools/VSCode/src/vscode_rendering.scala
)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/VSCode/etc/options Tue Dec 20 22:24:16 2016 +0100
@@ -0,0 +1,7 @@
+(* :mode=isabelle-options: *)
+
+option vscode_tooltip_margin : int = 60
+ -- "margin for tooltip pretty-printing"
+
+option vscode_timing_threshold : real = 0.1
+ -- "default threshold for timing display (seconds)"
--- a/src/Tools/VSCode/src/document_model.scala Tue Dec 20 21:35:56 2016 +0100
+++ b/src/Tools/VSCode/src/document_model.scala Tue Dec 20 22:24:16 2016 +0100
@@ -52,7 +52,10 @@
def unchanged: Document_Model = if (changed) copy(changed = false) else this
- /* snapshot */
+ /* snapshot and rendering */
def snapshot(): Document.Snapshot = session.snapshot(node_name, text_edits)
+
+ def rendering(options: Options): VSCode_Rendering =
+ new VSCode_Rendering(snapshot(), options, session.resources)
}
--- a/src/Tools/VSCode/src/server.scala Tue Dec 20 21:35:56 2016 +0100
+++ b/src/Tools/VSCode/src/server.scala Tue Dec 20 22:24:16 2016 +0100
@@ -188,125 +188,21 @@
}
- /* tooltips -- see $ISABELLE_HOME/src/Tools/jEdit/rendering.scala */
+ /* hover */
def hover(uri: String, pos: Line.Position): Option[(Line.Range, List[String])] =
for {
model <- state.value.models.get(uri)
- snapshot = model.snapshot()
+ rendering = model.rendering(options)
offset <- model.doc.offset(pos, text_length)
- info <- tooltip(snapshot, Text.Range(offset, offset + 1))
+ info <- rendering.tooltip(Text.Range(offset, offset + 1))
} yield {
val start = model.doc.position(info.range.start, text_length)
val stop = model.doc.position(info.range.stop, text_length)
- val s = Pretty.string_of(info.info, margin = tooltip_margin.toDouble)
+ val s = Pretty.string_of(info.info, margin = rendering.tooltip_margin)
(Line.Range(start, stop), List("```\n" + s + "\n```"))
}
- private val tooltip_descriptions =
- Map(
- Markup.CITATION -> "citation",
- Markup.TOKEN_RANGE -> "inner syntax token",
- Markup.FREE -> "free variable",
- Markup.SKOLEM -> "skolem variable",
- Markup.BOUND -> "bound variable",
- Markup.VAR -> "schematic variable",
- Markup.TFREE -> "free type variable",
- Markup.TVAR -> "schematic type variable")
-
- private val tooltip_elements =
- Markup.Elements(Markup.LANGUAGE, Markup.EXPRESSION, Markup.TIMING, Markup.ENTITY,
- Markup.SORTING, Markup.TYPING, Markup.CLASS_PARAMETER, Markup.ML_TYPING,
- Markup.ML_BREAKPOINT, Markup.PATH, Markup.DOC, Markup.URL, Markup.MARKDOWN_PARAGRAPH,
- Markup.Markdown_List.name) ++ Markup.Elements(tooltip_descriptions.keySet)
-
- private def pretty_typing(kind: String, body: XML.Body): XML.Tree =
- Pretty.block(XML.Text(kind) :: Pretty.brk(1) :: body)
-
- private def timing_threshold: Double = options.real("jedit_timing_threshold")
-
- def tooltip(snapshot: Document.Snapshot, range: Text.Range): Option[Text.Info[XML.Body]] =
- {
- def add(prev: Text.Info[(Timing, Vector[(Boolean, XML.Tree)])],
- r0: Text.Range, p: (Boolean, XML.Tree)): Text.Info[(Timing, Vector[(Boolean, XML.Tree)])] =
- {
- val r = snapshot.convert(r0)
- val (t, info) = prev.info
- if (prev.range == r)
- Text.Info(r, (t, info :+ p))
- else Text.Info(r, (t, Vector(p)))
- }
-
- val results =
- snapshot.cumulate[Text.Info[(Timing, Vector[(Boolean, XML.Tree)])]](
- range, Text.Info(range, (Timing.zero, Vector.empty)), tooltip_elements, _ =>
- {
- case (Text.Info(r, (t1, info)), Text.Info(_, XML.Elem(Markup.Timing(t2), _))) =>
- Some(Text.Info(r, (t1 + t2, info)))
-
- case (prev, Text.Info(r, XML.Elem(Markup.Entity(kind, name), _)))
- if kind != "" &&
- kind != Markup.ML_DEF &&
- kind != Markup.ML_OPEN &&
- kind != Markup.ML_STRUCTURE =>
- val kind1 = Word.implode(Word.explode('_', kind))
- val txt1 =
- if (name == "") kind1
- else if (kind1 == "") quote(name)
- else kind1 + " " + quote(name)
- val t = prev.info._1
- val txt2 =
- if (kind == Markup.COMMAND && t.elapsed.seconds >= timing_threshold)
- "\n" + t.message
- else ""
- Some(add(prev, r, (true, XML.Text(txt1 + txt2))))
-
- case (prev, Text.Info(r, XML.Elem(Markup.Doc(name), _))) =>
- val text = "doc " + quote(name)
- Some(add(prev, r, (true, XML.Text(text))))
-
- case (prev, Text.Info(r, XML.Elem(Markup.Url(name), _))) =>
- Some(add(prev, r, (true, XML.Text("URL " + quote(name)))))
-
- case (prev, Text.Info(r, XML.Elem(Markup(name, _), body)))
- if name == Markup.SORTING || name == Markup.TYPING =>
- Some(add(prev, r, (true, pretty_typing("::", body))))
-
- case (prev, Text.Info(r, XML.Elem(Markup(Markup.CLASS_PARAMETER, _), body))) =>
- Some(add(prev, r, (true, Pretty.block(0, body))))
-
- case (prev, Text.Info(r, XML.Elem(Markup(Markup.ML_TYPING, _), body))) =>
- Some(add(prev, r, (false, pretty_typing("ML:", body))))
-
- case (prev, Text.Info(r, XML.Elem(Markup.Language(language, _, _, _), _))) =>
- val lang = Word.implode(Word.explode('_', language))
- Some(add(prev, r, (true, XML.Text("language: " + lang))))
-
- case (prev, Text.Info(r, XML.Elem(Markup.Expression(kind), _))) =>
- val descr = if (kind == "") "expression" else "expression: " + kind
- Some(add(prev, r, (true, XML.Text(descr))))
-
- case (prev, Text.Info(r, XML.Elem(Markup(Markup.MARKDOWN_PARAGRAPH, _), _))) =>
- Some(add(prev, r, (true, XML.Text("Markdown: paragraph"))))
- case (prev, Text.Info(r, XML.Elem(Markup.Markdown_List(kind), _))) =>
- Some(add(prev, r, (true, XML.Text("Markdown: " + kind))))
-
- case (prev, Text.Info(r, XML.Elem(Markup(name, _), _))) =>
- tooltip_descriptions.get(name).
- map(descr => add(prev, r, (true, XML.Text(descr))))
- }).map(_.info)
-
- results.map(_.info).flatMap(res => res._2.toList) match {
- case Nil => None
- case tips =>
- val r = Text.Range(results.head.range.start, results.last.range.stop)
- val all_tips = (tips.filter(_._1) ++ tips.filter(!_._1).lastOption.toList).map(_._2)
- Some(Text.Info(r, Library.separate(Pretty.fbrk, all_tips)))
- }
- }
-
- def tooltip_margin: Int = options.int("jedit_tooltip_margin")
-
/* main loop */
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/VSCode/src/vscode_rendering.scala Tue Dec 20 22:24:16 2016 +0100
@@ -0,0 +1,21 @@
+/* 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._
+
+
+class VSCode_Rendering(snapshot: Document.Snapshot, options: Options, 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")
+}
--- a/src/Tools/jEdit/src/jedit_rendering.scala Tue Dec 20 21:35:56 2016 +0100
+++ b/src/Tools/jEdit/src/jedit_rendering.scala Tue Dec 20 22:24:16 2016 +0100
@@ -1,7 +1,7 @@
-/* Title: Tools/jEdit/src/rendering.scala
+/* Title: Tools/jEdit/src/jedit_rendering.scala
Author: Makarius
-Isabelle-specific implementation of quasi-abstract rendering and
+Isabelle/jEdit-specific implementation of quasi-abstract rendering and
markup interpretation.
*/
@@ -175,23 +175,6 @@
Markup.Elements(Markup.WRITELN, Markup.INFORMATION, Markup.WARNING, Markup.LEGACY, Markup.ERROR,
Markup.BAD)
- private val tooltip_descriptions =
- Map(
- Markup.CITATION -> "citation",
- Markup.TOKEN_RANGE -> "inner syntax token",
- Markup.FREE -> "free variable",
- Markup.SKOLEM -> "skolem variable",
- Markup.BOUND -> "bound variable",
- Markup.VAR -> "schematic variable",
- Markup.TFREE -> "free type variable",
- Markup.TVAR -> "schematic type variable")
-
- private val tooltip_elements =
- Markup.Elements(Markup.LANGUAGE, Markup.EXPRESSION, Markup.TIMING, Markup.ENTITY,
- Markup.SORTING, Markup.TYPING, Markup.CLASS_PARAMETER, Markup.ML_TYPING,
- Markup.ML_BREAKPOINT, Markup.PATH, Markup.DOC, Markup.URL, Markup.MARKDOWN_PARAGRAPH,
- Markup.Markdown_List.name) ++ Markup.Elements(tooltip_descriptions.keySet)
-
private val gutter_elements =
Markup.Elements(Markup.WRITELN, Markup.INFORMATION, Markup.WARNING, Markup.LEGACY, Markup.ERROR)
@@ -226,11 +209,9 @@
}
-class JEdit_Rendering private(val snapshot: Document.Snapshot, val options: Options)
+class JEdit_Rendering(snapshot: Document.Snapshot, options: Options)
+ extends Rendering(snapshot, options, PIDE.resources)
{
- override def toString: String = "Rendering(" + snapshot.toString + ")"
-
-
/* colors */
def color_value(s: String): Color = Color_Value(options.string(s))
@@ -479,18 +460,13 @@
/* hyperlinks */
- private def jedit_file(name: String): String =
- if (Path.is_valid(name))
- PIDE.resources.append(snapshot.node_name.master_dir, Path.explode(name))
- else name
-
def hyperlink(range: Text.Range): Option[Text.Info[PIDE.editor.Hyperlink]] =
{
snapshot.cumulate[Vector[Text.Info[PIDE.editor.Hyperlink]]](
range, Vector.empty, JEdit_Rendering.hyperlink_elements, _ =>
{
case (links, Text.Info(info_range, XML.Elem(Markup.Path(name), _))) =>
- val link = PIDE.editor.hyperlink_file(true, jedit_file(name))
+ val link = PIDE.editor.hyperlink_file(true, resolve_file(name))
Some(links :+ Text.Info(snapshot.convert(info_range), link))
case (links, Text.Info(info_range, XML.Elem(Markup.Doc(name), _))) =>
@@ -580,105 +556,8 @@
/* tooltips */
- private def pretty_typing(kind: String, body: XML.Body): XML.Tree =
- Pretty.block(XML.Text(kind) :: Pretty.brk(1) :: body)
-
- private def timing_threshold: Double = options.real("jedit_timing_threshold")
-
- def tooltip(range: Text.Range): Option[Text.Info[XML.Body]] =
- {
- def add(prev: Text.Info[(Timing, Vector[(Boolean, XML.Tree)])],
- r0: Text.Range, p: (Boolean, XML.Tree)): Text.Info[(Timing, Vector[(Boolean, XML.Tree)])] =
- {
- val r = snapshot.convert(r0)
- val (t, info) = prev.info
- if (prev.range == r)
- Text.Info(r, (t, info :+ p))
- else Text.Info(r, (t, Vector(p)))
- }
-
- val results =
- snapshot.cumulate[Text.Info[(Timing, Vector[(Boolean, XML.Tree)])]](
- range, Text.Info(range, (Timing.zero, Vector.empty)), JEdit_Rendering.tooltip_elements, _ =>
- {
- case (Text.Info(r, (t1, info)), Text.Info(_, XML.Elem(Markup.Timing(t2), _))) =>
- Some(Text.Info(r, (t1 + t2, info)))
-
- case (prev, Text.Info(r, XML.Elem(Markup.Entity(kind, name), _)))
- if kind != "" &&
- kind != Markup.ML_DEF &&
- kind != Markup.ML_OPEN &&
- kind != Markup.ML_STRUCTURE =>
- val kind1 = Word.implode(Word.explode('_', kind))
- val txt1 =
- if (name == "") kind1
- else if (kind1 == "") quote(name)
- else kind1 + " " + quote(name)
- val t = prev.info._1
- val txt2 =
- if (kind == Markup.COMMAND && t.elapsed.seconds >= timing_threshold)
- "\n" + t.message
- else ""
- Some(add(prev, r, (true, XML.Text(txt1 + txt2))))
-
- case (prev, Text.Info(r, XML.Elem(Markup.Path(name), _))) =>
- val file = jedit_file(name)
- val text =
- if (name == file) "file " + quote(file)
- else "path " + quote(name) + "\nfile " + quote(file)
- Some(add(prev, r, (true, XML.Text(text))))
-
- case (prev, Text.Info(r, XML.Elem(Markup.Doc(name), _))) =>
- val text = "doc " + quote(name)
- Some(add(prev, r, (true, XML.Text(text))))
-
- case (prev, Text.Info(r, XML.Elem(Markup.Url(name), _))) =>
- Some(add(prev, r, (true, XML.Text("URL " + quote(name)))))
-
- case (prev, Text.Info(r, XML.Elem(Markup(name, _), body)))
- if name == Markup.SORTING || name == Markup.TYPING =>
- Some(add(prev, r, (true, pretty_typing("::", body))))
-
- case (prev, Text.Info(r, XML.Elem(Markup(Markup.CLASS_PARAMETER, _), body))) =>
- Some(add(prev, r, (true, Pretty.block(0, body))))
-
- case (prev, Text.Info(r, XML.Elem(Markup(Markup.ML_TYPING, _), body))) =>
- Some(add(prev, r, (false, pretty_typing("ML:", body))))
-
- case (prev, Text.Info(r, Protocol.ML_Breakpoint(breakpoint))) =>
- val text =
- if (Debugger.breakpoint_state(breakpoint)) "breakpoint (enabled)"
- else "breakpoint (disabled)"
- Some(add(prev, r, (true, XML.Text(text))))
-
- case (prev, Text.Info(r, XML.Elem(Markup.Language(language, _, _, _), _))) =>
- val lang = Word.implode(Word.explode('_', language))
- Some(add(prev, r, (true, XML.Text("language: " + lang))))
-
- case (prev, Text.Info(r, XML.Elem(Markup.Expression(kind), _))) =>
- val descr = if (kind == "") "expression" else "expression: " + kind
- Some(add(prev, r, (true, XML.Text(descr))))
-
- case (prev, Text.Info(r, XML.Elem(Markup(Markup.MARKDOWN_PARAGRAPH, _), _))) =>
- Some(add(prev, r, (true, XML.Text("Markdown: paragraph"))))
- case (prev, Text.Info(r, XML.Elem(Markup.Markdown_List(kind), _))) =>
- Some(add(prev, r, (true, XML.Text("Markdown: " + kind))))
-
- case (prev, Text.Info(r, XML.Elem(Markup(name, _), _))) =>
- JEdit_Rendering.tooltip_descriptions.get(name).
- map(descr => add(prev, r, (true, XML.Text(descr))))
- }).map(_.info)
-
- results.map(_.info).flatMap(res => res._2.toList) match {
- case Nil => None
- case tips =>
- val r = Text.Range(results.head.range.start, results.last.range.stop)
- val all_tips = (tips.filter(_._1) ++ tips.filter(!_._1).lastOption.toList).map(_._2)
- Some(Text.Info(r, Library.separate(Pretty.fbrk, all_tips)))
- }
- }
-
def tooltip_margin: Int = options.int("jedit_tooltip_margin")
+ def timing_threshold: Double = options.real("jedit_timing_threshold")
lazy val tooltip_close_icon = JEdit_Lib.load_icon(options.string("tooltip_close_icon"))
lazy val tooltip_detach_icon = JEdit_Lib.load_icon(options.string("tooltip_detach_icon"))