src/Tools/jEdit/src/jedit_editor.scala
Mon, 14 Jan 2019 13:58:12 +0100 wenzelm clarified message;
Sun, 13 Jan 2019 19:42:06 +0100 wenzelm support hyperlink to theory exports;
Tue, 05 Sep 2017 16:45:23 +0200 wenzelm less aggressive default position: prefer persistent defaults maintained by jEdit (amending 89c5bb2a2128);
Sun, 20 Aug 2017 18:30:20 +0200 wenzelm more robust shutdown, e.g. when plugin is stopped;
Sat, 17 Jun 2017 14:47:36 +0200 wenzelm maintain overlays within main state of document models;
Fri, 16 Jun 2017 15:59:27 +0200 wenzelm more general dispatcher operations;
Tue, 13 Jun 2017 21:15:40 +0200 wenzelm tuned signature;
Tue, 13 Jun 2017 20:19:25 +0200 wenzelm tuned;
Tue, 13 Jun 2017 20:16:39 +0200 wenzelm clarified modules;
Tue, 14 Mar 2017 21:43:54 +0100 wenzelm clarified singleton module;
Sun, 12 Mar 2017 17:59:03 +0100 wenzelm clarified current_command: index refers to node content, negative index means first command;
Sun, 12 Mar 2017 14:23:38 +0100 wenzelm discontinued pointless Text.Length: Javascript and Java agree in old-fashioned UTF-16;
Sat, 11 Mar 2017 16:22:12 +0100 wenzelm tuned;
Thu, 12 Jan 2017 11:17:05 +0100 wenzelm tuned signature;
Tue, 10 Jan 2017 16:53:05 +0100 wenzelm support "purge" operation on document model;
Sun, 08 Jan 2017 19:08:26 +0100 wenzelm added node_name(String): imitate jEdit buffer operations;
Sun, 08 Jan 2017 17:53:44 +0100 wenzelm tuned;
Sun, 08 Jan 2017 16:47:53 +0100 wenzelm resolve dependencies implicitly via File_Model, without jEdit Buffer_Model;
Sun, 08 Jan 2017 11:41:18 +0100 wenzelm refer to bibtex entries via general Document_Model, instead of editor buffers;
Sat, 07 Jan 2017 14:34:53 +0100 wenzelm separate Buffer_Model vs. File_Model;
Fri, 06 Jan 2017 13:27:18 +0100 wenzelm manage buffer models as explicit global state;
Thu, 05 Jan 2017 12:23:25 +0100 wenzelm misc tuning and clarification;
Wed, 28 Dec 2016 17:10:09 +0100 wenzelm clarified modules;
Wed, 28 Dec 2016 17:02:38 +0100 wenzelm clarified signature: explicit Length to avoid implicit mistakes;
Fri, 23 Dec 2016 19:19:59 +0100 wenzelm full range for Position.Item;
Fri, 23 Dec 2016 17:04:29 +0100 wenzelm tuned;
Fri, 23 Dec 2016 16:20:42 +0100 wenzelm tuned;
Fri, 23 Dec 2016 15:53:53 +0100 wenzelm tuned;
Fri, 23 Dec 2016 11:53:31 +0100 wenzelm tuned;
Thu, 22 Dec 2016 11:38:16 +0100 wenzelm clarified modules;
less more (0) -50 -30 tip