# HG changeset patch # User wenzelm # Date 1397927012 -7200 # Node ID 891d1b8b64fb7655b5d531350c3d19551ed0f74d # Parent 798ba1c2da12cabcd085dd34cc0e9641c325081a clarified tooltip_lines: HTML.encode already takes care of newline (but not space); diff -r 798ba1c2da12 -r 891d1b8b64fb src/Pure/GUI/gui.scala --- a/src/Pure/GUI/gui.scala Sat Apr 19 18:37:41 2014 +0200 +++ b/src/Pure/GUI/gui.scala Sat Apr 19 19:03:32 2014 +0200 @@ -137,9 +137,9 @@ /* tooltip with multi-line support */ - def tooltip_lines(lines: List[String]): String = - if (lines.isEmpty) null - else "
" + HTML.encode(cat_lines(lines)) + "
" + def tooltip_lines(text: String): String = + if (text == null || text == "") null + else "" + HTML.encode(text) + "" /* screen resolution */ diff -r 798ba1c2da12 -r 891d1b8b64fb src/Tools/jEdit/src/find_dockable.scala --- a/src/Tools/jEdit/src/find_dockable.scala Sat Apr 19 18:37:41 2014 +0200 +++ b/src/Tools/jEdit/src/find_dockable.scala Sat Apr 19 19:03:32 2014 +0200 @@ -106,10 +106,8 @@ private val query_label = new Label("Search criteria:") { tooltip = - GUI.tooltip_lines(List( - "Search criteria for find operation, e.g.", - "", - " \"_ = _\" \"op +\" name: Group -name: monoid")) + GUI.tooltip_lines( + "Search criteria for find operation, e.g.\n\"_ = _\" \"op +\" name: Group -name: monoid") } private val query = new Completion_Popup.History_Text_Field("isabelle-find-theorems") { diff -r 798ba1c2da12 -r 891d1b8b64fb src/Tools/jEdit/src/jedit_options.scala --- a/src/Tools/jEdit/src/jedit_options.scala Sat Apr 19 18:37:41 2014 +0200 +++ b/src/Tools/jEdit/src/jedit_options.scala Sat Apr 19 19:03:32 2014 +0200 @@ -49,7 +49,7 @@ def load = button.setSelectedColor(Color_Value(string(opt_name))) def save = string(opt_name) = Color_Value.print(button.getSelectedColor) } - component.tooltip = GUI.tooltip_lines(List(opt.print_default)) + component.tooltip = GUI.tooltip_lines(opt.print_default) component } @@ -96,7 +96,7 @@ text_area } component.load() - component.tooltip = GUI.tooltip_lines(List(opt.print_default)) + component.tooltip = GUI.tooltip_lines(opt.print_default) component } diff -r 798ba1c2da12 -r 891d1b8b64fb src/Tools/jEdit/src/sledgehammer_dockable.scala --- a/src/Tools/jEdit/src/sledgehammer_dockable.scala Sat Apr 19 18:37:41 2014 +0200 +++ b/src/Tools/jEdit/src/sledgehammer_dockable.scala Sat Apr 19 19:03:32 2014 +0200 @@ -137,10 +137,8 @@ private val provers_label = new Label("Provers:") { tooltip = - GUI.tooltip_lines(List( - "Automatic provers as space-separated list, e.g.", - "", - " e spass remote_vampire")) + GUI.tooltip_lines( + "Automatic provers as space-separated list, e.g.\ne spass remote_vampire") } private val provers = new HistoryTextField("isabelle-sledgehammer-provers") { diff -r 798ba1c2da12 -r 891d1b8b64fb src/Tools/jEdit/src/spell_checker.scala --- a/src/Tools/jEdit/src/spell_checker.scala Sat Apr 19 18:37:41 2014 +0200 +++ b/src/Tools/jEdit/src/spell_checker.scala Sat Apr 19 19:03:32 2014 +0200 @@ -126,7 +126,7 @@ } component.load() - component.tooltip = GUI.tooltip_lines(List(opt.print_default)) + component.tooltip = GUI.tooltip_lines(opt.print_default) component } diff -r 798ba1c2da12 -r 891d1b8b64fb src/Tools/jEdit/src/symbols_dockable.scala --- a/src/Tools/jEdit/src/symbols_dockable.scala Sat Apr 19 18:37:41 2014 +0200 +++ b/src/Tools/jEdit/src/symbols_dockable.scala Sat Apr 19 19:03:32 2014 +0200 @@ -41,7 +41,9 @@ else text_area.setSelectedText(decoded) text_area.requestFocus } - tooltip = GUI.tooltip_lines(symbol :: Symbol.abbrevs.get_list(symbol).map(a => "abbrev: " + a)) + tooltip = + GUI.tooltip_lines( + cat_lines(symbol :: Symbol.abbrevs.get_list(symbol).map(a => "abbrev: " + a))) } private class Reset_Component extends Button