src/Tools/jEdit/src/jedit_editor.scala
2014-08-09 wenzelm 2014-08-09 clarified synchronized scope;
2014-07-23 wenzelm 2014-07-23 more explicit discrimination of empty nodes -- suppress from Theories panel;
2014-07-23 wenzelm 2014-07-23 clarified module name: facilitate alternative GUI frameworks;
2014-07-23 wenzelm 2014-07-23 proper change of perspective for removed nodes (stemming from closed buffers);
2014-04-28 wenzelm 2014-04-28 mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
2014-04-25 wenzelm 2014-04-25 prefer Isabelle/Scala operations;
2014-04-22 wenzelm 2014-04-22 avoid "Adaptation of argument list by inserting ()" -- deprecated in scala-2.11.0;
2014-04-09 wenzelm 2014-04-09 avoid confusion about pointless cursor movement with external links;
2014-04-08 wenzelm 2014-04-08 more explicit Command.Chunk types, less ooddities; tuned;
2014-04-08 wenzelm 2014-04-08 tuned;
2014-04-07 wenzelm 2014-04-07 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;
2014-04-07 wenzelm 2014-04-07 tuned signature -- prefer static type Document.Node.Name;
2014-04-04 wenzelm 2014-04-04 support for jEdit Navigator plugin;
2014-04-02 wenzelm 2014-04-02 tuned signature -- more explicit iterator terminology;
2014-03-29 wenzelm 2014-03-29 tuned signature;
2014-03-03 wenzelm 2014-03-03 tuned signature -- emphasize symbol positions (prover) vs. decoded text offsets (editor);
2014-03-03 wenzelm 2014-03-03 clarified path checks: avoid crash of rendering due to spurious errors;
2014-03-03 wenzelm 2014-03-03 more precise navigation within open files;
2014-03-03 wenzelm 2014-03-03 tuned signature;
2014-03-03 wenzelm 2014-03-03 tuned signature;
2014-03-01 wenzelm 2014-03-01 incorporate chunk range that is 1 off end-of-input, for improved error positions (NB: command spans are tight, without trailing whitespace); tuned signature;
2014-02-27 wenzelm 2014-02-27 more formal Document.Blobs; removed junk;
2014-02-27 wenzelm 2014-02-27 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);
2014-02-11 wenzelm 2014-02-11 maintain multiple command chunks and markup trees: for main chunk and loaded files; document view for all text areas, including auxiliary files;
2013-12-09 wenzelm 2013-12-09 browse directory hyperlink as well;
2013-12-09 wenzelm 2013-12-09 added document antiquotation @{url}, which produces formal markup for LaTeX and PIDE;
2013-11-20 wenzelm 2013-11-20 restrict node_required status and Theories panel to actual theories;
2013-11-20 wenzelm 2013-11-20 refer to thy_load command of auxiliary file;
2013-11-19 wenzelm 2013-11-19 tuned signature;
2013-11-19 wenzelm 2013-11-19 clarified Document.Blobs environment vs. actual edits of auxiliary files; more robust handling of vacuous edits;
2013-11-17 wenzelm 2013-11-17 centralized management of pending buffer edits;
2013-10-11 wenzelm 2013-10-11 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);
2013-09-24 wenzelm 2013-09-24 more tolerant treatment of end-of-buffer -- avoid debatable situations of jEdit buffer boundaries;
2013-09-24 wenzelm 2013-09-24 skip ignored commands, similar to former proper_command_at (see d68ea01d5084) -- relevant to Output, Query_Operation etc.; tuned signature;
2013-08-12 wenzelm 2013-08-12 manage hyperlinks via PIDE editor interface;
2013-08-12 wenzelm 2013-08-12 prefer PIDE editor operations; apply_query: insist in non-outdated snapshot via editor.current_command; tuned signature;
2013-08-12 wenzelm 2013-08-12 central management of Document.Overlays, independent of Document_Model;
2013-08-12 wenzelm 2013-08-12 tuned signature;
2013-08-12 wenzelm 2013-08-12 tuned signature;
2013-08-12 wenzelm 2013-08-12 tuned signature -- more abstract PIDE editor operations;