src/Tools/jEdit/src/output_dockable.scala
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;
2012-04-19 wenzelm 2012-04-19 more robust wrt. exceptions;
2012-04-18 wenzelm 2012-04-18 more robust Sendback handling: JVM/jEdit paranoia for case matching, treat Pretty body not just XML.Text, replace proper_range only (without trailing whitespace);
2012-03-19 wenzelm 2012-03-19 explicit propagation of assignment event, even if changed command set is empty; discontinued slightly odd Document_View.update_snapshot/flush_snapshot;
2012-03-01 wenzelm 2012-03-01 explicitly revoke delay, to avoid spurious timer events after deactivation of related components;
2012-02-21 wenzelm 2012-02-21 overview.delay_repaint: avoid wasting GUI cycles via update_delay; prefer delay_first for prover initiated events -- avoid indefinite delay;
2012-01-14 wenzelm 2012-01-14 tuned signature;
2011-11-28 wenzelm 2011-11-28 separate module for concrete Isabelle markup;
2011-09-07 wenzelm 2011-09-07 clarified terminology;
2011-08-31 wenzelm 2011-08-31 tuned Commands_Changed: cover nodes as well;
2011-08-30 wenzelm 2011-08-30 tuned signature;
2011-07-04 wenzelm 2011-07-04 quasi-static Isabelle_System -- reduced tendency towards "functorial style";
2011-06-23 wenzelm 2011-06-23 explicit import java.lang.System to prevent odd scope problems;
2011-06-17 wenzelm 2011-06-17 flush snapshot on falling edge of is_outdated -- recover effect of former buffer.propertiesChanged on text area (cf. f0770743b7ec);
2011-06-08 wenzelm 2011-06-08 moved sources -- eliminated Netbeans artifact of jedit package directory;