# HG changeset patch # User wenzelm # Date 1288883713 -3600 # Node ID 088e5adca5ad4614b7b7efcc385d919786f631a6 # Parent e2f03de2b3c79bd7ea2c36c433a0476f60ab1ad8 added property "tooltip-margin"; diff -r e2f03de2b3c7 -r 088e5adca5ad src/Tools/jEdit/plugin/Isabelle.props --- 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 diff -r e2f03de2b3c7 -r 088e5adca5ad src/Tools/jEdit/src/jedit/isabelle_markup.scala --- 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" diff -r e2f03de2b3c7 -r 088e5adca5ad src/Tools/jEdit/src/jedit/isabelle_options.scala --- 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] }