more sequential access to Session.manager.global_state: avoid minor divergence of tip version;

clarified inversion of file name to theory name, notably for Windows;

tuned signature;

find theory files via session structure: much faster Prover IDE startup;

find theory node name via session directories;

tuned imports -- accommodate scala-2.13.0-RC3;

static type for Library.using: avoid Java 11 warnings on "Illegal reflective access";
more uses of "using";

more uniform read_file_content for Isabelle/jEdit and Isabelle/VSCode: make_theory_content is required for semantic checking of user file-formats (e.g. bibtex);

more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;

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

implicit thy_load context for bibtex files (VSCode);

clarified theory_name vs. loaded_theory: proper import_name for already loaded theories from other sessions (amending 4c98c929a12a);

tuned signature (again, see 1a9e2a2bf251);

tuned signature;

tuned signature;

clarified modules;

tuned;

tuned signature;

recode Unicode text on the spot, e.g. from copy-paste of output;

store document version;

retain symlinks in file names from VSCode: relevant for proper file locations in decorations etc.;

clarified platform file operations;

proper bootstrap_name (amending b42743f5b595);

tuned signature;

tuned signature;

added commands for spell-checker dictionary;

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

proper treatment of editor overlays;

clarified signature;

tuned signature;

restricted perspective depending on the caret -- important for reactivity when editing big files;

eliminated default_qualifier: just a constant;

tuned signature;

prefer formal name from session context, for proper qualified theory name;

tuned signature (again);

tuned;

clarified loaded_theories: map to qualified theory name;
proper theory_name for PIDE editors;

clarified signature;

more session_base information in ML;
tuned signature;

tuned signature;

provide session qualifier via resources;

avoid race condition between current_state().stable_tip_version and model.rendering();

clarified caret offset;
show output at end of file;

tuned signature;

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

dynamic output, depending on caret focus (see also Tools/jEdit/src/output_dockable.scala);

support for caret handling and dynamic output;

incremental document changes;

decorations for spell-checker;

clarified options;

tuned;

tuned signature;

tuned;

simplified;

publish output more thoroughly;

potentially redundant pending_output, for the sake of uniformity and reactivity;

tuned;

tuned;

more robust treatment of pending input/output: these are often correlated;
no decorations for invisible node;

clarified pretty margin;

publish decorations like diagnostics;
Markup.BAD is decoration, not error message;

support for semantic completion;

clarified text output wrt. symbols;

tuned;

clarified modules;
tuned;

tuned signature;

tuned signature;

tuned;

support for bibtex entries;

more explocit Document_Model.Content;

tuned signature;

clarified lazy text content;

tuned;

tuned signature;

more robust treatment of logical lines;

manage document blobs as well;

tuned;

proper registration of implicitly loaded files;

tuned;

clarified Document.Node.Name (again): canonical platform file;
identify document models by native java.io.File;

clarified file URIs;

clarified file URLs, notably for Windows UNC paths;

clarified master_dir: file-URL;

proper bootstrap name, e.g. for Pure.thy;

just one synchronized access to global state: works recursively on JVM;
tuned;

clarified file URI operations;

automatically resolve dependencies from document models and file-system;

clarified;

tuned signature;

proper state update;

tuned;

tuned signature;

proper import_name;

manage changes of external files;
tuned;

more explicit edits -- eliminated Clear;

tuned;

clarified Document_Model perspective and edits;

tuned;

re-use options from resources;

moved main state to VSCode_Resources;
misc tuning;

clarified node_name: preserve original uri;

clarified module name;

--HG--
rename : src/Tools/VSCode/src/uri_resources.scala => src/Tools/VSCode/src/vscode_resources.scala