src/Pure/Thy/thy_info.ML
Mon, 10 Apr 2017 11:52:21 +0200 wenzelm clarified, according to Scala version;
Mon, 10 Apr 2017 11:29:47 +0200 wenzelm clarified signature;
Sat, 08 Apr 2017 22:36:32 +0200 wenzelm more qualifier treatment, but in the end it is still ignored;
Sat, 08 Apr 2017 21:35:04 +0200 wenzelm tuned signature;
Sat, 08 Apr 2017 21:28:19 +0200 wenzelm provide Resources.import_name in ML, similar to Scala version;
Mon, 27 Feb 2017 16:29:52 +0100 wenzelm absent timing information means zero, according to 0070053570c4, f235646b1b73;
Fri, 16 Dec 2016 19:07:16 +0100 wenzelm consolidate nested thms with persistent result, for improved performance;
Sun, 10 Apr 2016 20:15:39 +0200 wenzelm tuned;
Sat, 09 Apr 2016 14:00:23 +0200 wenzelm clarified bootstrap;
Wed, 06 Apr 2016 17:16:30 +0200 wenzelm tuned signature;
Tue, 05 Apr 2016 20:03:24 +0200 wenzelm clarified modules -- simplified bootstrap;
Mon, 04 Apr 2016 16:14:22 +0200 wenzelm clarified bootstrap;
Sat, 10 Oct 2015 16:21:34 +0200 wenzelm more explicit HTML.symbols;
Wed, 19 Aug 2015 16:21:10 +0200 wenzelm avoid ambiguities on native Windows, such as / vs. /cygdrive/c/cygwin;
Sat, 15 Aug 2015 19:42:35 +0200 wenzelm clarified context;
Wed, 14 Jan 2015 16:27:19 +0100 wenzelm clarified build_theories: proper protocol handler;
Wed, 14 Jan 2015 14:28:52 +0100 wenzelm clarified build_theories;
Tue, 13 Jan 2015 21:46:09 +0100 wenzelm some support for PIDE batch session;
Mon, 22 Dec 2014 20:40:37 +0100 wenzelm discontinued central critical sections: NAMED_CRITICAL / CRITICAL;
Mon, 22 Dec 2014 18:10:54 +0100 wenzelm proper Synchronized.var;
Mon, 22 Dec 2014 17:17:00 +0100 wenzelm removed remains from Proof General;
Fri, 07 Nov 2014 16:36:55 +0100 wenzelm plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
Fri, 31 Oct 2014 22:37:22 +0100 wenzelm provide explicit theory (amending 621c052789b4);
Fri, 31 Oct 2014 21:35:11 +0100 wenzelm obsolete;
Fri, 31 Oct 2014 21:20:06 +0100 wenzelm obsolete;
Fri, 31 Oct 2014 11:36:41 +0100 wenzelm discontinued obsolete Output.urgent_message;
Tue, 12 Aug 2014 20:18:27 +0200 wenzelm tuned signature according to Scala version -- prefer explicit argument;
Wed, 23 Jul 2014 21:02:45 +0200 wenzelm more official Thy_Info.script_thy;
Mon, 31 Mar 2014 10:28:08 +0200 wenzelm 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;
Tue, 18 Mar 2014 17:39:03 +0100 wenzelm clarifed module name;
Fri, 28 Feb 2014 11:13:25 +0100 wenzelm tuned errors -- in accordance to Scala version;
Fri, 14 Feb 2014 14:39:44 +0100 wenzelm more integrity checks of theory names vs. full node names;
Thu, 13 Feb 2014 22:35:38 +0100 wenzelm 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);
Thu, 12 Dec 2013 13:23:23 +0100 wenzelm tuned message;
Fri, 22 Nov 2013 20:36:57 +0100 wenzelm tuned messages;
Sat, 16 Nov 2013 22:17:45 +0100 wenzelm prefer explicit "document" flag -- eliminated stateful Present.no_document;
Sat, 16 Nov 2013 13:12:02 +0100 wenzelm tuned signature;
Wed, 06 Nov 2013 20:58:11 +0100 wenzelm join all theory body forks, notably Toplevel.atom_result (diagnostic commands), before peeking at full status;
Tue, 03 Sep 2013 11:29:01 +0200 wenzelm Execution.fork formally requires registered Execution.running;
Sun, 25 Aug 2013 20:32:26 +0200 wenzelm maintain goal forks as part of global execution;
Sun, 25 Aug 2013 17:04:22 +0200 wenzelm simplified Goal.forked_proofs: status is determined via group instead of dummy future (see also Pure/PIDE/execution.ML);
Tue, 09 Apr 2013 15:59:02 +0200 wenzelm clarified protocol_message undefinedness;
Wed, 13 Mar 2013 21:25:08 +0100 wenzelm clarified parallel_subproofs_saturation (blind guess) vs. parallel_subproofs_threshold (precient timing estimate);
Mon, 04 Mar 2013 11:36:16 +0100 wenzelm join all proofs before scheduling present phase (ordered according to weight);
Mon, 04 Mar 2013 10:02:58 +0100 wenzelm more explicit datatype result;
Wed, 27 Feb 2013 16:27:44 +0100 wenzelm discontinued obsolete header "files" -- these are loaded explicitly after exploring dependencies;
Wed, 27 Feb 2013 12:45:19 +0100 wenzelm discontinued obsolete 'uses' within theory header;
Tue, 26 Feb 2013 19:44:26 +0100 wenzelm fork diagnostic commands (theory loader and PIDE interaction);
Wed, 20 Feb 2013 15:22:22 +0100 wenzelm more tight representation of command timing;
Tue, 19 Feb 2013 12:58:32 +0100 wenzelm support for prescient timing information within command transactions;
Sun, 13 Jan 2013 19:45:32 +0100 wenzelm more sensible order of theory nodes (correspondance to Scala version), e.g. relevant to theory progress;
Sat, 12 Jan 2013 15:00:48 +0100 wenzelm immediate theory progress for build_dialog;
Thu, 30 Aug 2012 19:18:49 +0200 wenzelm some support for registering forked proofs within Proof.state, using its bottom context;
Thu, 30 Aug 2012 16:39:50 +0200 wenzelm tuned signature;
Wed, 29 Aug 2012 11:48:45 +0200 wenzelm renamed Position.str_of to Position.here;
Sun, 26 Aug 2012 22:10:27 +0200 wenzelm more accurate defining position of theory;
Sun, 26 Aug 2012 21:46:50 +0200 wenzelm theory def/ref position reports, which enable hyperlinks etc.;
Thu, 23 Aug 2012 12:33:42 +0200 wenzelm simplified Thy_Load.check_thy (again) -- no need to pass keywords nor find files in body text;
Wed, 22 Aug 2012 21:28:33 +0200 wenzelm tuned;
Wed, 22 Aug 2012 21:02:02 +0200 wenzelm discontinued separate list of required files -- maintain only provided files as they occur at runtime;
less more (0) -100 -60 tip