2014-01-25 wenzelm 2014-01-25 propagate update of outer syntax keywords: global propertiesChanged, buffer TokenMarker.markTokens, text area repainting;
2013-11-19 wenzelm 2013-11-19 clarified Document.Blobs environment vs. actual edits of auxiliary files; more robust handling of vacuous edits;
2013-11-19 wenzelm 2013-11-19 maintain blobs within document state: digest + text in ML, digest-only in Scala; resolve files for command span, based on defined blobs; tuned;
2013-11-19 wenzelm 2013-11-19 proper Thy_Load.append of auxiliary file names; inlined errors;
2013-11-19 wenzelm 2013-11-19 clarified boundary cases of Document.Node.Name;
2013-11-18 wenzelm 2013-11-18 clarified Thy_Load.node_name;
2013-11-18 wenzelm 2013-11-18 inline blobs into command, via SHA1 digest; broadcast all blobs within edit, without storing the result;
2013-04-08 wenzelm 2013-04-08 more general Thy_Load.import_name, e.g. relevant for Isabelle/eclipse -- NB: Thy_Load serves as main hub for funny overriding to adapt to provers and editors;
2013-02-27 wenzelm 2013-02-27 discontinued obsolete 'uses' within theory header;
2012-12-30 wenzelm 2012-12-30 tuned;
2012-12-16 wenzelm 2012-12-16 tuned signature: use thy_load to adapt to prover/editor specific view on sources;
2012-12-07 wenzelm 2012-12-07 fork slow part of Thy_Load.body_files only;
2012-12-07 wenzelm 2012-12-07 explore theory_body_files via future, for improved performance; further internalization of header errors;
2012-11-30 wenzelm 2012-11-30 prefer Symbol.decode_strict in batch mode, to avoid files with spurious Unicode symbols that clash with Isabelle symbol interpretation;
2012-11-25 wenzelm 2012-11-25 tuned signature -- avoid intrusion of module Path in generic PIDE concepts;
2012-08-22 wenzelm 2012-08-22 add keywords of this node as well (e.g. relevant for Pure.thy);
2012-08-22 wenzelm 2012-08-22 find files via load commands within theory text; clarified Thy_Load.with_thy_text, simplified Thy_Load.check_thy;
2012-08-22 wenzelm 2012-08-22 pass syntax through check_thy;
2012-08-22 wenzelm 2012-08-22 use on explicit text only -- potentially via, not Scan.byte_reader; tuned signatures;
2012-08-21 wenzelm 2012-08-21 clarified initialization of Thy_Load, Thy_Info, Session;
2012-08-16 wenzelm 2012-08-16 more robust multi-platform support;
2012-08-07 wenzelm 2012-08-07 need to expand path in order to resolve imports like "~~/src/Tools/Code_Generator";
2012-08-07 wenzelm 2012-08-07 prefer static Build.session_content for loaded theories -- discontinued incremental protocol;
2012-08-07 wenzelm 2012-08-07 simplified Document.Node.Header -- internalized errors;
2012-07-24 wenzelm 2012-07-24 more explicit checks during parsing;
2012-07-22 wenzelm 2012-07-22 determine source dependencies, relatively to preloaded theories; tuned signature;
2012-07-20 wenzelm 2012-07-20 more explicit{File => JFile};
2012-03-15 wenzelm 2012-03-15 some support for outer syntax keyword declarations within theory header; more uniform Thy_Header.header as argument for begin_theory etc.;
2012-03-03 wenzelm 2012-03-03 retain original "uses" (again) -- still required for Thy_Load.use_file etc. in ML (notably for maintaining required/provided); tuned;
2012-03-01 wenzelm 2012-03-01 refined node_header -- more direct buffer access (again);
2012-02-29 wenzelm 2012-02-29 clarified module Thy_Load; more precise graph based on Document.Node.Deps with actual Node.Name dependencies;
2011-09-17 wenzelm 2011-09-17 sane default for class Thy_Load;
2011-09-01 wenzelm 2011-09-01 tuned signature;
2011-09-01 wenzelm 2011-09-01 more abstract Document.Node.Name; tuned signature;
2011-08-30 wenzelm 2011-08-30 separate module for jEdit primitives for loading theory files;
2011-08-29 wenzelm 2011-08-29 actual auto loading of required files; eliminated File_Store in favour of Thy_Load; tuned;
2011-08-12 wenzelm 2011-08-12 simplified class Thy_Header;
2011-07-05 wenzelm 2011-07-05 Thy_Info.dependencies: ignore already loaded theories, according to initial prover session status;
2011-07-04 wenzelm 2011-07-04 some support for theory files within Isabelle/Scala session;