src/Tools/jEdit/src/jedit/isabelle_options.scala

 {
   private val logic_selector = Isabelle.logic_selector(Isabelle.Property("logic"))
   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()
   {
     addComponent(Isabelle.Property("logic.title"), logic_selector.peer)

     relative_font_size.setValue(Isabelle.Int_Property("relative-font-size", 100))
     addComponent(Isabelle.Property("relative-font-size.title"), relative_font_size)
 
     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)
   }
 

       relative_font_size.getValue().asInstanceOf[Int]
 
     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]
   }
 }