tuned;

tuned signature;

tuned signature;

clarified modules;

clarified modules;

clarified module name;

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

clarified modules;

tuned signature;

support more modes;

explicit kind "before_command";
tuned signature;

clarified modules;

--HG--
rename : src/Tools/jEdit/src/structure_matching.scala => src/Tools/jEdit/src/text_structure.scala

basic setup for indentation;

clarified symbol insertion, depending on buffer encoding;

tuned signature;

tuned message;

support for 'restricted' modifier: only qualified accesses outside the local scope;

more general notion of command span: command keyword not necessarily at start;
support for special 'private' prefix for local_theory commands;
clarified parse_spans, with related operations for document Thy_Output and editor Token_Markup;

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 signature;

tuned signature;

tuned signature -- more explicit types;

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;

encode text with control symbols;

more iterators;

find command span in buffer;
tuned signature;

added option jedit_structure_limit;
tuned signature;

some structure matching, based on line token iterators;

support for structure matching;
misc tuning;

make double-sure that line context is present, e.g. relevant for last line after visible text;

tuned signature;

tuned signature;

tuned signature;

more explicit Line_Nesting;

support line context with depth;
basic setup for "isabelle" fold handling;
misc tuning;

proper type comparison (amending cd4439d8799c);

buffer_line_context via untyped access;

support for bibtex token markup;
more robust ML token marker: no_context;
tuned signature;

clarified module name: facilitate alternative GUI frameworks;

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

more robust bold_style, e.g. relevant for accidental \<^bold> before keyword;

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

separate tokenization and language context for SML: no symbols, no antiquotes;

separate "sml" mode, suppress old "ml" mode altogether;

tuned signature -- emphasize line-oriented aspect;

isabelle-ml mode with separate token marker;
clarified ML_Lex.gap_start: end-of-input counts as single newline;

tuned signature;

completion popup for history text field;
imitate view font, for default rendering of symbols;
tuned signature;

explicit indication of outer syntax with no tokens;
uniform Isabelle.markers, based on syntax specification -- no tokens for NEWS;

always use extended styles (despite de26cf3191a3);

more uniform configuration of editor modes and token markers;

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;

tuned -- help finding rare NPE on cold start;

discontinued special treatment of \<^isub> and \<^isup> in rendering or editor front-end;
document antiquotations: renamed term style "isub" to "sub";

more liberal edit_control_style: include preceeding control symbol to reduce potential for user surprise;

no special treatment of control_reset, in accordance to other control styles;

renamed main plugin object to PIDE;

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

retain hidden_color (i.e. transparent white) instead of replacing it by semantic text color, to make control symbols more hidden and avoid "dirty" lines with some fonts;

prefer buffer_edit combinator over Java-style boilerplate;

special handling of control symbols in Symbols dockable;
less obscure Scala names;

improved editing support for control styles;
separate module for Isabelle actions;

clarified global get_recent_syntax: session always has its base_syntax, but it might be absent itself;

more token markers, based on actual outer syntax;
prefer official Outer_Syntax.init with its completions;

refined init_model: allow change of buffer name as caused by "Save as", for example;
avoid init_model while buffer.isLoading -- potentially prevent NPE of getText;
avoid emitting nested buffer.propertiesChanged events;

maintain Version.syntax within document state;
clarified Outer_Syntax.empty vs. Outer_Syntax.init, which pulls in Isabelle_System symbol completions;

paranoia null check -- prevent spurious crash of jedit token markup;

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

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

improved handling of extended styles and hard tabs when prover is inactive;

mark hard tabs as single chunks, as required by jEdit;

more robust initialization of token marker and line context wrt. session startup;

avoid actual Color.white, which would be turned into Color.black by org.gjt.sp.jedit.print.BufferPrintable;

default style for user fonts -- to prevent org.gjt.sp.jedit.print.BufferPrintable from choking on null;

some convenience actions/shortcuts for control symbols;

simplified Symbol based on lazy Symbol.Interpretation -- reduced odd "functorial style";
tuned implicit build/init messages;

simplified Symbol.iterator: produce strings, which are mostly preallocated;
eliminated Symbol.CharSequence complications;

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

proper tokens only if session is ready;

clarified decoded control symbols;

more precise font transformations: shift sub/superscript, adjust size for user fonts;
tuned;

hidden font: full height makes cursor more visible;

tuned iteration over short symbols;

Symbol.is_ctrl: handle decoded version as well;
clarified user font font index handling;

some support for user symbol fonts;

added SyntaxUtilities.StyleExtender hook, with actual functionality in Isabelle/Scala;

treat quotes as non-controllable, to reduce surprise in incremental editing;

support for bold style within text buffer;
hidden: white foreground;

--HG--
rename : src/Tools/jEdit/patches/scriptstyles => src/Tools/jEdit/patches/extended_styles

discontinued special treatment of \<^loc> (which was original meant as workaround for "local" syntax);

some unicode chars for special control symbols;

avoid setTokenMarker fluctuation on buffer reload etc. via static isabelle_token_marker, which is installed by hijacking the jEdit ModeProvider;

basic support for extended syntax styles: sub/superscript;

tuned signature;

simplified Line_Context (again);

more precise imitatation of original TokenMarker: no locking, interned context etc.;

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