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