| Fri, 21 Feb 2014 15:48:04 +0100 |
wenzelm |
tuned signature -- avoid redundancy and confusion of flags;
|
file |
diff |
annotate
|
| Fri, 21 Feb 2014 15:12:50 +0100 |
wenzelm |
more general / abstract Command.Markups, with separate index for status elements;
|
file |
diff |
annotate
|
| Fri, 21 Feb 2014 12:57:14 +0100 |
wenzelm |
more lightweight Rendering;
|
file |
diff |
annotate
|
| Fri, 21 Feb 2014 12:32:06 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Thu, 20 Feb 2014 18:23:32 +0100 |
wenzelm |
tuned comments;
|
file |
diff |
annotate
|
| Thu, 20 Feb 2014 17:57:26 +0100 |
wenzelm |
complete symbols within ML strings / comments;
|
file |
diff |
annotate
|
| Thu, 20 Feb 2014 17:21:48 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 20 Feb 2014 16:56:51 +0100 |
wenzelm |
clarified markup cumulation order (see also 25306d92f4ad and 0009a6ebc83b), e.g. relevant for completion_context;
|
file |
diff |
annotate
|
| Thu, 20 Feb 2014 16:00:37 +0100 |
wenzelm |
cumulate/select wrt. precise elements guard;
|
file |
diff |
annotate
|
| Thu, 20 Feb 2014 15:15:41 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 20 Feb 2014 13:23:49 +0100 |
wenzelm |
default completion context via outer syntax;
|
file |
diff |
annotate
|
| Thu, 20 Feb 2014 12:53:12 +0100 |
wenzelm |
completion of keywords and symbols based on language context;
|
file |
diff |
annotate
|
| Tue, 18 Feb 2014 16:34:02 +0100 |
wenzelm |
generic markup for embedded languages;
|
file |
diff |
annotate
|
| Mon, 17 Feb 2014 20:54:03 +0100 |
wenzelm |
hyperlink for visible positions;
|
file |
diff |
annotate
|
| Mon, 17 Feb 2014 11:14:26 +0100 |
wenzelm |
more markup;
|
file |
diff |
annotate
|
| Sun, 16 Feb 2014 16:48:30 +0100 |
wenzelm |
more uniform rendering of text that is formally interpreted: avoid clash with inner markup;
|
file |
diff |
annotate
|
| Sun, 16 Feb 2014 15:38:08 +0100 |
wenzelm |
support ML antiquotations in Scala;
|
file |
diff |
annotate
|
| Sat, 15 Feb 2014 18:28:18 +0100 |
wenzelm |
more uniform ML keyword markup;
|
file |
diff |
annotate
|
| Sat, 15 Feb 2014 17:04:55 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sat, 15 Feb 2014 16:49:10 +0100 |
wenzelm |
refined ML keyword styles;
|
file |
diff |
annotate
|
| Sat, 15 Feb 2014 16:27:58 +0100 |
wenzelm |
isabelle-ml mode with separate token marker;
|
file |
diff |
annotate
|
| Tue, 04 Feb 2014 09:04:59 +0000 |
Lars Hupel |
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
|
file |
diff |
annotate
|
| Sat, 18 Jan 2014 19:15:12 +0100 |
wenzelm |
support for nested text cartouches;
|
file |
diff |
annotate
|
| Mon, 09 Dec 2013 12:16:52 +0100 |
wenzelm |
added document antiquotation @{url}, which produces formal markup for LaTeX and PIDE;
|
file |
diff |
annotate
|
| Tue, 19 Nov 2013 12:57:56 +0100 |
wenzelm |
clarified boundary cases of Document.Node.Name;
|
file |
diff |
annotate
|
| Wed, 11 Sep 2013 20:16:28 +0200 |
wenzelm |
more explicit indication of 'done' as proof script element;
|
file |
diff |
annotate
|
| Mon, 02 Sep 2013 16:10:26 +0200 |
wenzelm |
more explicit indication of 'guess' as improper Isar (aka "script") element;
|
file |
diff |
annotate
|
| Thu, 29 Aug 2013 10:01:59 +0200 |
wenzelm |
more abstract Completion_Popup.Text_Area;
|
file |
diff |
annotate
|
| Tue, 27 Aug 2013 16:09:28 +0200 |
wenzelm |
determine completion geometry like tooltip;
|
file |
diff |
annotate
|
| Mon, 12 Aug 2013 17:11:27 +0200 |
wenzelm |
manage hyperlinks via PIDE editor interface;
|
file |
diff |
annotate
|
| Wed, 07 Aug 2013 19:59:58 +0200 |
wenzelm |
more elementary list structures for markup tree traversal;
|
file |
diff |
annotate
|
| Wed, 07 Aug 2013 14:13:59 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Wed, 07 Aug 2013 13:46:32 +0200 |
wenzelm |
more tight interface for markup cumulate/select: avoid duplicate application, allow to defer decision about definedness;
|
file |
diff |
annotate
|
| Mon, 05 Aug 2013 22:54:50 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sat, 13 Jul 2013 18:13:09 +0200 |
wenzelm |
more rendering for information messages;
|
file |
diff |
annotate
|
| Sat, 13 Jul 2013 13:58:13 +0200 |
wenzelm |
gutter icon for information messages;
|
file |
diff |
annotate
|
| Sat, 13 Jul 2013 13:25:42 +0200 |
wenzelm |
more explicit Markup.information for messages produced by "auto" tools;
|
file |
diff |
annotate
|
| Fri, 05 Jul 2013 15:38:03 +0200 |
wenzelm |
explicit module Document_ID as source of globally unique identifiers across ML/Scala;
|
file |
diff |
annotate
|
| Fri, 28 Jun 2013 14:51:19 +0200 |
wenzelm |
load icons via options -- prefer IntelliJ IDEA for now;
|
file |
diff |
annotate
|
| Fri, 28 Jun 2013 14:05:12 +0200 |
wenzelm |
support for idea-icons (using ideaIC-129.354/platform/icons/src from IntelliJ IDEA Community Edition 12.1.2);
|
file |
diff |
annotate
|
| Tue, 21 May 2013 16:51:16 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 21 May 2013 16:47:18 +0200 |
wenzelm |
less intrusive rendering of antiquoted text -- avoid visual clash with "blue variables" in particular;
|
file |
diff |
annotate
|
| Mon, 20 May 2013 13:54:24 +0200 |
wenzelm |
discontinued odd workaround for scala-2.9.2, which is hopefully obsolete in scala-2.10.x;
|
file |
diff |
annotate
|
| Sat, 30 Mar 2013 16:16:24 +0100 |
wenzelm |
tooltip of command keyword includes timing information;
|
file |
diff |
annotate
|
| Thu, 28 Mar 2013 22:42:18 +0100 |
wenzelm |
ghost bullet via markup, which is painted as bar under text (normally space);
|
file |
diff |
annotate
|
| Sat, 23 Mar 2013 19:39:31 +0100 |
wenzelm |
retain original tooltip range, to avoid repeated window popup when the mouse is moved over the same content;
|
file |
diff |
annotate
|
| Mon, 14 Jan 2013 23:08:40 +0100 |
wenzelm |
more prominent status ticks;
|
file |
diff |
annotate
|
| Fri, 04 Jan 2013 12:33:25 +0100 |
wenzelm |
prefer old graph browser in Isabelle/jEdit, which still produces better layout;
|
file |
diff |
annotate
|
| Sun, 30 Dec 2012 21:49:20 +0100 |
wenzelm |
tuned rendering;
|
file |
diff |
annotate
|
| Sat, 15 Dec 2012 21:07:52 +0100 |
wenzelm |
more general handling of graphics configurations, to increase chance of proper positioning of tooltips in multi-screen environment;
|
file |
diff |
annotate
|
| Sat, 15 Dec 2012 14:26:37 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sat, 15 Dec 2012 12:55:11 +0100 |
wenzelm |
explicit text_fold markup, which is used by default in Pretty.chunks/chunks2;
|
file |
diff |
annotate
|
| Sat, 15 Dec 2012 12:28:37 +0100 |
wenzelm |
fold main goal;
|
file |
diff |
annotate
|
| Sat, 15 Dec 2012 12:16:16 +0100 |
wenzelm |
fold handling within Pretty_Text_Area, based on formal document content, which is static here;
|
file |
diff |
annotate
|
| Fri, 14 Dec 2012 12:09:08 +0100 |
wenzelm |
more formal class Command.Results;
|
file |
diff |
annotate
|
| Thu, 13 Dec 2012 17:46:33 +0100 |
wenzelm |
include command results in tooltip as well;
|
file |
diff |
annotate
|
| Thu, 13 Dec 2012 17:29:23 +0100 |
wenzelm |
more careful handling of Dialog_Result, with active area and color feedback;
|
file |
diff |
annotate
|
| Thu, 13 Dec 2012 13:52:18 +0100 |
wenzelm |
identify dialogs via official serial and maintain as result message;
|
file |
diff |
annotate
|
| Wed, 12 Dec 2012 23:36:07 +0100 |
wenzelm |
rendering of selected dialog_result as active_result_color, depending on dynamic command status in output panel, but not static popups etc.;
|
file |
diff |
annotate
|
| Wed, 12 Dec 2012 21:50:42 +0100 |
wenzelm |
support dialog via document content;
|
file |
diff |
annotate
|