tuned signature -- facilitate testing;

tuned;

proper purge of auxiliary bibtex theory;

tuned;

tuned signature;

bibtex theory is always required and thus eventually consolidated;

avoid spurious noise: Prover IDE is meant to check for errors;

store full blob source for the sake of markup_to_XML;

action "isabelle.draft" for plain-text preview;

uniform preview for Isabelle/jEdit and Isabelle/VSCode;

tuned;

clarified URL: unique node name;

clarified modules;

proper HTML title;

isabelle.preview presents bibtex database files as well;

clarified signature;

isabelle.preview presents auxiliary text files as well;

tuned signature;

tuned signature;

tuned signature;

clarified modules;

tuned;

tuned signature;

support for HTTP/POST method;
more explict type HTTP.Arg;

tuned signature;

tuned signature;

clarified signature;

maintain overlays within main state of document models;
proper pending_input for Isabelle/VSCode;

clarified modules;

HTML preview based on PIDE markup;

clarified;

HTML preview via builtin HTTP server;

more explicit jEdit file operations;
less redundant JEdit_Resources.node_name();

provide session qualifier via resources;

clarified singleton module;

proper plugin access;

proper plugin access;

discontinued pointless Text.Length: Javascript and Java agree in old-fashioned UTF-16;

tuned;

tuned whitespace;

tuned signature;

tuned signature;

support "purge" operation on document model;

accomodate very big file_models and changed_files;

tuned;

update File_Model based on file-system events;

tuned;

resolve dependencies implicitly via File_Model, without jEdit Buffer_Model;

tuned;

tuned signature;

refer to bibtex entries via general Document_Model, instead of editor buffers;

clarified modules;

uniform Document.Model.node_edits (without void edits);

clarified check_thy_reader: check node_name here;

more uniform node_header (non-strict);
removed dead code;

tuned signature;

tuned signature;

clarified buffer events: exit model while loading;
misc tuning;

separate Buffer_Model vs. File_Model;
misc tuning and clarification;

manage buffer models as explicit global state;
tuned signature;

misc tuning and clarification;

tuned;

more uniform treatment of file name vs. theory name and special header;

tunes signature;

more IDE support for Isabelle/Pure bootstrap;

support ROOT0.ML as well -- independently of ROOT.ML;

treat ROOT.ML as theory with header "theory ML_Root imports ML_Bootstrap begin";

more thorough syntax_changed: new commands need require new folds;

double flush to ensure persistent "state" output is reset;
tuned GUI;

avoid highlighted area getting "stuck" after edit;

tuned signature;

more robust access to stable tip version: take all pending edits into account, don't assume model for current buffer;

more conservative Document_Model.init: avoid Document.Node.Clear due to change of token marker (e.g. due to change of jEdit mode properties);
clarified Isabelle.buffer_token_marker;

no GUI_Thread for SideKick parsers (in contrast to 4c8205fe3644), to avoid danger of deadlock due to nested context switch;

tuned;

tight span for theory header, which is relevant for error positions (including semantic completion);

avoid duplicate header errors, more precise positions;
tuned signature;

clarified span position;

tuned;

added Untyped.method convenience (for *this* class only);

tuned signature -- more explicit types;

more careful syntax_changed propagation -- avoid global jEdit.propertiesChanged;

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;

clarified modules;

clarified modules;

maintain Document_Model.bibtex_entries;
clarified Chunk predicates;

tuned -- eliminated redundant check (see 1f77110c94ef);

more frugal edits;

more explicit discrimination of empty nodes -- suppress from Theories panel;

clarified module name: facilitate alternative GUI frameworks;

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

tuned signature;

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;

some support for session-qualified theories: allow to refer to resources via qualified name instead of odd file-system path;

tuned signature;

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

simplified Text.Chunk -- eliminated ooddities;
afford strict symbol_index, which is usually empty anyway;

avoid data redundancy;

tuned signature -- moved Command.Chunk to Text.Chunk;

more explicit Command.Chunk types, less ooddities;
tuned;

tuned signature -- prefer static type Document.Node.Name;

store blob content within document node: aux. files that were once open are made persistent;
proper structural equality for Command.File and Symbol.Index;

tuned signature;

clarifed module name;

--HG--
rename : src/Pure/Thy/thy_load.ML => src/Pure/PIDE/resources.ML
rename : src/Pure/Thy/thy_load.scala => src/Pure/PIDE/resources.scala
rename : src/Tools/jEdit/src/jedit_thy_load.scala => src/Tools/jEdit/src/jedit_resources.scala

clarified init_models: simultaneous initialization of all document models, before flushing edits by regular means (via PIDE.editor.invoke) -- important for consolidated doc_blobs when determining initial edits;
clarified asynchronous event propagation: determine buffers where they are actually accessed;
tuned signature;

reparse only for actually changed blobs;
tuned signature;

proper document blobs for initial edit, which is relevant for loading auxiliary file buffers;

more formal Document.Blobs;
removed junk;

proper update of text perspective for nodes with changed blobs, which is important to refresh the corresponding command perspective (otherwise it might refer to invalid thy_load commands and cause full execution of the node by the prover);

tuned comment;

maintain blob edits within history, which is important for Snapshot.convert/revert;

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

common Command.Chunk for command source and auxiliary files (static Symbol.Index without actual String content);
more informative type Blob, to allow markup reports;

restrict node_required status and Theories panel to actual theories;

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

clarified Document.Blobs environment vs. actual edits of auxiliary files;
more robust handling of vacuous edits;

inline blobs into command, via SHA1 digest;
broadcast all blobs within edit, without storing the result;

caching of blob;
precise file content according to jEdit IO;

maintain document model for all files, with document view for theory only, and special blob for non-theory files;

tuned;

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

central management of Document.Overlays, independent of Document_Model;

tuned signature;

tuned signature;

tuned signature -- more uniform treatment of overlays as command mapping;

tuned signature;

avoid repeated PIDE.flush_buffers when manipulating overlays;

maintain overlays within node perspective;
tuned signature;

tuned signature;

home-grown mouse handling to pretend that the painted checkbox is actually a Swing component;
tuned signature;

actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
just one module for Isabelle/jEdit actions;

allow explicit indication of required node: full eval, no prints;

simplified flag for continuous checking: avoid GUI complexity and slow checking of all theories (including prints);

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

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

tuned property name;

tuned signature in accordance to document operations;

emit bulk edits on initialization of multiple buffers, which greatly improves performance when starting big sessions (e.g. JinjaThreads);

tuned signature;

renamed main plugin object to PIDE;

tuned signature;

somewhat more general JEdit_Lib;
tuned signatures;

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

more options;

more explicit Delay operations;

find files via load commands within theory text;
clarified Thy_Load.with_thy_text, simplified Thy_Load.check_thy;

pass syntax through check_thy;

use Thy_Header.read on explicit text only -- potentially via File.read, not Scan.byte_reader;
tuned signatures;

simplified Document.Node.Header -- internalized errors;

more robust update_perspective, e.g. required after reload of buffer that is not at start position;

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;

more explicit indication of swing thread context;

more robust locking;

refined node_header -- more direct buffer access (again);

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

clarified document nodes (full import graph) vs. node_status (non-preloaded theories);
tuned;

more defensive node_header;

clarified module Thy_Load;
more precise graph based on Document.Node.Deps with actual Node.Name dependencies;

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

more abstract Document.Node.Name;
tuned signature;

refined document state assignment: observe perspective, more explicit assignment message;
misc tuning and clarification;

slightly more abstract Text.Perspective;

early filtering of unchanged perspective;

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;

propagate editor perspective through document model;

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

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

clarified node header -- exclude master_dir;

clarified document model header: master_dir (native wrt. editor, potentially URL) and node_name (full canonical path);

propagate header changes to prover process;
simplified Document case classes;
Document.State.assignments: indexed by Version_ID;

clarified propagation of node name and header;

some support for blobs (arbitrary text files) within document nodes;

explicit Document.Node.Header, with master_dir and thy_name;
imitate ML path operations more closely;

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

more explicit edit_node vs. init_node;
some support for master_dir and header;

tuned signature;

clarified init/exit procedure;

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

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

more robust init;

more elaborate syntax styles;

builtin sub/superscript styles for jedit-4.3.2;

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