| Thu, 04 Nov 2010 10:58:03 +0100 |
wenzelm |
clarified tooltips: message output by default, extra info via control/command;
|
file |
diff |
annotate
|
| Tue, 26 Oct 2010 16:56:07 +0200 |
wenzelm |
disable broken popups for now;
|
file |
diff |
annotate
|
| Wed, 29 Sep 2010 17:58:27 +0200 |
wenzelm |
CONTROL-mouse management: handle windowDeactivated as well;
|
file |
diff |
annotate
|
| Tue, 28 Sep 2010 23:47:45 +0200 |
wenzelm |
CONTROL-mouse management: handle windowIconified;
|
file |
diff |
annotate
|
| Tue, 28 Sep 2010 23:02:05 +0200 |
wenzelm |
basic support for message popups via HTML_Panel;
|
file |
diff |
annotate
|
| Tue, 28 Sep 2010 20:22:58 +0200 |
wenzelm |
more defensive overview.paintComponent: avoid potential crash due to buffer change while painting;
|
file |
diff |
annotate
|
| Sat, 25 Sep 2010 15:40:40 +0200 |
wenzelm |
more precise treatment of backgrounds vs. rectangles;
|
file |
diff |
annotate
|
| Fri, 24 Sep 2010 17:09:07 +0200 |
wenzelm |
some attempts to improve visual appearance of bad text;
|
file |
diff |
annotate
|
| Fri, 24 Sep 2010 14:12:33 +0200 |
wenzelm |
permissive exit;
|
file |
diff |
annotate
|
| Wed, 08 Sep 2010 00:17:41 +0200 |
wenzelm |
disposed some old TODO/FIXME;
|
file |
diff |
annotate
|
| Tue, 07 Sep 2010 23:59:14 +0200 |
wenzelm |
Document_View: select gutter message icons from markup over line range, not full range results;
|
file |
diff |
annotate
|
| Tue, 07 Sep 2010 23:06:52 +0200 |
wenzelm |
concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
|
file |
diff |
annotate
|
| Tue, 07 Sep 2010 22:28:58 +0200 |
wenzelm |
simplified Markup_Tree.select: Stream instead of Iterator (again), explicit Option instead of default;
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| Tue, 07 Sep 2010 18:44:28 +0200 |
wenzelm |
basic support for warning/error gutter icons;
|
file |
diff |
annotate
|
| Tue, 07 Sep 2010 17:34:28 +0200 |
wenzelm |
Document_View: some markup for main inner syntax categories;
|
file |
diff |
annotate
|
| Tue, 07 Sep 2010 16:08:29 +0200 |
wenzelm |
highlight bad range of nested error (here from inner parsing);
|
file |
diff |
annotate
|
| Tue, 07 Sep 2010 14:53:05 +0200 |
wenzelm |
Document_View: less aggressive background coloring, departing from classic PG highlighting;
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| Sat, 04 Sep 2010 22:36:42 +0200 |
wenzelm |
refined treatment of multi-line subexpressions;
|
file |
diff |
annotate
|
| Sat, 04 Sep 2010 22:00:25 +0200 |
wenzelm |
basic support for subexpression highlighting (see also gatchan.jedit.hyperlinks.HyperlinkManager/HyperlinkTextAreaPainter);
|
file |
diff |
annotate
|
| Thu, 02 Sep 2010 23:37:14 +0200 |
wenzelm |
Document_View: squiggly underline for messages;
|
file |
diff |
annotate
|
| Tue, 31 Aug 2010 22:03:55 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 31 Aug 2010 17:49:45 +0200 |
wenzelm |
Document_View: repaint overview for any command change of this node (again);
|
file |
diff |
annotate
|
| Tue, 31 Aug 2010 17:40:32 +0200 |
wenzelm |
refined proper_line_range (again), to make text_area_extension work with soft wwrap;
|
file |
diff |
annotate
|
| Tue, 31 Aug 2010 16:07:25 +0200 |
wenzelm |
tuned commands_changed_actor: more precise/efficient handling of visible screen lines;
|
file |
diff |
annotate
|
| Tue, 31 Aug 2010 13:20:12 +0200 |
wenzelm |
simplified/clarified Document_View.text_area_extension;
|
file |
diff |
annotate
|
| Mon, 30 Aug 2010 10:36:55 +0200 |
wenzelm |
Document_View.text_area_extension: do not insist in crashing if (weak) assertion is violated;
|
file |
diff |
annotate
|
| Sun, 29 Aug 2010 15:09:11 +0200 |
wenzelm |
added Document.Snapshot.select_markup, which includes command iteration, range conversion etc.;
|
file |
diff |
annotate
|
| Sat, 28 Aug 2010 20:24:41 +0200 |
wenzelm |
more careful locking of jEdit buffer;
|
file |
diff |
annotate
|