--- a/src/Tools/jEdit/plugin/Isabelle.props Thu Nov 04 10:58:03 2010 +0100
+++ b/src/Tools/jEdit/plugin/Isabelle.props Thu Nov 04 16:15:13 2010 +0100
@@ -29,6 +29,8 @@
options.isabelle.relative-font-size=100
options.isabelle.tooltip-font-size.title=Tooltip Font Size
options.isabelle.tooltip-font-size=10
+options.isabelle.tooltip-margin.title=Tooltip Margin
+options.isabelle.tooltip-margin=40
options.isabelle.tooltip-dismiss-delay.title=Tooltip Dismiss Delay (global)
options.isabelle.tooltip-dismiss-delay=8000
options.isabelle.startup-timeout=10000
--- a/src/Tools/jEdit/src/jedit/isabelle_markup.scala Thu Nov 04 10:58:03 2010 +0100
+++ b/src/Tools/jEdit/src/jedit/isabelle_markup.scala Thu Nov 04 16:15:13 2010 +0100
@@ -88,7 +88,7 @@
{
case Text.Info(_, msg @ XML.Elem(Markup(markup, _), _))
if markup == Markup.WRITELN || markup == Markup.WARNING || markup == Markup.ERROR =>
- Pretty.string_of(List(msg), margin = 40)
+ Pretty.string_of(List(msg), margin = Isabelle.Int_Property("tooltip-margin"))
}
val gutter_message: Markup_Tree.Select[Icon] =
@@ -110,7 +110,8 @@
val tooltip: Markup_Tree.Select[String] =
{
case Text.Info(_, XML.Elem(Markup(Markup.ML_TYPING, _), body)) =>
- Pretty.string_of(List(Pretty.block(XML.Text("ML:") :: Pretty.Break(1) :: body)), margin = 40)
+ Pretty.string_of(List(Pretty.block(XML.Text("ML:") :: Pretty.Break(1) :: body)),
+ margin = Isabelle.Int_Property("tooltip-margin"))
case Text.Info(_, XML.Elem(Markup(Markup.SORT, _), _)) => "sort"
case Text.Info(_, XML.Elem(Markup(Markup.TYP, _), _)) => "type"
case Text.Info(_, XML.Elem(Markup(Markup.TERM, _), _)) => "term"
--- a/src/Tools/jEdit/src/jedit/isabelle_options.scala Thu Nov 04 10:58:03 2010 +0100
+++ b/src/Tools/jEdit/src/jedit/isabelle_options.scala Thu Nov 04 16:15:13 2010 +0100
@@ -20,6 +20,7 @@
private val auto_start = new CheckBox()
private val relative_font_size = new JSpinner()
private val tooltip_font_size = new JSpinner()
+ private val tooltip_margin = new JSpinner()
private val tooltip_dismiss_delay = new JSpinner()
override def _init()
@@ -35,6 +36,9 @@
tooltip_font_size.setValue(Isabelle.Int_Property("tooltip-font-size", 10))
addComponent(Isabelle.Property("tooltip-font-size.title"), tooltip_font_size)
+ tooltip_margin.setValue(Isabelle.Int_Property("tooltip-margin", 40))
+ addComponent(Isabelle.Property("tooltip-margin.title"), tooltip_margin)
+
tooltip_dismiss_delay.setValue(Isabelle.Int_Property("tooltip-dismiss-delay", 8000))
addComponent(Isabelle.Property("tooltip-dismiss-delay.title"), tooltip_dismiss_delay)
}
@@ -51,6 +55,9 @@
Isabelle.Int_Property("tooltip-font-size") =
tooltip_font_size.getValue().asInstanceOf[Int]
+ Isabelle.Int_Property("tooltip-margin") =
+ tooltip_margin.getValue().asInstanceOf[Int]
+
Isabelle.Int_Property("tooltip-dismiss-delay") =
tooltip_dismiss_delay.getValue().asInstanceOf[Int]
}