src/Tools/jEdit/src/jedit_options.scala

             }
           })
         text_area
       }
     component.load()
-    component.tooltip = opt.print
+    component.tooltip = Isabelle.tooltip(opt.print)
     component
   }
 }