src/Pure/Thy/thy_info.ML
14 months ago wenzelm 2018-05-14 support for dynamic document output while editing;
14 months ago wenzelm 2018-05-14 tuned signature (see Command.eval_state);
14 months ago wenzelm 2018-05-14 export generated document.tex, unless explicit document=false;
14 months ago wenzelm 2018-05-14 more general presentation hook, with document preparation as application;
14 months ago wenzelm 2018-05-14 clarified signature: more explicit type "context" with full options;
14 months ago wenzelm 2018-05-14 more explicit type Thy_Output.segment;
14 months ago wenzelm 2018-05-11 support for general theory presentation;
14 months ago wenzelm 2018-05-09 clarified future scheduling parameters, with support for parallel_limit;
18 months ago wenzelm 2018-01-08 clarified implicit Pure.thy;
19 months ago wenzelm 2017-12-29 formal check of @{cite} bibtex entries -- only in batch-mode session builds;
19 months ago wenzelm 2017-12-13 positions as postlude: avoid intrusion of odd %-forms into main tex source;
19 months ago wenzelm 2017-12-10 more explicit latex errors;
19 months ago wenzelm 2017-12-08 removed somewhat pointless warning;
21 months ago wenzelm 2017-10-16 provide theory timing information, similar to command timing but always considered relevant;
22 months ago wenzelm 2017-09-28 discontinued extra checks (see ce676a750575 and 60c159d490a2) -- qualified theory names are meant to cover this;
23 months ago wenzelm 2017-08-08 tuned;
23 months ago wenzelm 2017-08-07 more thorough Execution.join, under the assumption that nested Execution.fork only happens from given exed_ids;
23 months ago wenzelm 2017-08-07 more synchronized Execution.snapshot;
23 months ago wenzelm 2017-08-07 tuned;
2017-04-21 wenzelm 2017-04-21 eliminated default_qualifier: just a constant;
2017-04-18 wenzelm 2017-04-18 exclude theories from other sessions; clarified modules;
2017-04-10 wenzelm 2017-04-10 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 wenzelm 2017-04-10 proper qualifier for imports;
2017-04-10 wenzelm 2017-04-10 clarified, according to Scala version;
2017-04-10 wenzelm 2017-04-10 clarified signature;
2017-04-08 wenzelm 2017-04-08 more qualifier treatment, but in the end it is still ignored;
2017-04-08 wenzelm 2017-04-08 tuned signature;
2017-04-08 wenzelm 2017-04-08 provide Resources.import_name in ML, similar to Scala version; reset default_qualifier for now; tuned;
2017-02-27 wenzelm 2017-02-27 absent timing information means zero, according to 0070053570c4, f235646b1b73;
2016-12-16 wenzelm 2016-12-16 consolidate nested thms with persistent result, for improved performance; always consolidate parts of fulfill_norm_proof: important to exhibit cyclic thms (via non-termination as officially published), but this was lost in f33d5a00c25d;
2016-04-10 wenzelm 2016-04-10 tuned;
2016-04-09 wenzelm 2016-04-09 clarified bootstrap;
2016-04-06 wenzelm 2016-04-06 tuned signature;
2016-04-05 wenzelm 2016-04-05 clarified modules -- simplified bootstrap;
2016-04-04 wenzelm 2016-04-04 clarified bootstrap;
2015-10-10 wenzelm 2015-10-10 more explicit HTML.symbols; tuned signature;
2015-08-19 wenzelm 2015-08-19 avoid ambiguities on native Windows, such as / vs. /cygdrive/c/cygwin;
2015-08-15 wenzelm 2015-08-15 clarified context;
2015-01-14 wenzelm 2015-01-14 clarified build_theories: proper protocol handler;
2015-01-14 wenzelm 2015-01-14 clarified build_theories;
2015-01-13 wenzelm 2015-01-13 some support for PIDE batch session; clarified Thy_Info.use_thys_options and corresponding protocol command;
2014-12-22 wenzelm 2014-12-22 discontinued central critical sections: NAMED_CRITICAL / CRITICAL;
2014-12-22 wenzelm 2014-12-22 proper Synchronized.var; more atomic operations;
2014-12-22 wenzelm 2014-12-22 removed remains from Proof General;
2014-11-07 wenzelm 2014-11-07 plain value Keywords.keywords, which might be used outside theory for bootstrap purposes; plain value Outer_Syntax within theory: parsing requires current theory context; clarified name of Keyword.is_literal according to its semantics; eliminated pointless type Keyword.T; simplified @{command_spec}; clarified bootstrap keywords and syntax: take it as basis instead of side-branch;
2014-10-31 wenzelm 2014-10-31 provide explicit theory (amending 621c052789b4);
2014-10-31 wenzelm 2014-10-31 obsolete;
2014-10-31 wenzelm 2014-10-31 obsolete;
2014-10-31 wenzelm 2014-10-31 discontinued obsolete Output.urgent_message;
2014-08-12 wenzelm 2014-08-12 tuned signature according to Scala version -- prefer explicit argument;
2014-07-23 wenzelm 2014-07-23 more official Thy_Info.script_thy;
2014-03-31 wenzelm 2014-03-31 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 wenzelm 2014-03-18 clarifed module name;
2014-02-28 wenzelm 2014-02-28 tuned errors -- in accordance to Scala version;
2014-02-14 wenzelm 2014-02-14 more integrity checks of theory names vs. full node names;
2014-02-13 wenzelm 2014-02-13 more integrity checks of theory names vs. full node names -- at least for the scope of a single use_thys (or "theories" section in ROOT);
2013-12-12 wenzelm 2013-12-12 tuned message;
2013-11-22 wenzelm 2013-11-22 tuned messages;
2013-11-16 wenzelm 2013-11-16 prefer explicit "document" flag -- eliminated stateful Present.no_document;
2013-11-16 wenzelm 2013-11-16 tuned signature;