| 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
|
| Wed, 25 Aug 2010 15:41:14 +0200 |
wenzelm |
select tangible text ranges here -- more robust against ongoing changes of the markup query model
|
file |
diff |
annotate
|
| Tue, 24 Aug 2010 21:22:01 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Mon, 23 Aug 2010 17:35:47 +0200 |
wenzelm |
sporadic locking of jEdit buffer;
|
file |
diff |
annotate
|
| Sun, 22 Aug 2010 20:25:15 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sun, 22 Aug 2010 19:55:41 +0200 |
wenzelm |
proper range for hyperlinks and tooltips, using original markup information;
|
file |
diff |
annotate
|
| Sun, 22 Aug 2010 18:46:16 +0200 |
wenzelm |
renamed Markup_Tree.Node to Text.Info;
|
file |
diff |
annotate
|
| Sun, 22 Aug 2010 13:59:47 +0200 |
wenzelm |
Document_View.text_area_extension: select relevant information directly from Markup_Tree, without intermediate TypeInfo;
|
file |
diff |
annotate
|
| Fri, 20 Aug 2010 11:57:43 +0200 |
wenzelm |
concentrate protocol message formats in Isar_Document;
|
file |
diff |
annotate
|
| Mon, 16 Aug 2010 00:07:28 +0200 |
wenzelm |
simplified command status: interpret stacked markup on demand;
|
file |
diff |
annotate
|
| Sun, 15 Aug 2010 22:48:56 +0200 |
wenzelm |
specific types Text.Offset and Text.Range;
|
file |
diff |
annotate
|
| Thu, 12 Aug 2010 13:49:08 +0200 |
wenzelm |
specific Session.Commands_Changed;
|
file |
diff |
annotate
|
| Wed, 11 Aug 2010 23:29:17 +0200 |
wenzelm |
consider command state as part of Snapshot, not Document;
|
file |
diff |
annotate
|
| Sat, 07 Aug 2010 19:52:14 +0200 |
wenzelm |
concentrate structural document notions in document.scala;
|
file |
diff |
annotate
|
| Sat, 07 Aug 2010 16:15:52 +0200 |
wenzelm |
more explicit treatment of Swing thread context;
|
file |
diff |
annotate
|
| Thu, 05 Aug 2010 23:43:43 +0200 |
wenzelm |
Document_Model: include token marker here;
|
file |
diff |
annotate
|
| Thu, 05 Aug 2010 18:13:12 +0200 |
wenzelm |
renamed to_current to convert, and from_current to revert;
|
file |
diff |
annotate
|
| Thu, 05 Aug 2010 18:00:37 +0200 |
wenzelm |
Change.Snapshot: include from_current/to_current here, with precomputed changes;
|
file |
diff |
annotate
|
| Thu, 05 Aug 2010 16:58:18 +0200 |
wenzelm |
explicit Change.Snapshot and Document.Node;
|
file |
diff |
annotate
|
| Thu, 05 Aug 2010 14:35:35 +0200 |
wenzelm |
simplified/refined document model: collection of named nodes, without proper dependencies yet;
|
file |
diff |
annotate
|
| Mon, 19 Jul 2010 22:19:18 +0200 |
wenzelm |
Session: predefined real time parameters;
|
file |
diff |
annotate
|
| Sat, 03 Jul 2010 20:20:13 +0200 |
wenzelm |
more efficient document model/view -- avoid repeated iteration over commands from start, prefer bulk operations;
|
file |
diff |
annotate
|
| Sat, 26 Jun 2010 21:26:35 +0200 |
wenzelm |
simplified text_area_painter, with more precise treatment of visible line end;
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| Sun, 30 May 2010 23:42:03 +0200 |
wenzelm |
control tooltip font via Swing HTML, with tooltip-font-size property;
|
file |
diff |
annotate
|
| Sat, 29 May 2010 20:34:28 +0200 |
wenzelm |
do not highlight ignored command spans;
|
file |
diff |
annotate
|
| Sat, 29 May 2010 20:03:47 +0200 |
wenzelm |
more explicit handling of document;
|
file |
diff |
annotate
|
| Sat, 29 May 2010 19:46:29 +0200 |
wenzelm |
explicit markup for forked goals, as indicated by Goal.fork;
|
file |
diff |
annotate
|
| Thu, 27 May 2010 12:35:40 +0200 |
wenzelm |
indicate prospective properties;
|
file |
diff |
annotate
|
| Thu, 27 May 2010 00:47:15 +0200 |
wenzelm |
Command.toString: include id for debugging;
|
file |
diff |
annotate
|
| Thu, 20 May 2010 10:43:46 +0200 |
wenzelm |
explicit Command.Status.UNDEFINED -- avoid fragile/cumbersome treatment of Option[State];
|
file |
diff |
annotate
|
| Sat, 08 May 2010 21:08:30 +0200 |
wenzelm |
tuned headers;
|
file |
diff |
annotate
|
| Tue, 30 Mar 2010 00:13:27 +0200 |
wenzelm |
adapted to Scala 2.8.0 Beta 1;
|
file |
diff |
annotate
|
| Mon, 11 Jan 2010 23:00:05 +0100 |
wenzelm |
incorporate "proofdocument" part into main Isabelle/Pure.jar -- except for html_panel.scala, which depends on external library (Lobo/Cobra browser);
|
file |
diff |
annotate
|
| Mon, 11 Jan 2010 20:51:58 +0100 |
wenzelm |
more tobust treatment of Document.current_state;
|
file |
diff |
annotate
|
| Sun, 10 Jan 2010 20:38:23 +0100 |
wenzelm |
eliminated Command.stop, which tends to case duplicate traversal of commands;
|
file |
diff |
annotate
|
| Sun, 10 Jan 2010 20:14:21 +0100 |
wenzelm |
iterators for ranges of commands/starts -- avoid extra array per document;
|
file |
diff |
annotate
|