#
cbcb9b75 |
|
05-Sep-2017 |
wenzelm <none@none> |
less aggressive default position: prefer persistent defaults maintained by jEdit (amending 89c5bb2a2128);
|
#
d6fe72c5 |
|
20-Aug-2017 |
wenzelm <none@none> |
more robust shutdown, e.g. when plugin is stopped;
|
#
9357e275 |
|
17-Jun-2017 |
wenzelm <none@none> |
maintain overlays within main state of document models; proper pending_input for Isabelle/VSCode;
|
#
9bd022db |
|
16-Jun-2017 |
wenzelm <none@none> |
more general dispatcher operations;
|
#
70cb547d |
|
13-Jun-2017 |
wenzelm <none@none> |
tuned signature;
|
#
518273a3 |
|
13-Jun-2017 |
wenzelm <none@none> |
tuned;
|
#
4a4e793f |
|
13-Jun-2017 |
wenzelm <none@none> |
clarified modules;
|
#
7dec135b |
|
14-Mar-2017 |
wenzelm <none@none> |
clarified singleton module;
|
#
7a4055d4 |
|
12-Mar-2017 |
wenzelm <none@none> |
clarified current_command: index refers to node content, negative index means first command;
|
#
65cade08 |
|
12-Mar-2017 |
wenzelm <none@none> |
discontinued pointless Text.Length: Javascript and Java agree in old-fashioned UTF-16;
|
#
c868f18e |
|
11-Mar-2017 |
wenzelm <none@none> |
tuned;
|
#
5fcecffa |
|
12-Jan-2017 |
wenzelm <none@none> |
tuned signature;
|
#
7fdd3866 |
|
10-Jan-2017 |
wenzelm <none@none> |
support "purge" operation on document model;
|
#
1a9260bd |
|
08-Jan-2017 |
wenzelm <none@none> |
added node_name(String): imitate jEdit buffer operations; more uniform get_file_content for external source file references;
|
#
37ea566c |
|
08-Jan-2017 |
wenzelm <none@none> |
tuned;
|
#
e0d152c5 |
|
08-Jan-2017 |
wenzelm <none@none> |
resolve dependencies implicitly via File_Model, without jEdit Buffer_Model;
|
#
06be203f |
|
08-Jan-2017 |
wenzelm <none@none> |
refer to bibtex entries via general Document_Model, instead of editor buffers;
|
#
02111fe7 |
|
07-Jan-2017 |
wenzelm <none@none> |
separate Buffer_Model vs. File_Model; misc tuning and clarification;
|
#
1b8abc07 |
|
06-Jan-2017 |
wenzelm <none@none> |
manage buffer models as explicit global state; tuned signature;
|
#
d3bfc6f1 |
|
04-Jan-2017 |
wenzelm <none@none> |
misc tuning and clarification;
|
#
302ad5fc |
|
28-Dec-2016 |
wenzelm <none@none> |
clarified modules;
|
#
b56fd855 |
|
28-Dec-2016 |
wenzelm <none@none> |
clarified signature: explicit Length to avoid implicit mistakes;
|
#
dfcd32f3 |
|
23-Dec-2016 |
wenzelm <none@none> |
full range for Position.Item; more hyperlinks for VSCode;
|
#
52af301a |
|
23-Dec-2016 |
wenzelm <none@none> |
tuned;
|
#
4a214b56 |
|
23-Dec-2016 |
wenzelm <none@none> |
tuned;
|
#
6c905f17 |
|
23-Dec-2016 |
wenzelm <none@none> |
tuned;
|
#
96d9d013 |
|
23-Dec-2016 |
wenzelm <none@none> |
tuned;
|
#
b4ebc04a |
|
22-Dec-2016 |
wenzelm <none@none> |
clarified modules;
|
#
d23c8e09 |
|
21-Dec-2016 |
wenzelm <none@none> |
tuned -- use zero-based Line.Position;
|
#
5982f528 |
|
20-Dec-2016 |
wenzelm <none@none> |
proper counting of chars;
|
#
b714257b |
|
20-Dec-2016 |
wenzelm <none@none> |
tuned;
|
#
17963ce2 |
|
24-Nov-2016 |
wenzelm <none@none> |
explicit option editor_generated_input_delay, which is more aggressive by default;
|
#
b9176ec5 |
|
23-Nov-2016 |
wenzelm <none@none> |
delay_first for machine generated editor events: avoid starvation, e.g. when operating on big sessions;
|
#
8a39146a |
|
27-Jan-2016 |
wenzelm <none@none> |
allow single quote within URL;
|
#
4d897091 |
|
05-Jan-2016 |
wenzelm <none@none> |
fewer use of GUI_Thread.now to reduce danger of deadlock on shutdown;
|
#
e586062c |
|
21-Nov-2015 |
wenzelm <none@none> |
double flush to ensure persistent "state" output is reset; tuned GUI;
|
#
7fc4465c |
|
13-Nov-2015 |
wenzelm <none@none> |
added antiquotation @{doc}, e.g. useful for demonstration purposes;
|
#
5f27c221 |
|
03-Nov-2015 |
wenzelm <none@none> |
prefer ad-hoc non-worker threads;
|
#
5b0dc9fd |
|
02-Nov-2015 |
wenzelm <none@none> |
redundant;
|
#
633fafe2 |
|
23-Aug-2015 |
wenzelm <none@none> |
more explicit debugger caret rendering;
|
#
376e854a |
|
20-Aug-2015 |
wenzelm <none@none> |
tuned signature, according to ML version;
|
#
74cdc740 |
|
15-Aug-2015 |
wenzelm <none@none> |
more robust access to stable tip version: take all pending edits into account, don't assume model for current buffer;
|
#
e434d293 |
|
11-Aug-2015 |
wenzelm <none@none> |
support hyperlinks with optional focus change; no change of focus for debuffer position, to avoid visual glitches and keep panel active;
|
#
4529062a |
|
10-Aug-2015 |
wenzelm <none@none> |
tuned signature;
|
#
7908f989 |
|
08-Jan-2015 |
wenzelm <none@none> |
tuned;
|
#
e6917fdc |
|
02-Dec-2014 |
wenzelm <none@none> |
added Untyped.method convenience (for *this* class only);
|
#
0eef378e |
|
05-Oct-2014 |
wenzelm <none@none> |
citation tooltip/hyperlink based on open buffers with .bib files;
|
#
3a774892 |
|
10-Aug-2014 |
wenzelm <none@none> |
follow link to originating command, to ensure that Simplifier_Trace_Dockable displays its results (via current_command);
|
#
7db92137 |
|
09-Aug-2014 |
wenzelm <none@none> |
clarified synchronized scope;
|
#
6ea51c65 |
|
23-Jul-2014 |
wenzelm <none@none> |
more explicit discrimination of empty nodes -- suppress from Theories panel;
|
#
40e642df |
|
23-Jul-2014 |
wenzelm <none@none> |
clarified module name: facilitate alternative GUI frameworks; --HG-- rename : src/Pure/GUI/swing_thread.scala => src/Pure/GUI/gui_thread.scala
|
#
8da7bdb9 |
|
23-Jul-2014 |
wenzelm <none@none> |
proper change of perspective for removed nodes (stemming from closed buffers);
|
#
023585e2 |
|
28-Apr-2014 |
wenzelm <none@none> |
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
|
#
ca07262c |
|
25-Apr-2014 |
wenzelm <none@none> |
prefer Isabelle/Scala operations;
|
#
da5844fe |
|
22-Apr-2014 |
wenzelm <none@none> |
avoid "Adaptation of argument list by inserting ()" -- deprecated in scala-2.11.0;
|
#
71a521c4 |
|
09-Apr-2014 |
wenzelm <none@none> |
avoid confusion about pointless cursor movement with external links;
|
#
38f7f406 |
|
07-Apr-2014 |
wenzelm <none@none> |
more explicit Command.Chunk types, less ooddities; tuned;
|
#
06b46b22 |
|
08-Apr-2014 |
wenzelm <none@none> |
tuned;
|
#
f5860017 |
|
07-Apr-2014 |
wenzelm <none@none> |
simplified blob again (amending 1e77ed11f2f7): only store file node name, i.e. the raw editor file name; more liberal hyperlink to files, allow hyperlinks within editor files independently of the (POSIX) file-system;
|
#
642259a2 |
|
07-Apr-2014 |
wenzelm <none@none> |
tuned signature -- prefer static type Document.Node.Name;
|
#
87eb49e0 |
|
04-Apr-2014 |
wenzelm <none@none> |
support for jEdit Navigator plugin;
|
#
c547a7d9 |
|
02-Apr-2014 |
wenzelm <none@none> |
tuned signature -- more explicit iterator terminology;
|
#
41c15472 |
|
29-Mar-2014 |
wenzelm <none@none> |
tuned signature;
|
#
1447d8e0 |
|
02-Mar-2014 |
wenzelm <none@none> |
tuned signature -- emphasize symbol positions (prover) vs. decoded text offsets (editor);
|
#
1b4c02e6 |
|
03-Mar-2014 |
wenzelm <none@none> |
clarified path checks: avoid crash of rendering due to spurious errors;
|
#
54210d31 |
|
03-Mar-2014 |
wenzelm <none@none> |
more precise navigation within open files;
|
#
211dbc11 |
|
03-Mar-2014 |
wenzelm <none@none> |
tuned signature;
|
#
a6d1922c |
|
03-Mar-2014 |
wenzelm <none@none> |
tuned signature;
|
#
9b664ef4 |
|
01-Mar-2014 |
wenzelm <none@none> |
incorporate chunk range that is 1 off end-of-input, for improved error positions (NB: command spans are tight, without trailing whitespace); tuned signature;
|
#
220d2361 |
|
27-Feb-2014 |
wenzelm <none@none> |
more formal Document.Blobs; removed junk;
|
#
0e096df6 |
|
26-Feb-2014 |
wenzelm <none@none> |
proper update of text perspective for nodes with changed blobs, which is important to refresh the corresponding command perspective (otherwise it might refer to invalid thy_load commands and cause full execution of the node by the prover);
|
#
f08475a6 |
|
11-Feb-2014 |
wenzelm <none@none> |
maintain multiple command chunks and markup trees: for main chunk and loaded files; document view for all text areas, including auxiliary files;
|
#
c891e793 |
|
09-Dec-2013 |
wenzelm <none@none> |
browse directory hyperlink as well;
|
#
9efc3abf |
|
08-Dec-2013 |
wenzelm <none@none> |
added document antiquotation @{url}, which produces formal markup for LaTeX and PIDE;
|
#
d7a3e31f |
|
20-Nov-2013 |
wenzelm <none@none> |
restrict node_required status and Theories panel to actual theories;
|
#
2983aed5 |
|
19-Nov-2013 |
wenzelm <none@none> |
refer to thy_load command of auxiliary file;
|
#
66bd2215 |
|
19-Nov-2013 |
wenzelm <none@none> |
tuned signature;
|
#
c7c8c42b |
|
19-Nov-2013 |
wenzelm <none@none> |
clarified Document.Blobs environment vs. actual edits of auxiliary files; more robust handling of vacuous edits;
|
#
1ec4de97 |
|
17-Nov-2013 |
wenzelm <none@none> |
centralized management of pending buffer edits;
|
#
50858dac |
|
11-Oct-2013 |
wenzelm <none@none> |
clarified Editor.current_command: allow outdated snapshot; more accurate Document_View.perspective based on current_command for proper state output (see also 88c6e630c15f and ef62204a126b);
|
#
f3f45213 |
|
24-Sep-2013 |
wenzelm <none@none> |
more tolerant treatment of end-of-buffer -- avoid debatable situations of jEdit buffer boundaries;
|
#
3dedff6e |
|
24-Sep-2013 |
wenzelm <none@none> |
skip ignored commands, similar to former proper_command_at (see d68ea01d5084) -- relevant to Output, Query_Operation etc.; tuned signature;
|
#
66269220 |
|
12-Aug-2013 |
wenzelm <none@none> |
manage hyperlinks via PIDE editor interface;
|
#
8db402ed |
|
12-Aug-2013 |
wenzelm <none@none> |
prefer PIDE editor operations; apply_query: insist in non-outdated snapshot via editor.current_command; tuned signature;
|
#
0745bc76 |
|
12-Aug-2013 |
wenzelm <none@none> |
central management of Document.Overlays, independent of Document_Model;
|
#
bda7145c |
|
11-Aug-2013 |
wenzelm <none@none> |
tuned signature;
|
#
511693dd |
|
12-Aug-2013 |
wenzelm <none@none> |
tuned signature;
|
#
a79a6626 |
|
12-Aug-2013 |
wenzelm <none@none> |
tuned signature -- more abstract PIDE editor operations;
|