# 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]
   }