src/Tools/jEdit/src/rich_text_area.scala
Sun, 25 Nov 2012 18:47:33 +0100 wenzelm quasi-abstract module Rendering, with Isabelle-specific implementation;
Thu, 22 Nov 2012 14:53:02 +0100 wenzelm reset active area for outdated snapshot (again?);
Thu, 22 Nov 2012 14:40:39 +0100 wenzelm some support for implicit senback, meaning that it uses the caret position instead of explicit command exec_id;
Fri, 19 Oct 2012 21:52:45 +0200 wenzelm more precise pixel_range: avoid popup when pointing into empty space after actual end-of-line;
Fri, 12 Oct 2012 23:38:48 +0200 wenzelm further refinement of jEdit line range, avoiding lack of final \n;
Mon, 08 Oct 2012 12:40:35 +0200 wenzelm use Pretty_Tooltip for Graphview_Panel;
Thu, 04 Oct 2012 20:14:40 +0200 wenzelm separate module Pretty_Tooltip;
Thu, 04 Oct 2012 19:31:50 +0200 wenzelm refined rich tooltip options;
Thu, 04 Oct 2012 18:28:31 +0200 wenzelm Rich_Text_Area tooltips via nested Pretty_Text_Area, based on some techniques of FoldViewer plugin;
Fri, 21 Sep 2012 16:50:44 +0200 wenzelm more realistic sendback: pick exec_id from message position and text from buffer;
Fri, 21 Sep 2012 15:39:51 +0200 wenzelm some support for hovering and sendback area;
Thu, 20 Sep 2012 22:25:30 +0200 wenzelm tuned painter;
Thu, 20 Sep 2012 21:31:56 +0200 wenzelm tuned rendering;
Wed, 19 Sep 2012 12:10:40 +0200 wenzelm more robust GUI component handlers;
Mon, 17 Sep 2012 20:34:19 +0200 wenzelm renamed Text_Area_Painter to Rich_Text_Area;
less more (0) tip