src/Tools/jEdit/src/output_dockable.scala
2016-12-20 wenzelm 2016-12-20 clarified module name;
2016-02-04 wenzelm 2016-02-04 recovered handle_resize from 5922db0430f1;
2015-11-21 wenzelm 2015-11-21 double flush to ensure persistent "state" output is reset; tuned GUI;
2015-11-21 wenzelm 2015-11-21 more thorough update of options;
2015-11-21 wenzelm 2015-11-21 more direct access to option "editor_output_state";
2015-09-21 wenzelm 2015-09-21 tuned;
2015-07-17 wenzelm 2015-07-17 more uniform ComponentAdapter;
2014-07-23 wenzelm 2014-07-23 clarified module name: facilitate alternative GUI frameworks;
2014-05-21 wenzelm 2014-05-21 more uniform Font_Info.Zoom_Box; misc tuning and clarification;
2014-05-21 wenzelm 2014-05-21 tuned signature;
2014-05-09 wenzelm 2014-05-09 always bounce focus back to main text area, unless explicit focus component is given here (see also 7b65f4da136d);
2014-05-08 wenzelm 2014-05-08 clarified detach_operation: ignore empty output;
2014-05-08 wenzelm 2014-05-08 bounce focus back to main text area -- Output is for output, not query input;
2014-05-08 wenzelm 2014-05-08 enable "PIDE" docking framework by default, and rely on its "Detach" menu item;
2014-05-08 wenzelm 2014-05-08 some odd tricks to provide "Detach" menu item, via "PIDE" docking framework;
2014-05-06 wenzelm 2014-05-06 tuned GUI layout;
2014-05-06 wenzelm 2014-05-06 common support for search field, which is actually a light-weight Highlighter;
2014-05-06 wenzelm 2014-05-06 more uniform detach button;
2014-05-06 wenzelm 2014-05-06 tuned signature;
2014-04-25 wenzelm 2014-04-25 clarified Session.Consumer, with Session.Outlet managed by dispatcher thread; eliminated old actors;
2014-04-22 wenzelm 2014-04-22 avoid "Adaptation of argument list by inserting ()" -- deprecated in scala-2.11.0;
2014-03-27 wenzelm 2014-03-27 more careful treatment of multiple command states (eval + prints): merge content that is actually required; more standard Markup_Tree merge, including trivial cases;
2014-03-01 wenzelm 2014-03-01 tuned signature -- separate module Font_Info;
2014-02-20 wenzelm 2014-02-20 tuned imports;
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-09-18 wenzelm 2013-09-18 improved FlowLayout for wrapping of components over multiple lines;
2013-08-24 wenzelm 2013-08-24 more uniform treatment of Swing_Thread context switch: prefer asynchronous Swing_Thread.later from actor;
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 tuned signature;
2013-08-02 wenzelm 2013-08-02 tuned;
2013-04-04 wenzelm 2013-04-04 tuned signature -- concentrate GUI tools;
2013-01-08 wenzelm 2013-01-08 more aggressive update -- potentially relevant for previously is_outdated output;
2012-12-15 wenzelm 2012-12-15 tuned signature;
2012-12-13 wenzelm 2012-12-13 more careful handling of Dialog_Result, with active area and color feedback; more formal type Command.Results; propagate command results to output, which is required to resolve update of dialog state; clarified Markup.message: retain uninterpreted messages;
2012-12-13 wenzelm 2012-12-13 identify dialogs via official serial and maintain as result message; clarified Protocol.is_inlined: suppress result/tracing/state messages uniformly; cumulate_markup/select_markup depending on command state; explicit Rendering.output_messages; tuned source structure;
2012-12-12 wenzelm 2012-12-12 rendering of selected dialog_result as active_result_color, depending on dynamic command status in output panel, but not static popups etc.;
2012-12-06 wenzelm 2012-12-06 discontinued obsolete "Tracing" button -- limited tracing channel works sufficiently well;
2012-11-25 wenzelm 2012-11-25 tuned signature;
2012-11-25 wenzelm 2012-11-25 tuned signature; uniform view.fontsize fallback;
2012-11-25 wenzelm 2012-11-25 renamed main plugin object to PIDE;
2012-11-21 wenzelm 2012-11-21 tuned;
2012-11-18 wenzelm 2012-11-18 update options via protocol; jEdit dialog for "Parallel Checking" options;
2012-10-17 wenzelm 2012-10-17 added Output "Detach" button;
2012-10-11 wenzelm 2012-10-11 refined separator: FBreak needs to be free for proper breaking, extra space at end helps to work around last-line oddity in jEdit;
2012-10-07 wenzelm 2012-10-07 detach tooltip as dockable window;
2012-10-04 wenzelm 2012-10-04 refined rich tooltip options; basic tooltips without markup;
2012-09-28 wenzelm 2012-09-28 smarter handling of tracing messages;
2012-09-28 wenzelm 2012-09-28 display number of tracing messages;
2012-09-22 wenzelm 2012-09-22 tuned signature;
2012-09-21 wenzelm 2012-09-21 merged
2012-09-21 wenzelm 2012-09-21 renamed Output to Output1 and Output2 to Output, and thus make the new version the default;
2012-09-18 wenzelm 2012-09-18 more explicit message markup and rendering;
2012-09-18 wenzelm 2012-09-18 some support for inital command markup; tuned signature;
2012-09-17 wenzelm 2012-09-17 renamed Text_Area_Painter to Rich_Text_Area;
2012-09-17 wenzelm 2012-09-17 tuned signature -- more general Text_Area_Painter operations;
2012-09-14 wenzelm 2012-09-14 refined output panel: more value-oriented approach to update and caret focus;
2012-09-11 wenzelm 2012-09-11 more options;
2012-09-07 wenzelm 2012-09-07 more explicit Delay operations;
2012-09-03 wenzelm 2012-09-03 actually reset output when there is no valid command span here (especially relevant at very end of jEdit buffer, which lacks the terminating newline);
2012-05-29 wenzelm 2012-05-29 update GUI components after init;