src/Pure/Thy/thy_info.scala
19 months ago wenzelm 2017-10-07 clarified empty merge; tuned;
19 months ago wenzelm 2017-10-07 permissive loaded_theories (amending 67dbf5cdc056): user errors are produced e.g. in Known.make;
20 months ago wenzelm 2017-10-01 cache sources: invoke SHA1.digest at most once; maintain imported_sources, as required for new theories;
20 months ago wenzelm 2017-09-29 clarified theory syntax vs. overall session syntax;
20 months ago wenzelm 2017-09-29 more informative loaded_theories: dependencies and syntax;
20 months ago wenzelm 2017-09-29 tuned;
20 months ago wenzelm 2017-09-29 tuned signature;
20 months ago wenzelm 2017-09-28 session-qualified theory names are mandatory;
20 months ago wenzelm 2017-09-28 discontinued extra checks (see ce676a750575 and 60c159d490a2) -- qualified theory names are meant to cover this;
20 months ago wenzelm 2017-09-27 maintain loaded_files for each theory;
20 months ago wenzelm 2017-09-27 prefer sequential file-system access, but parallel parse;
20 months ago wenzelm 2017-09-26 tuned;
2017-04-18 wenzelm 2017-04-18 clarified session graph: collapse theories from other sessions;
2017-04-12 wenzelm 2017-04-12 clarified loaded_theories: map to qualified theory name; proper theory_name for PIDE editors;
2017-04-08 wenzelm 2017-04-08 tuned signature;
2017-04-07 wenzelm 2017-04-07 more explicit lookup of loaded_theories: base names allowed here; no base names for known_theories;
2017-04-06 wenzelm 2017-04-06 clarified fall-back name;
2017-04-06 wenzelm 2017-04-06 tuned whitespace;
2017-04-06 wenzelm 2017-04-06 clarified modules;
2017-04-06 wenzelm 2017-04-06 clarified checks -- avoid duplicated messages (amending 60c159d490a2);
2017-04-03 wenzelm 2017-04-03 tuned signature;
2017-04-03 wenzelm 2017-04-03 provide session qualifier via resources;
2017-04-03 wenzelm 2017-04-03 tuned signature;
2017-01-09 wenzelm 2017-01-09 tuned signature;
2016-08-02 wenzelm 2016-08-02 tuned signature -- prover-independence is presently theoretical;
2016-08-02 wenzelm 2016-08-02 support 'abbrevs' within theory header; simplified 'keywords': no abbreviations here;
2016-04-05 wenzelm 2016-04-05 tuned output;
2015-11-02 wenzelm 2015-11-02 more accurate imports: allow re-uses of base names in PIDE interaction (amending 60c159d490a2);
2015-04-15 wenzelm 2015-04-15 tuned signature, clarified modules;
2015-03-15 wenzelm 2015-03-15 clarified span position;
2015-03-14 wenzelm 2015-03-14 clarified positions of theory imports;
2015-01-25 wenzelm 2015-01-25 support for session graph from Scala side;
2014-12-11 wenzelm 2014-12-11 added Par_List in Scala, in accordance to ML version; system property "isabelle.threads" determines size of Scala thread pool, like system option "threads" for ML; avoid ".par" framework with its hard-wired thread pool, which also has problems with cancellation; tuned;
2014-05-02 wenzelm 2014-05-02 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;
2014-04-30 wenzelm 2014-04-30 some support for session-qualified theories: allow to refer to resources via qualified name instead of odd file-system path;
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;