src/Pure/Thy/thy_info.ML
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;
2013-01-13 wenzelm 2013-01-13 more sensible order of theory nodes (correspondance to Scala version), e.g. relevant to theory progress;
2013-01-12 wenzelm 2013-01-12 immediate theory progress for build_dialog; more formal Bash_Result -- accumulate output as lines;
2012-08-30 wenzelm 2012-08-30 some support for registering forked proofs within Proof.state, using its bottom context; tuned signature;
2012-08-30 wenzelm 2012-08-30 tuned signature;
2012-08-29 wenzelm 2012-08-29 renamed Position.str_of to Position.here;
2012-08-26 wenzelm 2012-08-26 more accurate defining position of theory;
2012-08-26 wenzelm 2012-08-26 theory def/ref position reports, which enable hyperlinks etc.; more official header command parsing;
2012-08-23 wenzelm 2012-08-23 simplified Thy_Load.check_thy (again) -- no need to pass keywords nor find files in body text;
2012-08-22 wenzelm 2012-08-22 tuned;
2012-08-22 wenzelm 2012-08-22 discontinued separate list of required files -- maintain only provided files as they occur at runtime; tuned signature;
2012-08-21 wenzelm 2012-08-21 more standard Thy_Load.check_thy for Pure.thy, relying on its header; pass uses and keywords from Thy_Load.check_thy to Thy_Info.load_thy; clarified 'ML_file' wrt. Thy_Load.require/provide, which is also relevant for Thy_Load.all_current;
2012-08-21 wenzelm 2012-08-21 refined Thy_Load.check_thy: find more uses in body text, based on keywords; refined Thy_Info.require_thy(s): cumulate additional keywords; slightly more value-oriented type Keywords.keywords;
2012-08-07 wenzelm 2012-08-07 prefer static Build.session_content for loaded theories -- discontinued incremental protocol;
2012-08-01 wenzelm 2012-08-01 more standard bootstrapping of Pure.thy;
2012-03-16 wenzelm 2012-03-16 define keywords early when processing the theory header, before running the body commands;
2012-03-15 wenzelm 2012-03-15 some support for outer syntax keyword declarations within theory header; more uniform Thy_Header.header as argument for begin_theory etc.;
2012-03-03 wenzelm 2012-03-03 clarified terminology of raw protocol messages;
2012-02-25 wenzelm 2012-02-25 discontinued slightly odd Graph.del_nodes (inefficient due to full Table.map);
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-08-20 wenzelm 2011-08-20 clarified get_imports -- should not rely on accidental order within graph;
2011-08-19 wenzelm 2011-08-19 tuned;
2011-08-17 wenzelm 2011-08-17 more systematic handling of parallel exceptions; distinguish exception concatanation EXCEPTIONS from parallel Par_Exn;
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;