Fri, 27 Mar 2020 22:01:27 +0100 |
wenzelm |
misc tuning based on hints by IntelliJ IDEA;
|
file |
diff |
annotate
|
Tue, 16 Apr 2019 19:42:56 +0200 |
wenzelm |
clarified goto_file (again): treat bad entry as plain file to open empty buffer instead of error (amending a8142ac5e4b6);
|
file |
diff |
annotate
|
Sat, 30 Mar 2019 22:51:38 +0100 |
wenzelm |
more PIDE markup and hyperlinks;
|
file |
diff |
annotate
|
Mon, 11 Mar 2019 22:13:14 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
Mon, 14 Jan 2019 13:58:12 +0100 |
wenzelm |
clarified message;
|
file |
diff |
annotate
|
Sun, 13 Jan 2019 19:42:06 +0100 |
wenzelm |
support hyperlink to theory exports;
|
file |
diff |
annotate
|
Tue, 05 Sep 2017 16:45:23 +0200 |
wenzelm |
less aggressive default position: prefer persistent defaults maintained by jEdit (amending 89c5bb2a2128);
|
file |
diff |
annotate
|
Sun, 20 Aug 2017 18:30:20 +0200 |
wenzelm |
more robust shutdown, e.g. when plugin is stopped;
|
file |
diff |
annotate
|
Sat, 17 Jun 2017 14:47:36 +0200 |
wenzelm |
maintain overlays within main state of document models;
|
file |
diff |
annotate
|
Fri, 16 Jun 2017 15:59:27 +0200 |
wenzelm |
more general dispatcher operations;
|
file |
diff |
annotate
|
Tue, 13 Jun 2017 21:15:40 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Tue, 13 Jun 2017 20:19:25 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Tue, 13 Jun 2017 20:16:39 +0200 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
Tue, 14 Mar 2017 21:43:54 +0100 |
wenzelm |
clarified singleton module;
|
file |
diff |
annotate
|
Sun, 12 Mar 2017 17:59:03 +0100 |
wenzelm |
clarified current_command: index refers to node content, negative index means first command;
|
file |
diff |
annotate
|
Sun, 12 Mar 2017 14:23:38 +0100 |
wenzelm |
discontinued pointless Text.Length: Javascript and Java agree in old-fashioned UTF-16;
|
file |
diff |
annotate
|
Sat, 11 Mar 2017 16:22:12 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Thu, 12 Jan 2017 11:17:05 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Tue, 10 Jan 2017 16:53:05 +0100 |
wenzelm |
support "purge" operation on document model;
|
file |
diff |
annotate
|
Sun, 08 Jan 2017 19:08:26 +0100 |
wenzelm |
added node_name(String): imitate jEdit buffer operations;
|
file |
diff |
annotate
|
Sun, 08 Jan 2017 17:53:44 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Sun, 08 Jan 2017 16:47:53 +0100 |
wenzelm |
resolve dependencies implicitly via File_Model, without jEdit Buffer_Model;
|
file |
diff |
annotate
|
Sun, 08 Jan 2017 11:41:18 +0100 |
wenzelm |
refer to bibtex entries via general Document_Model, instead of editor buffers;
|
file |
diff |
annotate
|
Sat, 07 Jan 2017 14:34:53 +0100 |
wenzelm |
separate Buffer_Model vs. File_Model;
|
file |
diff |
annotate
|
Fri, 06 Jan 2017 13:27:18 +0100 |
wenzelm |
manage buffer models as explicit global state;
|
file |
diff |
annotate
|
Thu, 05 Jan 2017 12:23:25 +0100 |
wenzelm |
misc tuning and clarification;
|
file |
diff |
annotate
|
Wed, 28 Dec 2016 17:10:09 +0100 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
Wed, 28 Dec 2016 17:02:38 +0100 |
wenzelm |
clarified signature: explicit Length to avoid implicit mistakes;
|
file |
diff |
annotate
|
Fri, 23 Dec 2016 19:19:59 +0100 |
wenzelm |
full range for Position.Item;
|
file |
diff |
annotate
|
Fri, 23 Dec 2016 17:04:29 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Fri, 23 Dec 2016 16:20:42 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Fri, 23 Dec 2016 15:53:53 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Fri, 23 Dec 2016 11:53:31 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Thu, 22 Dec 2016 11:38:16 +0100 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
Wed, 21 Dec 2016 23:30:13 +0100 |
wenzelm |
tuned -- use zero-based Line.Position;
|
file |
diff |
annotate
|
Tue, 20 Dec 2016 10:01:53 +0100 |
wenzelm |
proper counting of chars;
|
file |
diff |
annotate
|
Tue, 20 Dec 2016 09:52:01 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Thu, 24 Nov 2016 15:21:54 +0100 |
wenzelm |
explicit option editor_generated_input_delay, which is more aggressive by default;
|
file |
diff |
annotate
|
Wed, 23 Nov 2016 16:15:17 +0100 |
wenzelm |
delay_first for machine generated editor events: avoid starvation, e.g. when operating on big sessions;
|
file |
diff |
annotate
|
Wed, 27 Jan 2016 14:14:06 +0100 |
wenzelm |
allow single quote within URL;
|
file |
diff |
annotate
|
Tue, 05 Jan 2016 15:40:25 +0100 |
wenzelm |
fewer use of GUI_Thread.now to reduce danger of deadlock on shutdown;
|
file |
diff |
annotate
|
Sat, 21 Nov 2015 20:13:52 +0100 |
wenzelm |
double flush to ensure persistent "state" output is reset;
|
file |
diff |
annotate
|
Fri, 13 Nov 2015 19:59:28 +0100 |
wenzelm |
added antiquotation @{doc}, e.g. useful for demonstration purposes;
|
file |
diff |
annotate
|
Tue, 03 Nov 2015 14:03:44 +0100 |
wenzelm |
prefer ad-hoc non-worker threads;
|
file |
diff |
annotate
|
Mon, 02 Nov 2015 16:03:03 +0100 |
wenzelm |
redundant;
|
file |
diff |
annotate
|
Mon, 24 Aug 2015 00:20:20 +0200 |
wenzelm |
more explicit debugger caret rendering;
|
file |
diff |
annotate
|
Thu, 20 Aug 2015 19:15:17 +0200 |
wenzelm |
tuned signature, according to ML version;
|
file |
diff |
annotate
|
Sat, 15 Aug 2015 18:59:31 +0200 |
wenzelm |
more robust access to stable tip version: take all pending edits into account, don't assume model for current buffer;
|
file |
diff |
annotate
|
Tue, 11 Aug 2015 17:00:16 +0200 |
wenzelm |
support hyperlinks with optional focus change;
|
file |
diff |
annotate
|
Mon, 10 Aug 2015 14:13:49 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Thu, 08 Jan 2015 20:56:39 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Tue, 02 Dec 2014 17:30:53 +0100 |
wenzelm |
added Untyped.method convenience (for *this* class only);
|
file |
diff |
annotate
|
Sun, 05 Oct 2014 17:58:36 +0200 |
wenzelm |
citation tooltip/hyperlink based on open buffers with .bib files;
|
file |
diff |
annotate
|
Sun, 10 Aug 2014 13:06:26 +0200 |
wenzelm |
follow link to originating command, to ensure that Simplifier_Trace_Dockable displays its results (via current_command);
|
file |
diff |
annotate
|
Sat, 09 Aug 2014 11:25:46 +0200 |
wenzelm |
clarified synchronized scope;
|
file |
diff |
annotate
|
Wed, 23 Jul 2014 13:01:30 +0200 |
wenzelm |
more explicit discrimination of empty nodes -- suppress from Theories panel;
|
file |
diff |
annotate
|
Wed, 23 Jul 2014 11:19:24 +0200 |
wenzelm |
clarified module name: facilitate alternative GUI frameworks;
|
file |
diff |
annotate
|
Wed, 23 Jul 2014 11:08:24 +0200 |
wenzelm |
proper change of perspective for removed nodes (stemming from closed buffers);
|
file |
diff |
annotate
|
Mon, 28 Apr 2014 14:41:49 +0200 |
wenzelm |
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
|
file |
diff |
annotate
|
Fri, 25 Apr 2014 20:21:27 +0200 |
wenzelm |
prefer Isabelle/Scala operations;
|
file |
diff |
annotate
|