--- a/src/Tools/jEdit/plugin/Isabelle.props Sun May 30 23:40:24 2010 +0200
+++ b/src/Tools/jEdit/plugin/Isabelle.props Sun May 30 23:42:03 2010 +0200
@@ -27,6 +27,8 @@
options.isabelle.logic.title=Logic
options.isabelle.relative-font-size.title=Relative Font Size
options.isabelle.relative-font-size=100
+options.isabelle.tooltip-font-size.title=Tooltip Font Size
+options.isabelle.tooltip-font-size=4
options.isabelle.startup-timeout=10000
#menu actions
--- a/src/Tools/jEdit/src/jedit/document_view.scala Sun May 30 23:40:24 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/document_view.scala Sun May 30 23:42:03 2010 +0200
@@ -131,7 +131,10 @@
val offset = model.from_current(document, text_area.xyToOffset(x, y))
document.command_at(offset) match {
case Some((command, command_start)) =>
- document.current_state(command).type_at(offset - command_start) getOrElse null
+ document.current_state(command).type_at(offset - command_start) match {
+ case Some(text) => Isabelle.tooltip(text)
+ case None => null
+ }
case None => null
}
}
--- a/src/Tools/jEdit/src/jedit/isabelle_options.scala Sun May 30 23:40:24 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/isabelle_options.scala Sun May 30 23:42:03 2010 +0200
@@ -16,6 +16,7 @@
{
private val logic_name = new JComboBox()
private val relative_font_size = new JSpinner()
+ private val tooltip_font_size = new JSpinner()
private class List_Item(val name: String, val descr: String) {
def this(name: String) = this(name, name)
@@ -37,9 +38,14 @@
})
addComponent(Isabelle.Property("relative-font-size.title"), {
- relative_font_size.setValue(Isabelle.Int_Property("relative-font-size"))
+ relative_font_size.setValue(Isabelle.Int_Property("relative-font-size", 100))
relative_font_size
})
+
+ addComponent(Isabelle.Property("tooltip-font-size.title"), {
+ tooltip_font_size.setValue(Isabelle.Int_Property("tooltip-font-size", 4))
+ tooltip_font_size
+ })
}
override def _save()
@@ -49,5 +55,8 @@
Isabelle.Int_Property("relative-font-size") =
relative_font_size.getValue().asInstanceOf[Int]
+
+ Isabelle.Int_Property("tooltip-font-size") =
+ tooltip_font_size.getValue().asInstanceOf[Int]
}
}
--- a/src/Tools/jEdit/src/jedit/plugin.scala Sun May 30 23:40:24 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/plugin.scala Sun May 30 23:42:03 2010 +0200
@@ -81,6 +81,20 @@
Int_Property("relative-font-size", 100)).toFloat / 100
+ /* tooltip markup */
+
+ // raw font markup
+
+ def font(name: String, size: Int, body: List[XML.Tree]): XML.Tree =
+ XML.Elem("font", List(("face", name), ("size", size.toString)), body)
+
+
+ def tooltip(text: String): String =
+ "<html><font face=\"" + font_family() + "\" size=\"" +
+ Int_Property("tooltip-font-size", 4).toString + "\">" +
+ HTML.encode(text) + "</font></html>"
+
+
/* settings */
def default_logic(): String =