avoid output showing up in kill ring (via TextArea.setText, JEditBuffer.remove, UndoManager.contentRemoved), e.g. relevant for action "paste-deleted";

clarified breakgain: keeping it constant avoids margin fluctuation in Pretty_Tooltip vs. Pretty_Text_Area;

clarified signature;

clarified modules;

clarified modules;

clarified module name;

--HG--
rename : src/Tools/jEdit/src/rendering.scala => src/Tools/jEdit/src/jedit_rendering.scala

proper noWordSep as in "isabelle" mode (cf. 5024d0c48e02);

more thorough update;

bypass input method for better imitation of read-only mode (cf. f26a4d5e82b5): e.g. relevant for composition of ALT-u u on Mac OS X;

dummy input handler to imitate former read-only mode, which has changed its meaning in jedit-5.3.0 as mere hint for saving;

prefer Isabelle/Scala Future;

clarified modules;

--HG--
rename : src/Pure/Concurrent/simple_thread.ML => src/Pure/Concurrent/standard_thread.ML
rename : src/Pure/Concurrent/simple_thread.scala => src/Pure/Concurrent/standard_thread.scala

tuned;

proper fold painter according to jEdit options, not the hardwired default of JEditEmbeddedTextArea;

GUI.imitate_font: more explicit result size, e.g. relevant for caching;
some graphview font options: Helvetica family is important for self-contained PDF;
tuned;

tuned;

node-specific syntax, with base_syntax as default;
clarified Document_Model.init: convergence of editor events towards buffer-specific token marker;

clarified token marker / syntax for mode vs. buffer;

hardwired imitation of copy.shortcut2 default;

tuned imports;

clarified module name: facilitate alternative GUI frameworks;

--HG--
rename : src/Pure/GUI/swing_thread.scala => src/Pure/GUI/gui_thread.scala

tuned signature;

clarified detach_operation: ignore empty output;

enable "PIDE" docking framework by default, and rely on its "Detach" menu item;

clarified GUI events, e.g. relevant for insert via completion;

common support for search field, which is actually a light-weight Highlighter;

more uniform detach button;

tuned signature;

tuned signature;

--HG--
rename : src/Pure/System/interrupt.scala => src/Pure/System/posix_interrupt.scala

tuned whitespace;

tuned signature -- separate pool for JFuture tasks, which can be canceled;

tuned signature;

avoid "Adaptation of argument list by inserting ()" -- deprecated in scala-2.11.0;

observe extra line spacing for output as well;

do not absorb vacuous copy operation, e.g. relevant when tooltip has focus but no selection, while the main text area has a selection but no focus;

tuned;

tuned signature -- separate module Font_Info;

more uniform configuration of editor modes and token markers;

dismiss popups more uniformly;

avoid complication and event duplication due to KeyEventInterceptor -- NB: popup has focus within root window, it is closed on loss of focus;
uniform JEdit_Lib.propagate_key;

more standard key handling according to jEdit (with workaround);
clarified handling of ESCAPE (again): dismiss without second interpretation as select-none;

more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;

tuned signature;

tuned signature;

imitate "noWordSep" of isabelle mode, e.g. relevant for word selection via double-click;

support somewhat standard "select all" by default;

some attempts to avoid sandwiching of actions stemming from single ESCAPE key event, to avoid potential conflict with ongoing text selection;

explicit module Document_ID as source of globally unique identifiers across ML/Scala;

separate exec_id assignment for Command.print states, without affecting result of eval;
tuned signature;
tuned;

more aggresive ESCAPE handling, while retaining its regular meaning for jEdit;

manage popup windows via PopupFactory, which prefers light-weight JComponent, but might fall back on JWindow (despite JPanel of 0f88591478e6);
more explicit tooltip hierarchy: manage exactly the visible stack -- caching is part of PopupFactory;
auxiliary geometry measurement via single hidden window;
tuned signature;

reverted most of 5944b20c41bf -- tends to cause race condition of synchronous vs. asynchronous version;

no censorship of "view.fracFontMetrics", although it often degrades rendering quality;

apply small result immediately, to avoid visible delay of text update after window move;

allow fractional pretty margin -- avoid premature rounding;

more explicit Pretty.Metric, with clear distinction of unit (space width) vs. average char width (for visual adjustments) -- NB: Pretty formatting works via full space characters (despite a981a5c8a505 and 70f7483df9cb);
separate JEdit_Lib.pretty_metric, with slightly closer imitation of jEdit;

eliminated char_width_int to avoid unclear rounding;
clarified integer conversion for margin;

extra tooltip_delay after window.dismiss operation, to avoid flickering of quick reactivation;

recovered special background handling from 8d6e478934dc, particularly relevant for gutter border;

explicit handling of tooltip window stack -- avoid memory leak due to not-so-weak references to disposed windows (via event handlers and other aux. components);

more precise tooltip window size (NB: dimensions are known after layout pack, before making content visible);
more precise margin width based on fractional Pretty.char_width (avoid multiplication of rounding errors);
early initialization of gutter to get proper text area painter size (see also 2585c81d840a);

close tooltip after Active.action, to make it look more interactive (notably due to lack of dynamic update);

more uniform Pretty.char_width;

propagate keys to enclosing view like org.gjt.sp.jedit.gui.CompletionPopup, but without its KeyEventInterceptor;

more elementary key handling: listen to low-level KEY_PRESSED events (without consuming);

more informative error;

fold handling within Pretty_Text_Area, based on formal document content, which is static here;
fold subgoals;

init gutter according to view properties, which improves symmetry of windows and allows use of folds etc;

more formal class Command.Results;

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;

updated to jedit-5.0.0;

reset active areas on content update;

renamed main plugin object to PIDE;

quasi-abstract module Rendering, with Isabelle-specific implementation;

prefer buffer_edit combinator over Java-style boilerplate;

always refresh font metrics, to help window size calculation (amending 2585c81d840a);

take component width as indication if it is already visible/layed-out, to avoid multiple formatting with minimal margin;

tuned comment;

Rich_Text_Area tooltips via nested Pretty_Text_Area, based on some techniques of FoldViewer plugin;

tighten margin for TextArea instead of Lobo;

some support for hovering and sendback area;

tuned painter;

no caret painting;

text_rendering as managed task, with cancellation;

more direct GUI component;

minimal clipboard support (similar to org.lobobrowser.html.gui.HtmlBlockPanel);
tuned;

output is read-only;

token marker for extended syntax styles;

pass base_snapshot to enable hyperlinks into other nodes;
clarified "def" positions: refrain from renaming properties;
clarified snapshot.is_output vs. output and hyperlinks;

some actual rich text markup via XML.content_markup;
tuned signature;

some support for inital command markup;
tuned signature;

more static rendering state;

Pretty_Text_Area is based on Rich_Text_Area;

alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;