| changeset 53786 | 064cb0458071 |
| parent 53785 | e64edcc2f8bf |
| child 53848 | 8d7029eb0c31 |
--- a/src/Pure/GUI/gui.scala Sun Sep 22 18:36:22 2013 +0200 +++ b/src/Pure/GUI/gui.scala Sun Sep 22 18:42:18 2013 +0200 @@ -109,6 +109,13 @@ } + /* tooltip with multi-line support */ + + def tooltip_lines(lines: List[String]): String = + if (lines.isEmpty) null + else "<html><pre>" + HTML.encode(cat_lines(lines)) + "</pre></html>" + + /* screen resolution */ def resolution_scale(): Double = Toolkit.getDefaultToolkit.getScreenResolution.toDouble / 72