| Wed, 25 Nov 2020 17:49:09 +0100 |
wenzelm |
more robust: include reports from Thy_Output.present_thy/output_document;
|
file |
diff |
annotate
|
| Wed, 25 Nov 2020 13:30:06 +0100 |
wenzelm |
unused;
|
file |
diff |
annotate
|
| Mon, 23 Nov 2020 15:14:58 +0100 |
wenzelm |
support for PIDE markup in batch build (inactive due to pide_reports=false);
|
file |
diff |
annotate
|
| Fri, 20 Nov 2020 23:47:34 +0100 |
wenzelm |
generate theory HTML in Isabelle/Scala;
|
file |
diff |
annotate
|
| Wed, 18 Nov 2020 15:47:53 +0100 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Tue, 17 Nov 2020 22:57:56 +0100 |
wenzelm |
refer to command_timings/last_timing via resources;
|
file |
diff |
annotate
|
| Mon, 16 Nov 2020 22:46:02 +0100 |
wenzelm |
clarified signature: master_dir is just Path.current;
|
file |
diff |
annotate
|
| Mon, 16 Nov 2020 22:23:04 +0100 |
wenzelm |
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
|
file |
diff |
annotate
|
| Mon, 16 Nov 2020 13:11:15 +0100 |
wenzelm |
refer to HTML symbols via resources;
|
file |
diff |
annotate
|
| Sun, 15 Nov 2020 17:34:19 +0100 |
wenzelm |
clarified bibtex_entries: refer to overall session structure;
|
file |
diff |
annotate
|
| Sat, 14 Nov 2020 17:29:37 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Wed, 11 Nov 2020 21:00:14 +0100 |
wenzelm |
build documents in Isabelle/Scala, based on generated tex files as session exports;
|
file |
diff |
annotate
|
| Tue, 27 Oct 2020 22:34:37 +0100 |
wenzelm |
clarified signature: overloaded "+" for Path.append;
|
file |
diff |
annotate
|
| Sat, 26 Sep 2020 16:02:54 +0200 |
wenzelm |
clarified document export;
|
file |
diff |
annotate
|
| Tue, 01 Sep 2020 18:03:17 +0200 |
wenzelm |
discontinue export_document --- always enabled (reverting f0f83ce0badd);
|
file |
diff |
annotate
|
| Fri, 03 Apr 2020 13:51:56 +0200 |
wenzelm |
more accurate context position reports;
|
file |
diff |
annotate
|
| Fri, 06 Dec 2019 15:53:09 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Sat, 02 Nov 2019 12:02:27 +0100 |
wenzelm |
more scalable protocol_message: use XML.body directly (Output.output hook is not required);
|
file |
diff |
annotate
|
| Mon, 16 Sep 2019 15:30:38 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sat, 30 Mar 2019 20:54:47 +0100 |
wenzelm |
clarified signature: more explicit type Path.binding;
|
file |
diff |
annotate
|
| Sun, 10 Mar 2019 21:12:29 +0100 |
wenzelm |
document markers are formal comments, and may thus occur anywhere in the command-span;
|
file |
diff |
annotate
|
| Sat, 09 Mar 2019 23:57:07 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Sat, 09 Mar 2019 13:19:13 +0100 |
wenzelm |
clarified Toplevel.state: more explicit types;
|
file |
diff |
annotate
|
| Fri, 08 Mar 2019 19:22:28 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sat, 02 Feb 2019 15:52:14 +0100 |
wenzelm |
clarified signature: Path.T as in Generated_Files;
|
file |
diff |
annotate
|
| Wed, 29 Aug 2018 11:44:28 +0200 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Tue, 26 Jun 2018 14:39:49 +0200 |
wenzelm |
prefer explicit options;
|
file |
diff |
annotate
|
| Sun, 24 Jun 2018 22:13:23 +0200 |
wenzelm |
disable export_document by default (presently unused and for demo/testing purposes): avoid spurious IO exception in highly parallel environment;
|
file |
diff |
annotate
|
| Mon, 14 May 2018 22:22:47 +0200 |
wenzelm |
support for dynamic document output while editing;
|
file |
diff |
annotate
|
| Mon, 14 May 2018 16:00:10 +0200 |
wenzelm |
tuned signature (see Command.eval_state);
|
file |
diff |
annotate
|
| Mon, 14 May 2018 14:30:13 +0200 |
wenzelm |
export generated document.tex, unless explicit document=false;
|
file |
diff |
annotate
|
| Mon, 14 May 2018 11:29:22 +0200 |
wenzelm |
more general presentation hook, with document preparation as application;
|
file |
diff |
annotate
|
| Mon, 14 May 2018 10:58:14 +0200 |
wenzelm |
clarified signature: more explicit type "context" with full options;
|
file |
diff |
annotate
|
| Mon, 14 May 2018 10:22:45 +0200 |
wenzelm |
more explicit type Thy_Output.segment;
|
file |
diff |
annotate
|
| Fri, 11 May 2018 22:40:02 +0200 |
wenzelm |
support for general theory presentation;
|
file |
diff |
annotate
|
| Wed, 09 May 2018 20:45:57 +0200 |
wenzelm |
clarified future scheduling parameters, with support for parallel_limit;
|
file |
diff |
annotate
|
| Mon, 08 Jan 2018 22:36:02 +0100 |
wenzelm |
clarified implicit Pure.thy;
|
file |
diff |
annotate
|
| Fri, 29 Dec 2017 17:40:57 +0100 |
wenzelm |
formal check of @{cite} bibtex entries -- only in batch-mode session builds;
|
file |
diff |
annotate
|
| Wed, 13 Dec 2017 16:18:40 +0100 |
wenzelm |
positions as postlude: avoid intrusion of odd %-forms into main tex source;
|
file |
diff |
annotate
|
| Sun, 10 Dec 2017 14:29:14 +0100 |
wenzelm |
more explicit latex errors;
|
file |
diff |
annotate
|
| Fri, 08 Dec 2017 16:02:44 +0100 |
wenzelm |
removed somewhat pointless warning;
|
file |
diff |
annotate
|
| Mon, 16 Oct 2017 14:32:09 +0200 |
wenzelm |
provide theory timing information, similar to command timing but always considered relevant;
|
file |
diff |
annotate
|
| Thu, 28 Sep 2017 11:53:55 +0200 |
wenzelm |
discontinued extra checks (see ce676a750575 and 60c159d490a2) -- qualified theory names are meant to cover this;
|
file |
diff |
annotate
|
| Tue, 08 Aug 2017 11:49:35 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Mon, 07 Aug 2017 20:05:23 +0200 |
wenzelm |
more thorough Execution.join, under the assumption that nested Execution.fork only happens from given exed_ids;
|
file |
diff |
annotate
|
| Mon, 07 Aug 2017 15:13:21 +0200 |
wenzelm |
more synchronized Execution.snapshot;
|
file |
diff |
annotate
|
| Mon, 07 Aug 2017 11:34:32 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 21 Apr 2017 14:09:03 +0200 |
wenzelm |
eliminated default_qualifier: just a constant;
|
file |
diff |
annotate
|
| Tue, 18 Apr 2017 16:34:58 +0200 |
wenzelm |
exclude theories from other sessions;
|
file |
diff |
annotate
|
| 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
|
| Wed, 22 Aug 2012 21:28:33 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 22 Aug 2012 21:02:02 +0200 |
wenzelm |
discontinued separate list of required files -- maintain only provided files as they occur at runtime;
|
file |
diff |
annotate
|
| Tue, 21 Aug 2012 21:48:32 +0200 |
wenzelm |
more standard Thy_Load.check_thy for Pure.thy, relying on its header;
|
file |
diff |
annotate
|
| Tue, 21 Aug 2012 20:32:33 +0200 |
wenzelm |
refined Thy_Load.check_thy: find more uses in body text, based on keywords;
|
file |
diff |
annotate
|
| Tue, 07 Aug 2012 17:08:22 +0200 |
wenzelm |
prefer static Build.session_content for loaded theories -- discontinued incremental protocol;
|
file |
diff |
annotate
|
| Wed, 01 Aug 2012 19:53:20 +0200 |
wenzelm |
more standard bootstrapping of Pure.thy;
|
file |
diff |
annotate
|
| Fri, 16 Mar 2012 13:05:30 +0100 |
wenzelm |
define keywords early when processing the theory header, before running the body commands;
|
file |
diff |
annotate
|
| Thu, 15 Mar 2012 00:10:45 +0100 |
wenzelm |
some support for outer syntax keyword declarations within theory header;
|
file |
diff |
annotate
|
| Sat, 03 Mar 2012 18:18:39 +0100 |
wenzelm |
clarified terminology of raw protocol messages;
|
file |
diff |
annotate
|
| Sat, 25 Feb 2012 12:34:56 +0100 |
wenzelm |
discontinued slightly odd Graph.del_nodes (inefficient due to full Table.map);
|
file |
diff |
annotate
|
| Thu, 05 Jan 2012 14:34:18 +0100 |
wenzelm |
prefer raw_message for protocol implementation;
|
file |
diff |
annotate
|