src/Pure/Thy/thy_info.ML
20 months ago wenzelm 2017-10-16 provide theory timing information, similar to command timing but always considered relevant;
21 months ago wenzelm 2017-09-28 discontinued extra checks (see ce676a750575 and 60c159d490a2) -- qualified theory names are meant to cover this;
22 months ago wenzelm 2017-08-08 tuned;
22 months ago wenzelm 2017-08-07 more thorough Execution.join, under the assumption that nested Execution.fork only happens from given exed_ids;
22 months ago wenzelm 2017-08-07 more synchronized Execution.snapshot;
22 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;
2013-11-06 wenzelm 2013-11-06 join all theory body forks, notably Toplevel.atom_result (diagnostic commands), before peeking at full status;
2013-09-03 wenzelm 2013-09-03 Execution.fork formally requires registered Execution.running; Thy_Info.load_thy: more official exec_id registration (batch mode); dummy exec Document_ID.none is always registered (TTY mode); clarified exceptions for module Execution (NB: fork is used in user space, unlike protocol operations of Command and Document);
2013-08-25 wenzelm 2013-08-25 maintain goal forks as part of global execution; tuned;
2013-08-25 wenzelm 2013-08-25 simplified Goal.forked_proofs: status is determined via group instead of dummy future (see also Pure/PIDE/execution.ML); clarified Task_Queue.group_status; tuned;
2013-04-09 wenzelm 2013-04-09 clarified protocol_message undefinedness;
2013-03-13 wenzelm 2013-03-13 clarified parallel_subproofs_saturation (blind guess) vs. parallel_subproofs_threshold (precient timing estimate); clarified unknown timing vs. zero timing; tuned;
2013-03-04 wenzelm 2013-03-04 join all proofs before scheduling present phase (ordered according to weight); tuned;
2013-03-04 wenzelm 2013-03-04 more explicit datatype result;
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;
2013-02-26 wenzelm 2013-02-26 fork diagnostic commands (theory loader and PIDE interaction); explicit id for load_thy, for more robust Goal.fork accounting and commit for each theory -- NB: use_thys nodes become subject to Position.is_reported like PIDE document transactions; clarified Toplevel.command_exception vs. Toplevel.command_errors;
2013-02-20 wenzelm 2013-02-20 more tight representation of command timing; tuned signatures; tuned;
2013-02-19 wenzelm 2013-02-19 support for prescient timing information within command transactions;