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