src/Tools/jEdit/src/pretty_tooltip.scala
changeset 49844 19ea3242ec37
parent 49842 a974f66062c8
child 50146 03f38212442a
equal deleted inserted replaced
49843:afddf4e26fac 49844:19ea3242ec37
   111       XML.traverse_text(Pretty.formatted(body, margin, Pretty.font_metric(font_metrics)))(0)(
   111       XML.traverse_text(Pretty.formatted(body, margin, Pretty.font_metric(font_metrics)))(0)(
   112         (n: Int, s: String) => n + s.iterator.filter(_ == '\n').length)
   112         (n: Int, s: String) => n + s.iterator.filter(_ == '\n').length)
   113 
   113 
   114     val screen = Toolkit.getDefaultToolkit.getScreenSize
   114     val screen = Toolkit.getDefaultToolkit.getScreenSize
   115     val w = (font_metrics.charWidth(Pretty.spc) * margin) min (screen.width / 2)
   115     val w = (font_metrics.charWidth(Pretty.spc) * margin) min (screen.width / 2)
   116     val h = (font_metrics.getHeight * (lines + 3)) min (screen.height / 2)
   116     val h = (font_metrics.getHeight * (lines + 2) + 25) min (screen.height / 2)
   117     window.setSize(w, h)
   117     window.setSize(w, h)
   118   }
   118   }
   119 
   119 
   120   {
   120   {
   121     val point = new Point(mouse_x, mouse_y)
   121     val point = new Point(mouse_x, mouse_y)