src/Tools/jEdit/src/plugin.scala
2017-06-05 wenzelm 2017-06-05 HTML preview via builtin HTTP server;
2017-04-24 wenzelm 2017-04-24 clarified modules;
2017-04-23 wenzelm 2017-04-23 prefer strict operation (despite 8edca3465758): there might be errors from all_known = true (ae09b9f5980b);
2017-04-21 wenzelm 2017-04-21 afford unconditional all_known = true (reverting ea42dfd95ec8), for practical usability of qualified imports from arbitrary sessions;
2017-04-19 wenzelm 2017-04-19 optionally explore all sessions -- potentially slow, e.g. for AFP;
2017-04-11 wenzelm 2017-04-11 more informative known_files: known_theories within the local session directory come first; more thorough Session.Base.platform_path;
2017-04-03 wenzelm 2017-04-03 tuned;
2017-04-03 wenzelm 2017-04-03 provide session qualifier via resources;
2017-03-19 wenzelm 2017-03-19 updated to jedit-5.4.0;
2017-03-18 wenzelm 2017-03-18 more informative session result;
2017-03-16 wenzelm 2017-03-16 tuned;
2017-03-16 wenzelm 2017-03-16 clarified message: exception output usally happens in a context without extra newline;
2017-03-15 wenzelm 2017-03-15 clarified message;
2017-03-15 wenzelm 2017-03-15 keep PIDE.plugin for the sake of still open dockables etc. -- jEdit exits these *after* the stop operation;
2017-03-15 wenzelm 2017-03-15 keep style extender for the sake of potentially remaining token markers;
2017-03-15 wenzelm 2017-03-15 dynamic session_options for tuning parameters and initial prover options;
2017-03-15 wenzelm 2017-03-15 strict initialization of plugin.session: no user errors to be expected before session.start;
2017-03-15 wenzelm 2017-03-15 resources are part of early/strict initialization, but session_base is permissive to avoid crash of "isabelle jedit -l BAD"; PIDE._plugin indicates intialization state of Plugin; tuned;
2017-03-15 wenzelm 2017-03-15 clarified initialization; tuned;
2017-03-15 wenzelm 2017-03-15 clarified initialization;
2017-03-15 wenzelm 2017-03-15 clarified modules;
2017-03-15 wenzelm 2017-03-15 more explicit strict vs. non-strict initialization;
2017-03-15 wenzelm 2017-03-15 more explicit options; tuned signature;
2017-03-14 wenzelm 2017-03-14 tuned signature;
2017-03-14 wenzelm 2017-03-14 tuned;
2017-03-14 wenzelm 2017-03-14 tuned signature;
2017-03-14 wenzelm 2017-03-14 clarified singleton module;
2017-03-14 wenzelm 2017-03-14 proper plugin access;
2017-03-14 wenzelm 2017-03-14 clarified modules;
2017-03-14 wenzelm 2017-03-14 proper plugin access;
2017-03-14 wenzelm 2017-03-14 tuned;
2017-03-14 wenzelm 2017-03-14 prefer local variables;
2017-03-14 wenzelm 2017-03-14 clarified modules;
2017-03-14 wenzelm 2017-03-14 avoid global variables with implicit initialization;
2017-03-14 wenzelm 2017-03-14 more robust early initialization;
2017-03-14 wenzelm 2017-03-14 afford early initialization of JEdit_Options, but it may lead to messy exception trace for malformed etc/preferences (see also 6eeaaefcea56); tuned signature;
2017-03-14 wenzelm 2017-03-14 tuned;
2017-03-14 wenzelm 2017-03-14 more robust debugger initialization, e.g. required for GUI components before actual session startup;
2017-03-13 wenzelm 2017-03-13 proper local debugger state, depending on session; tuned signature;
2017-03-13 wenzelm 2017-03-13 tuned signature;
2017-03-13 wenzelm 2017-03-13 clarified Session.Phase;
2017-01-12 wenzelm 2017-01-12 tuned signature;
2017-01-12 wenzelm 2017-01-12 tuned signature;
2017-01-09 wenzelm 2017-01-09 update File_Model based on file-system events;
2017-01-09 wenzelm 2017-01-09 clarified modules; tuned;
2017-01-09 wenzelm 2017-01-09 tuned signature;
2017-01-08 wenzelm 2017-01-08 tuned signature;
2017-01-08 wenzelm 2017-01-08 avoid immediate editor.flush on buffer events;
2017-01-08 wenzelm 2017-01-08 resolve dependencies implicitly via File_Model, without jEdit Buffer_Model;
2017-01-07 wenzelm 2017-01-07 clarified buffer events: exit model while loading; misc tuning;
2017-01-07 wenzelm 2017-01-07 separate Buffer_Model vs. File_Model; misc tuning and clarification;
2017-01-06 wenzelm 2017-01-06 manage buffer models as explicit global state; tuned signature;
2016-12-20 wenzelm 2016-12-20 clarified module name;
2016-12-18 wenzelm 2016-12-18 added isabelle jedit -R; errors in session_info/session_content are ignored and deferred to later checks of Build.build;
2016-11-24 wenzelm 2016-11-24 explicit option editor_generated_input_delay, which is more aggressive by default;
2016-11-23 wenzelm 2016-11-23 delay_first for machine generated editor events: avoid starvation, e.g. when operating on big sessions;
2016-11-10 wenzelm 2016-11-10 more robust jedit_auto_resolve: avoid losing events deps_changed() / delay_load.invoke();
2016-09-01 wenzelm 2016-09-01 tuned GUI: modal dialog last;
2016-09-01 wenzelm 2016-09-01 separate action; tuned message;
2016-09-01 wenzelm 2016-09-01 check keymap changes on startup;