src/Tools/jEdit/src/jedit_lib.scala
2016-04-14 wenzelm 2016-04-14 background color for entity def/ref focus;
2016-02-04 wenzelm 2016-02-04 re-init document views for the sake of Text_Overview size;
2015-12-19 wenzelm 2015-12-19 tuned signature;
2015-09-19 wenzelm 2015-09-19 tuned signature;
2015-08-20 wenzelm 2015-08-20 clarified modules, like ML version;
2015-08-20 wenzelm 2015-08-20 tuned signature, according to ML version;
2015-05-03 wenzelm 2015-05-03 misc tuning, based on warnings by IntelliJ IDEA;
2015-02-28 wenzelm 2015-02-28 updated to jedit-5.2.0; updated CommonControls.jar, kappalayout.jar, MacOSX.jar, SideKick.jar;
2014-12-02 wenzelm 2014-12-02 node-specific syntax, with base_syntax as default; clarified Document_Model.init: convergence of editor events towards buffer-specific token marker;
2014-12-01 wenzelm 2014-12-01 clarified token marker / syntax for mode vs. buffer;
2014-08-03 wenzelm 2014-08-03 more robust popup geometry vs. formatted margin;
2014-07-23 wenzelm 2014-07-23 clarified module name: facilitate alternative GUI frameworks;
2014-05-09 wenzelm 2014-05-09 tuned signature;
2014-05-02 wenzelm 2014-05-02 more frugal access to theory text via Reader, reduced costs for I/O text decoding; prefer non-strict Symbol.decode, since Reader[Char] may present symbols in either way;
2014-04-28 wenzelm 2014-04-28 tuned -- fewer aliases of critical operations;
2014-04-24 wenzelm 2014-04-24 further robustification wrt. unclear ranges;
2014-04-22 wenzelm 2014-04-22 avoid "Adaptation of argument list by inserting ()" -- deprecated in scala-2.11.0;
2014-04-15 wenzelm 2014-04-15 back to unrestricted before_caret_range, which is important for quick editing at the end of line (amending 83777a91f5de);
2014-04-15 wenzelm 2014-04-15 prefer direct caret_range for update_dictionary actions, which usually happen outside the flow of editing; more robust point_range; tuned;
2014-04-15 wenzelm 2014-04-15 more robust JEdit_Lib.line_range, according to usual jEdit confusion at end of last line;
2014-04-15 wenzelm 2014-04-15 clarified before_caret_range: prevent continuation on next line; more robust jedit_text_areas in unclear situations of object initialization;
2014-04-14 wenzelm 2014-04-14 some actions to maintain spell-checker dictionary;
2014-04-07 wenzelm 2014-04-07 tuned signature -- prefer static type Document.Node.Name;
2014-02-28 wenzelm 2014-02-28 more regular buffer_range, despite 47e8c8daccae; more robust invalidate_range, which is relevant when editing at the end of the buffer (NB: last line offset by be outside actual buffer length);
2014-02-26 wenzelm 2014-02-26 more precise before_caret_range (looking both in space and time);
2014-02-23 wenzelm 2014-02-23 tuned whitespace;
2014-02-23 wenzelm 2014-02-23 clarified stretch_point_range wrt. UTF-16 surrogates; tuned;
2014-02-18 wenzelm 2014-02-18 clarified special eol treatment (amending 3d55ef732cd7): allow last line to be empty, which means stop == end for second-last line;
2013-09-22 wenzelm 2013-09-22 tuned;
2013-09-22 wenzelm 2013-09-22 completion popup for history text field; imitate view font, for default rendering of symbols; tuned signature;
2013-09-18 wenzelm 2013-09-18 tuned signature;
2013-08-29 wenzelm 2013-08-29 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;
2013-08-28 wenzelm 2013-08-28 uniform use of isabelle.jEdit.Popup, based on generic screen location operations;
2013-08-27 wenzelm 2013-08-27 enable jEdit KeyEventWorkaround uniformly;
2013-08-27 wenzelm 2013-08-27 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;
2013-08-27 wenzelm 2013-08-27 more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
2013-08-24 wenzelm 2013-08-24 strict checking of coordinates wrt. inner painter component;
2013-08-13 wenzelm 2013-08-13 more general window_geometry;
2013-08-13 wenzelm 2013-08-13 attempt to transfer focus back to main window after closing popups, which is potentially relevant for heavy-weight windows (cf. workaround in org/gjt/sp/jedit/gui/CompletionPopup.java);
2013-08-05 wenzelm 2013-08-05 query process animation;
2013-08-05 wenzelm 2013-08-05 tuned signature;
2013-06-29 wenzelm 2013-06-29 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;
2013-03-25 wenzelm 2013-03-25 tuned signature;
2013-03-23 wenzelm 2013-03-23 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;
2013-03-21 wenzelm 2013-03-21 eliminated char_width_int to avoid unclear rounding; clarified integer conversion for margin;
2013-02-06 wenzelm 2013-02-06 more robust JEdit_Lib.pixel_range, which could crash via Rich_Text_Area.tooltip_painter with bad mouse coordinates;
2013-01-12 wenzelm 2013-01-12 more uniform Pretty.char_width;
2012-12-31 wenzelm 2012-12-31 tuned signature;
2012-12-16 wenzelm 2012-12-16 tuned signature: use thy_load to adapt to prover/editor specific view on sources;
2012-12-15 wenzelm 2012-12-15 more general handling of graphics configurations, to increase chance of proper positioning of tooltips in multi-screen environment; more tooltip options via Rendering;
2012-12-05 wenzelm 2012-12-05 tuned signature in accordance to document operations;
2012-11-26 wenzelm 2012-11-26 more general sendback properties; support for padding of line boundary, e.g. for ad-hoc insertion of commands via 'help';
2012-11-24 wenzelm 2012-11-24 prefer buffer_edit combinator over Java-style boilerplate;
2012-11-24 wenzelm 2012-11-24 recovered some tooltip wrapping from e2762f962042, with multi-line support via HTML.encode;
2012-11-18 wenzelm 2012-11-18 more accurate pixel_range -- do not round offset here;
2012-11-18 wenzelm 2012-11-18 tuned signature;
2012-10-19 wenzelm 2012-10-19 more precise pixel_range: avoid popup when pointing into empty space after actual end-of-line;
2012-10-12 wenzelm 2012-10-12 further refinement of jEdit line range, avoiding lack of final \n;
2012-10-05 wenzelm 2012-10-05 further support for nested tooltips;
2012-10-05 wenzelm 2012-10-05 refer to parent frame -- relevant for floating dockables in particular;