src/Tools/jEdit/src/jedit/document_view.scala
Thu, 04 Nov 2010 10:58:03 +0100 wenzelm clarified tooltips: message output by default, extra info via control/command;
Tue, 26 Oct 2010 16:56:07 +0200 wenzelm disable broken popups for now;
Wed, 29 Sep 2010 17:58:27 +0200 wenzelm CONTROL-mouse management: handle windowDeactivated as well;
Tue, 28 Sep 2010 23:47:45 +0200 wenzelm CONTROL-mouse management: handle windowIconified;
Tue, 28 Sep 2010 23:02:05 +0200 wenzelm basic support for message popups via HTML_Panel;
Tue, 28 Sep 2010 20:22:58 +0200 wenzelm more defensive overview.paintComponent: avoid potential crash due to buffer change while painting;
Sat, 25 Sep 2010 15:40:40 +0200 wenzelm more precise treatment of backgrounds vs. rectangles;
Fri, 24 Sep 2010 17:09:07 +0200 wenzelm some attempts to improve visual appearance of bad text;
Fri, 24 Sep 2010 14:12:33 +0200 wenzelm permissive exit;
Wed, 08 Sep 2010 00:17:41 +0200 wenzelm disposed some old TODO/FIXME;
Tue, 07 Sep 2010 23:59:14 +0200 wenzelm Document_View: select gutter message icons from markup over line range, not full range results;
Tue, 07 Sep 2010 23:06:52 +0200 wenzelm concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
Tue, 07 Sep 2010 22:28:58 +0200 wenzelm simplified Markup_Tree.select: Stream instead of Iterator (again), explicit Option instead of default;
Tue, 07 Sep 2010 21:06:58 +0200 wenzelm Document_View: more precise painting of gutter icons, only if line selection area is sufficiently large;
Tue, 07 Sep 2010 18:44:28 +0200 wenzelm basic support for warning/error gutter icons;
Tue, 07 Sep 2010 17:34:28 +0200 wenzelm Document_View: some markup for main inner syntax categories;
Tue, 07 Sep 2010 16:08:29 +0200 wenzelm highlight bad range of nested error (here from inner parsing);
Tue, 07 Sep 2010 14:53:05 +0200 wenzelm Document_View: less aggressive background coloring, departing from classic PG highlighting;
Tue, 07 Sep 2010 14:08:21 +0200 wenzelm report token range after inner parse error -- often provides important clues about misunderstanding concerning lexical phase;
Sat, 04 Sep 2010 22:36:42 +0200 wenzelm refined treatment of multi-line subexpressions;
Sat, 04 Sep 2010 22:00:25 +0200 wenzelm basic support for subexpression highlighting (see also gatchan.jedit.hyperlinks.HyperlinkManager/HyperlinkTextAreaPainter);
Thu, 02 Sep 2010 23:37:14 +0200 wenzelm Document_View: squiggly underline for messages;
Tue, 31 Aug 2010 22:03:55 +0200 wenzelm tuned;
Tue, 31 Aug 2010 17:49:45 +0200 wenzelm Document_View: repaint overview for any command change of this node (again);
Tue, 31 Aug 2010 17:40:32 +0200 wenzelm refined proper_line_range (again), to make text_area_extension work with soft wwrap;
Tue, 31 Aug 2010 16:07:25 +0200 wenzelm tuned commands_changed_actor: more precise/efficient handling of visible screen lines;
Tue, 31 Aug 2010 13:20:12 +0200 wenzelm simplified/clarified Document_View.text_area_extension;
Mon, 30 Aug 2010 10:36:55 +0200 wenzelm Document_View.text_area_extension: do not insist in crashing if (weak) assertion is violated;
Sun, 29 Aug 2010 15:09:11 +0200 wenzelm added Document.Snapshot.select_markup, which includes command iteration, range conversion etc.;
Sat, 28 Aug 2010 20:24:41 +0200 wenzelm more careful locking of jEdit buffer;
Wed, 25 Aug 2010 15:41:14 +0200 wenzelm select tangible text ranges here -- more robust against ongoing changes of the markup query model
Tue, 24 Aug 2010 21:22:01 +0200 wenzelm tuned;
Mon, 23 Aug 2010 17:35:47 +0200 wenzelm sporadic locking of jEdit buffer;
Sun, 22 Aug 2010 20:25:15 +0200 wenzelm tuned signature;
Sun, 22 Aug 2010 19:55:41 +0200 wenzelm proper range for hyperlinks and tooltips, using original markup information;
Sun, 22 Aug 2010 18:46:16 +0200 wenzelm renamed Markup_Tree.Node to Text.Info;
Sun, 22 Aug 2010 13:59:47 +0200 wenzelm Document_View.text_area_extension: select relevant information directly from Markup_Tree, without intermediate TypeInfo;
Fri, 20 Aug 2010 11:57:43 +0200 wenzelm concentrate protocol message formats in Isar_Document;
Mon, 16 Aug 2010 00:07:28 +0200 wenzelm simplified command status: interpret stacked markup on demand;
Sun, 15 Aug 2010 22:48:56 +0200 wenzelm specific types Text.Offset and Text.Range;
Thu, 12 Aug 2010 13:49:08 +0200 wenzelm specific Session.Commands_Changed;
Wed, 11 Aug 2010 23:29:17 +0200 wenzelm consider command state as part of Snapshot, not Document;
Sat, 07 Aug 2010 19:52:14 +0200 wenzelm concentrate structural document notions in document.scala;
Sat, 07 Aug 2010 16:15:52 +0200 wenzelm more explicit treatment of Swing thread context;
Thu, 05 Aug 2010 23:43:43 +0200 wenzelm Document_Model: include token marker here;
Thu, 05 Aug 2010 18:13:12 +0200 wenzelm renamed to_current to convert, and from_current to revert;
Thu, 05 Aug 2010 18:00:37 +0200 wenzelm Change.Snapshot: include from_current/to_current here, with precomputed changes;
Thu, 05 Aug 2010 16:58:18 +0200 wenzelm explicit Change.Snapshot and Document.Node;
Thu, 05 Aug 2010 14:35:35 +0200 wenzelm simplified/refined document model: collection of named nodes, without proper dependencies yet;
Mon, 19 Jul 2010 22:19:18 +0200 wenzelm Session: predefined real time parameters;
Sat, 03 Jul 2010 20:20:13 +0200 wenzelm more efficient document model/view -- avoid repeated iteration over commands from start, prefer bulk operations;
Sat, 26 Jun 2010 21:26:35 +0200 wenzelm simplified text_area_painter, with more precise treatment of visible line end;
Tue, 01 Jun 2010 17:27:38 +0200 wenzelm basic support for sub/superscript token markup -- NB: need to maintain extended token types eagerly, since jEdit occasionally reinstalls a style array that is too short;
Sun, 30 May 2010 23:42:03 +0200 wenzelm control tooltip font via Swing HTML, with tooltip-font-size property;
Sat, 29 May 2010 20:34:28 +0200 wenzelm do not highlight ignored command spans;
Sat, 29 May 2010 20:03:47 +0200 wenzelm more explicit handling of document;
Sat, 29 May 2010 19:46:29 +0200 wenzelm explicit markup for forked goals, as indicated by Goal.fork;
Thu, 27 May 2010 12:35:40 +0200 wenzelm indicate prospective properties;
Thu, 27 May 2010 00:47:15 +0200 wenzelm Command.toString: include id for debugging;
Thu, 20 May 2010 10:43:46 +0200 wenzelm explicit Command.Status.UNDEFINED -- avoid fragile/cumbersome treatment of Option[State];
less more (0) -60 tip