# HG changeset patch # User wenzelm # Date 1275255723 -7200 # Node ID 8517a650cfdc2dda993e2f0c8d9c5e3ee0720027 # Parent 0f3edc64356a1d9e1ca71ff0dd3f00cdba34797e control tooltip font via Swing HTML, with tooltip-font-size property; diff -r 0f3edc64356a -r 8517a650cfdc src/Tools/jEdit/plugin/Isabelle.props --- 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 diff -r 0f3edc64356a -r 8517a650cfdc src/Tools/jEdit/src/jedit/document_view.scala --- 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 } } diff -r 0f3edc64356a -r 8517a650cfdc src/Tools/jEdit/src/jedit/isabelle_options.scala --- 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] } } diff -r 0f3edc64356a -r 8517a650cfdc src/Tools/jEdit/src/jedit/plugin.scala --- 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.encode(text) + "" + + /* settings */ def default_logic(): String =