added option jedit_text_overview for visual appearance (not performance, see also 72216713733a);

tuned signature;

clarified signature;

clarified modules;

eliminated redundant check (see also 27328dcaf64c vs. 9c53198dbb1c);

clarified singleton module;

clarified modules;

tuned signature;

separate Buffer_Model vs. File_Model;
misc tuning and clarification;

misc tuning and clarification;

clarified module name;

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

explicit option editor_generated_input_delay, which is more aggressive by default;

delay_first for machine generated editor events: avoid starvation, e.g. when operating on big sessions;

more thorough update;

background color for entity def/ref focus;

tuned;

more thorough GUI update;

render snapshot.is_outdated in text overview, where other status information is shown already;

fast synchronous painting and asynchronous refresh of text overview, reduces GUI thread latency from 100ms to 1ms for big files like src/HOL/Multivariate_Analsyis/Integration.thy;

more informative gutter content: fall-back on background color, e.g. when line numbers are enabled;
non-transparent information_message_color like other message colors;
removed unused error1_color;

support for structure matching;
misc tuning;

clarified module name: facilitate alternative GUI frameworks;

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

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

mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;

clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
eliminated old actors;

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

more explicit message discrimination;

tuned signature -- more explicit iterator terminology;

tuned for-comprehensions -- less structure mapping;

tuned signature;

tuned signature -- weaker type requirement;

tuned imports;

maintain multiple command chunks and markup trees: for main chunk and loaded files;
document view for all text areas, including auxiliary files;

ranges of thy_load commands count as visible within perspective;
convert ranges wrt. snapshot -- relevant for outdated situation;

centralized management of pending buffer edits;

tuned imports;

clarified Editor.current_command: allow outdated snapshot;
more accurate Document_View.perspective based on current_command for proper state output (see also 88c6e630c15f and ef62204a126b);

caret range of active text area counts as visible (e.g. relevant for Output after scrolling outside of text view);

maintain Completion_Popup.Text_Area as client property like Document_View;
global Completion_Popup.Text_Area init/exit like SideKickPlugin;
eliminated old SideKick completion -- cover all Isabelle modes uniformly;
dynamic lookup of Isabelle.mode_syntax -- NB: buffer mode might be undefined in intermediate stages;

more abstract Completion_Popup.Text_Area;
more uniform font size;

tuned;

dismiss popups more uniformly;

tuned signature;

some actual completion via outer syntax;
disable old SideKick completion for "isabelle" mode;

some key event handling in the manner of SideKickBindings, SideKickCompletionPopup;

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;

back to model.update_perspective with delay (cf. a20631db9c8a);

support declarative editor_execution_range, instead of old-style check/cancel buttons;

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

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

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

more direct invalidateScreenLineRange after changed assignment;

tuned signature in accordance to document operations;

updated to jedit-5.0.0;

tuned signature;

renamed main plugin object to PIDE;

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

further refinement of jEdit line range, avoiding lack of final \n;

some support for hovering and sendback area;

more robust GUI component handlers;

renamed Text_Area_Painter to Rich_Text_Area;

--HG--
rename : src/Tools/jEdit/src/text_area_painter.scala => src/Tools/jEdit/src/rich_text_area.scala

tuned signature -- more general Text_Area_Painter operations;

tuned signature;

tuned signature;

somewhat more general JEdit_Lib;
tuned signatures;

no longer react on global_settings (cf. 34ac36642a31);

refined output panel: more value-oriented approach to update and caret focus;

clarified markup names;

more general Document_Model.point_range;
more general Document_View.Active_Area;
eliminated dead popup material;

more static handling of rendering options;

more options;

postpone update of text overview panel after incoming session edits, to improve reactivity of editing massive theories like src/HOL/Multivariate_Analysis;

more explicit Delay operations;

support for direct hyperlinks, without the Hyperlinks plugin;

less warning in scala-2.10.0-M3;

tuned imports;

explicit propagation of assignment event, even if changed command set is empty;
discontinued slightly odd Document_View.update_snapshot/flush_snapshot;

further amendment of "updated" edge (cf. 6ed49c52d463) -- required for repainting of unassigned command, e.g. for inactive buffe;

misc tuning to accomodate scala-2.10.0-M2;

more explicit indication of swing thread context;

prefer asynchronous context switch from actor to swing thread, to reduce danger of deadlocks;
more robust use of Session.Commands_Changed vs. Document_View.visible_range as asynchronous swing task, taking into account that the model might have switched in the meantime (e.g. via fast clicking on hypersearch while the prover is crunching);

tuned comment;

removed obsolete proper_command_at (cf. 03a2dc9e0624);

clarified special eol treatment and moved to gfx_range -- enables error messages at end of input, e.g. "prop PROP";

explicitly revoke delay, to avoid spurious timer events after deactivation of related components;

more robust visible_range: allow empty view;

separate module for text status overview;

overview.delay_repaint: avoid wasting GUI cycles via update_delay;
prefer delay_first for prover initiated events -- avoid indefinite delay;

observe HEIGHT of overview ticks;
misc tuning and clarification;

more careful painting of overview component: more precise and more efficient;

back to more basic caret_range (reverting 0ad063afa3d6) -- BreakIterator crashes due to non-zero text.offset when deleting the first character of the buffer;

more precise rendering of overview_color/gutter_message/squiggly_underline based on cumulation of command status and warning/error messages;

ignore empty gfx_range;
tuned;

clarified Isabelle_Rendering vs. physical painting;
discontinued slightly odd object-oriented Markup_Tree.Cumulate/Select;

caret_range based on BreakIterator, which handles combined unicode characters as well;

renamed Isabelle_Markup to Isabelle_Rendering to emphasize its meaning and make room for Pure Isabelle_Markup module;

--HG--
rename : src/Tools/jEdit/src/isabelle_markup.scala => src/Tools/jEdit/src/isabelle_rendering.scala

tuned signature;

more tooltip content;

clarified terminology;

added "check" button: adhoc change to full buffer perspective;

more abstract Document.Node.Name;
tuned signature;

tuned Commands_Changed: cover nodes as well;

restrict perspective to actual buffer_range, to avoid spurious edits due to faulty last_exec_offset (NB: jEdit screenlines may be silently extended by trailing newline);

slightly more abstract Text.Perspective;

more reliable update_perspective handler based on actual text visibility (e.g. on startup or when resizing without scrolling);

update_perspective without actual edits, bypassing the full state assignment protocol;
edit_nodes/Perspective: do not touch_descendants here;
propagate editor scroll events via update_perspective;
misc tuning;

added official Text.Range.Ordering;
some support for text perspective;

tuned signature;

quasi-static Isabelle_System -- reduced tendency towards "functorial style";

imitate exception ERROR of Isabelle/ML;

explicit import java.lang.System to prevent odd scope problems;

init/exit model/view synchronously within the swing thread -- EditBus.send in jedit-4.4.1 always runs there;

more robust caret painting wrt. surrogate characters;
discontinued glyphvector drawing -- less special cases;

flush snapshot on falling edge of is_outdated -- recover effect of former buffer.propertiesChanged on text area (cf. f0770743b7ec);

more precise imitation of original TextAreaPainter: no locking;

static token markup, based on outer syntax only;
eliminated obsolete buffer.propertiesChanged (expensive due to remarking of full buffer etc.);

uniform use of Document_View.robust_body;

more robust init;

more precise caret painting, working around existing painter (which is reinstalled by jEdit occasionally);

paint caret according to precise font metrics;

builtin sub/superscript styles for jedit-4.3.2;

recovered tooltip Entity content (odd effect of layer change!? cf. 806878ae2219);

separate module for text area painting;

--HG--
rename : src/Tools/jEdit/src/text_painter.scala => src/Tools/jEdit/src/text_area_painter.scala

some direct text foreground painting, instead of token marking;
common snapshot for all text area painters (NOT gutter etc.)
tuned;

separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;

moved sources -- eliminated Netbeans artifact of jedit package directory;

--HG--
rename : src/Tools/jEdit/src/jedit/dockable.scala => src/Tools/jEdit/src/dockable.scala
rename : src/Tools/jEdit/src/jedit/document_model.scala => src/Tools/jEdit/src/document_model.scala
rename : src/Tools/jEdit/src/jedit/document_view.scala => src/Tools/jEdit/src/document_view.scala
rename : src/Tools/jEdit/src/jedit/html_panel.scala => src/Tools/jEdit/src/html_panel.scala
rename : src/Tools/jEdit/src/jedit/isabelle_encoding.scala => src/Tools/jEdit/src/isabelle_encoding.scala
rename : src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala => src/Tools/jEdit/src/isabelle_hyperlinks.scala
rename : src/Tools/jEdit/src/jedit/isabelle_markup.scala => src/Tools/jEdit/src/isabelle_markup.scala
rename : src/Tools/jEdit/src/jedit/isabelle_options.scala => src/Tools/jEdit/src/isabelle_options.scala
rename : src/Tools/jEdit/src/jedit/isabelle_sidekick.scala => src/Tools/jEdit/src/isabelle_sidekick.scala
rename : src/Tools/jEdit/src/jedit/output_dockable.scala => src/Tools/jEdit/src/output_dockable.scala
rename : src/Tools/jEdit/src/jedit/plugin.scala => src/Tools/jEdit/src/plugin.scala
rename : src/Tools/jEdit/src/jedit/protocol_dockable.scala => src/Tools/jEdit/src/protocol_dockable.scala
rename : src/Tools/jEdit/src/jedit/raw_output_dockable.scala => src/Tools/jEdit/src/raw_output_dockable.scala
rename : src/Tools/jEdit/src/jedit/scala_console.scala => src/Tools/jEdit/src/scala_console.scala
rename : src/Tools/jEdit/src/jedit/session_dockable.scala => src/Tools/jEdit/src/session_dockable.scala