src/Tools/jEdit/src/isabelle.scala
changeset 71504 f2a79950748e
parent 71502 f61e55bab00c
child 71520 62755ec99671
equal deleted inserted replaced
71503:df7494f14388 71504:f2a79950748e
   530       doc_view <- Document_View.get(text_area)
   530       doc_view <- Document_View.get(text_area)
   531       rendering = doc_view.get_rendering()
   531       rendering = doc_view.get_rendering()
   532       tip <- rendering.tooltip(caret_range, control)
   532       tip <- rendering.tooltip(caret_range, control)
   533       loc0 <- Option(text_area.offsetToXY(caret_range.start))
   533       loc0 <- Option(text_area.offsetToXY(caret_range.start))
   534     } {
   534     } {
   535       val loc = new Point(loc0.x, loc0.y + painter.getLineHeight / 2)
   535       val loc = new Point(loc0.x, loc0.y + painter.getLineHeight * 3 / 4)
   536       val results = rendering.snapshot.command_results(tip.range)
   536       val results = rendering.snapshot.command_results(tip.range)
   537       Pretty_Tooltip(view, painter, loc, rendering, results, tip)
   537       Pretty_Tooltip(view, painter, loc, rendering, results, tip)
   538     }
   538     }
   539   }
   539   }
   540 
   540