src/Pure/Thy/thy_info.scala
2014-04-25 wenzelm 2014-04-25 unused;
2014-04-03 wenzelm 2014-04-03 more abstract Prover.Syntax, as proposed by Carst Tankink;
2014-04-03 wenzelm 2014-04-03 tuned signature (see also 0850d43cb355);
2014-03-18 wenzelm 2014-03-18 clarifed module name;
2014-02-14 wenzelm 2014-02-14 more integrity checks of theory names vs. full node names;
2013-12-12 wenzelm 2013-12-12 tuned message;
2013-11-21 wenzelm 2013-11-21 actually expose errors of cumulative theory dependencies; more informative error messages;
2013-11-19 wenzelm 2013-11-19 clarified boundary cases of Document.Node.Name;
2013-02-27 wenzelm 2013-02-27 parallel dep.load_files saves approx. 1s on 4 cores;
2013-02-27 wenzelm 2013-02-27 discontinued obsolete header "files" -- these are loaded explicitly after exploring dependencies;
2013-02-27 wenzelm 2013-02-27 discontinued obsolete 'uses' within theory header;
2012-12-07 wenzelm 2012-12-07 deactivate actual fork -- unstable in scala-2.9.2 on multicore hardware;
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-09-03 wenzelm 2012-09-03 bypass slow check for inlined files, where it is not really required;
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-21 wenzelm 2012-08-21 more direct cumulation of (sparse) keywords; discontinued slightly odd patching of Pure keywords; tuned signature;
2012-08-21 wenzelm 2012-08-21 some support for thy_load_commands; clarified signatures;
2012-08-21 wenzelm 2012-08-21 tuned signature;
2012-08-21 wenzelm 2012-08-21 clarified initialization of Thy_Load, Thy_Info, Session;
2012-08-07 wenzelm 2012-08-07 simplified Document.Node.Header -- internalized errors;
2012-02-29 wenzelm 2012-02-29 clarified module Thy_Load; more precise graph based on Document.Node.Deps with actual Node.Name dependencies;
2012-01-05 wenzelm 2012-01-05 prefer raw_message for protocol implementation; tuned;
2011-11-28 wenzelm 2011-11-28 separate module for concrete Isabelle markup;
2011-09-17 wenzelm 2011-09-17 more careful traversal of theory dependencies to retain standard import order;
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-29 wenzelm 2011-08-29 actual auto loading of required files; eliminated File_Store in favour of Thy_Load; tuned;
2011-08-16 wenzelm 2011-08-16 more robust Thy_Header.base_name, with minimal assumptions about path syntax; Isabelle.buffer_path: keep platform syntax;
2011-08-16 wenzelm 2011-08-16 use full .thy file name as node name, which makes MiscUtilities.resolveSymlinks/File.getCanonicalPath more predictable; more robust treatment of node dependencies; misc tuning;
2011-08-12 wenzelm 2011-08-12 simplified class Thy_Header;
2011-07-05 wenzelm 2011-07-05 tuned comment (cf. e9f26e66692d);
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 pervasive Basic_Library in Scala; tuned;
2011-07-04 wenzelm 2011-07-04 some support for theory files within Isabelle/Scala session;