src/Pure/Thy/thy_info.ML
2 months ago ago clarified signature;
2 months ago ago clarified Toplevel.state: more explicit types;
2 months ago ago tuned signature;
3 months ago ago clarified signature: Path.T as in Generated_Files;
8 months ago ago clarified modules;
10 months ago ago prefer explicit options;
11 months ago ago disable export_document by default (presently unused and for demo/testing purposes): avoid spurious IO exception in highly parallel environment;
12 months ago ago support for dynamic document output while editing;
12 months ago ago tuned signature (see Command.eval_state);
12 months ago ago export generated document.tex, unless explicit document=false;
12 months ago ago more general presentation hook, with document preparation as application;
12 months ago ago clarified signature: more explicit type "context" with full options;
12 months ago ago more explicit type Thy_Output.segment;
12 months ago ago support for general theory presentation;
12 months ago ago clarified future scheduling parameters, with support for parallel_limit;
16 months ago ago clarified implicit Pure.thy;
16 months ago ago formal check of @{cite} bibtex entries -- only in batch-mode session builds;
17 months ago ago positions as postlude: avoid intrusion of odd %-forms into main tex source;
17 months ago ago more explicit latex errors;
17 months ago ago removed somewhat pointless warning;
19 months ago ago provide theory timing information, similar to command timing but always considered relevant;
19 months ago ago discontinued extra checks (see ce676a750575 and 60c159d490a2) -- qualified theory names are meant to cover this;
21 months ago ago tuned;
21 months ago ago more thorough Execution.join, under the assumption that nested Execution.fork only happens from given exed_ids;
21 months ago ago more synchronized Execution.snapshot;
21 months ago ago tuned;
2017-04-21 ago eliminated default_qualifier: just a constant;
2017-04-18 ago exclude theories from other sessions;
2017-04-10 ago clarified theory_long_name (for qualified access to Thy_Info) vs. short theory_name (which is unique within any given theory context);
2017-04-10 ago proper qualifier for imports;
2017-04-10 ago clarified, according to Scala version;
2017-04-10 ago clarified signature;
2017-04-08 ago more qualifier treatment, but in the end it is still ignored;
2017-04-08 ago tuned signature;
2017-04-08 ago provide Resources.import_name in ML, similar to Scala version;
2017-02-27 ago absent timing information means zero, according to 0070053570c4, f235646b1b73;
2016-12-16 ago consolidate nested thms with persistent result, for improved performance;
2016-04-10 ago tuned;
2016-04-09 ago clarified bootstrap;
2016-04-06 ago tuned signature;
2016-04-05 ago clarified modules -- simplified bootstrap;
2016-04-04 ago clarified bootstrap;
2015-10-10 ago more explicit HTML.symbols;
2015-08-19 ago avoid ambiguities on native Windows, such as / vs. /cygdrive/c/cygwin;
2015-08-15 ago clarified context;
2015-01-14 ago clarified build_theories: proper protocol handler;
2015-01-14 ago clarified build_theories;
2015-01-13 ago some support for PIDE batch session;
2014-12-22 ago discontinued central critical sections: NAMED_CRITICAL / CRITICAL;
2014-12-22 ago proper Synchronized.var;
2014-12-22 ago removed remains from Proof General;
2014-11-07 ago plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
2014-10-31 ago provide explicit theory (amending 621c052789b4);
2014-10-31 ago obsolete;
2014-10-31 ago obsolete;
2014-10-31 ago discontinued obsolete Output.urgent_message;
2014-08-12 ago tuned signature according to Scala version -- prefer explicit argument;
2014-07-23 ago more official Thy_Info.script_thy;
2014-03-31 ago support bulk messages consisting of small string segments, which are more healthy to the Poly/ML RTS and might prevent spurious GC crashes such as MTGCProcessMarkPointers::ScanAddressesInObject;
2014-03-18 ago clarifed module name;