# HG changeset patch # User wenzelm # Date 1347299768 -7200 # Node ID bff772033a97b358c876a2c785bec1b9d3baab8a # Parent ffd9ad9dc35b44e103ae1760f529aab8eae3d720 proper multi-line tooltip; diff -r ffd9ad9dc35b -r bff772033a97 src/Tools/jEdit/src/isabelle_logic.scala --- a/src/Tools/jEdit/src/isabelle_logic.scala Mon Sep 10 19:49:30 2012 +0200 +++ b/src/Tools/jEdit/src/isabelle_logic.scala Mon Sep 10 19:56:08 2012 +0200 @@ -53,7 +53,7 @@ component.listenTo(component.selection) component.reactions += { case SelectionChanged(_) => component.save() } } - component.tooltip = Isabelle.options.value.check_name("jedit_logic").print + component.tooltip = Isabelle.tooltip(Isabelle.options.value.check_name("jedit_logic").print) component } diff -r ffd9ad9dc35b -r bff772033a97 src/Tools/jEdit/src/jedit_options.scala --- a/src/Tools/jEdit/src/jedit_options.scala Mon Sep 10 19:49:30 2012 +0200 +++ b/src/Tools/jEdit/src/jedit_options.scala Mon Sep 10 19:56:08 2012 +0200 @@ -58,7 +58,7 @@ text_area } component.load() - component.tooltip = opt.print + component.tooltip = Isabelle.tooltip(opt.print) component } }