Thu, 12 Aug 2021 13:13:10 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
Tue, 08 Jun 2021 13:17:45 +0200 |
wenzelm |
more formal ML profiling messages;
|
file |
diff |
annotate
|
Mon, 07 Jun 2021 16:40:26 +0200 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
Fri, 21 May 2021 12:29:29 +0200 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
Sun, 02 May 2021 14:07:19 +0200 |
wenzelm |
early definition of ML antiquotations;
|
file |
diff |
annotate
|
Fri, 16 Apr 2021 23:35:20 +0200 |
wenzelm |
clarified conditional ML;
|
file |
diff |
annotate
|
Sun, 11 Apr 2021 21:32:09 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Wed, 31 Mar 2021 22:58:17 +0200 |
wenzelm |
further clarification of Isabelle distribution identification -- avoid odd patching of sources;
|
file |
diff |
annotate
|
Tue, 23 Mar 2021 19:47:15 +0100 |
wenzelm |
enforce full build;
|
file |
diff |
annotate
|
Sun, 21 Mar 2021 23:16:34 +0100 |
wenzelm |
enforce full build;
|
file |
diff |
annotate
|
Fri, 05 Mar 2021 16:09:42 +0100 |
wenzelm |
clarified signature --- augment existing structure Time;
|
file |
diff |
annotate
|
Thu, 04 Mar 2021 22:03:33 +0100 |
wenzelm |
enforce full build, after significant changes in Isabelle/Scala;
|
file |
diff |
annotate
|
Mon, 22 Feb 2021 14:48:03 +0100 |
wenzelm |
clarified signature, following Isabelle/Scala;
|
file |
diff |
annotate
|
Sun, 21 Feb 2021 00:49:09 +0100 |
wenzelm |
clarified lines (again);
|
file |
diff |
annotate
|
Sat, 20 Feb 2021 23:01:35 +0100 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
Sat, 20 Feb 2021 22:09:16 +0100 |
wenzelm |
more uniform Bash.process: always ask Isabelle/Scala;
|
file |
diff |
annotate
|
Sun, 07 Feb 2021 15:32:57 +0100 |
wenzelm |
clarified modules: less redundancy;
|
file |
diff |
annotate
|
Sun, 07 Feb 2021 12:55:41 +0100 |
wenzelm |
clarified modules: allow early invocation of Scala functions;
|
file |
diff |
annotate
|
Sun, 07 Feb 2021 12:30:52 +0100 |
wenzelm |
clarified modules: allow early definition of protocol commands;
|
file |
diff |
annotate
|
Sat, 16 Jan 2021 22:52:43 +0100 |
wenzelm |
updated to scala-2.13.4;
|
file |
diff |
annotate
|
Sun, 20 Dec 2020 15:47:54 +0100 |
wenzelm |
present auxiliary files with PIDE markup;
|
file |
diff |
annotate
|
Sat, 28 Nov 2020 21:56:24 +0100 |
wenzelm |
added document antiquotation @{tool};
|
file |
diff |
annotate
|
Sat, 28 Nov 2020 17:38:03 +0100 |
wenzelm |
clarified protocol: Doc.check at run-time via Scala function;
|
file |
diff |
annotate
|
Tue, 24 Nov 2020 16:39:58 +0100 |
wenzelm |
clarified signature and database layout;
|
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
|
Sun, 01 Nov 2020 16:54:49 +0100 |
haftmann |
bundle mixins for locale and class specifications
|
file |
diff |
annotate
|
Mon, 12 Oct 2020 07:25:38 +0000 |
haftmann |
dedicated module for toplevel target handling
|
file |
diff |
annotate
|
Thu, 16 Jul 2020 22:24:03 +0200 |
wenzelm |
support native PID for ML process;
|
file |
diff |
annotate
|
Mon, 13 Jul 2020 22:07:18 +0200 |
wenzelm |
clarified modules: ML_Statistics within bootstrap environment;
|
file |
diff |
annotate
|
Mon, 25 May 2020 20:43:19 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
Sun, 24 May 2020 19:45:42 +0200 |
wenzelm |
proper check of registered Scala functions;
|
file |
diff |
annotate
|
Wed, 20 May 2020 20:45:43 +0200 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
Sun, 05 Apr 2020 13:05:40 +0200 |
wenzelm |
clarified names;
|
file |
diff |
annotate
|
Fri, 03 Apr 2020 20:49:49 +0200 |
wenzelm |
tuned -- prefer Config.T over Data;
|
file |
diff |
annotate
|
Fri, 03 Apr 2020 17:35:10 +0200 |
wenzelm |
less redundant markup reports;
|
file |
diff |
annotate
|
Fri, 08 Nov 2019 19:06:50 +0100 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
Fri, 08 Nov 2019 16:11:09 +0100 |
wenzelm |
tuned modules;
|
file |
diff |
annotate
|
Sat, 19 Oct 2019 11:33:36 +0200 |
wenzelm |
proper protocol_message for bootstrap proofs;
|
file |
diff |
annotate
|
Thu, 17 Oct 2019 20:28:31 +0200 |
wenzelm |
clarified files;
|
file |
diff |
annotate
|
Fri, 04 Oct 2019 15:30:52 +0200 |
wenzelm |
Term_XML.Encode/Decode.term uses Const "typargs";
|
file |
diff |
annotate
|
Mon, 19 Aug 2019 19:12:44 +0200 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
Sat, 17 Aug 2019 11:13:16 +0200 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
Tue, 13 Aug 2019 15:34:46 +0200 |
wenzelm |
added SUBPROOFS / "subproofs" method combinator, for more compact proofterms;
|
file |
diff |
annotate
|
Tue, 13 Aug 2019 10:27:21 +0200 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
Tue, 30 Jul 2019 14:35:29 +0200 |
wenzelm |
clarified modules: provide reconstruct_proof / expand_proof at the bottom of proof term construction;
|
file |
diff |
annotate
|
Tue, 30 Jul 2019 11:41:39 +0200 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
Mon, 22 Jul 2019 16:15:40 +0200 |
wenzelm |
support export_proofs, prune_proofs;
|
file |
diff |
annotate
|
Tue, 16 Jul 2019 15:39:32 +0200 |
wenzelm |
support for a soft-type system within the Isabelle logical framework;
|
file |
diff |
annotate
|
Sun, 10 Mar 2019 00:21:34 +0100 |
wenzelm |
added semantic document markers;
|
file |
diff |
annotate
|
Fri, 08 Mar 2019 17:05:23 +0100 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
Tue, 11 Dec 2018 21:23:02 +0100 |
wenzelm |
more uniform multi-language operations;
|
file |
diff |
annotate
|
Tue, 11 Dec 2018 19:25:35 +0100 |
wenzelm |
more uniform multi-language operations;
|
file |
diff |
annotate
|
Mon, 10 Dec 2018 20:20:24 +0100 |
wenzelm |
clarified modules, following bytes.scala;
|
file |
diff |
annotate
|
Sat, 01 Dec 2018 16:11:59 +0100 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
Fri, 30 Nov 2018 23:43:10 +0100 |
wenzelm |
more general command 'generate_file' for registered file types, notably Haskell;
|
file |
diff |
annotate
|
Tue, 30 Oct 2018 19:18:01 +0100 |
wenzelm |
support for GHC: string literals;
|
file |
diff |
annotate
|
Tue, 30 Oct 2018 19:14:31 +0100 |
wenzelm |
some support for UTF-8 (similar to Isabelle/Scala version);
|
file |
diff |
annotate
|
Wed, 29 Aug 2018 11:44:28 +0200 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
Fri, 11 May 2018 22:59:00 +0200 |
wenzelm |
some export of foundational theory content;
|
file |
diff |
annotate
|
Sun, 06 May 2018 22:15:52 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Sat, 10 Feb 2018 11:55:12 +0100 |
wenzelm |
more accessible src/Pure/ROOT.ML;
|
file |
diff |
annotate
|
Sun, 14 Jan 2018 14:11:02 +0100 |
wenzelm |
clarified modules: uniform notion of formal comments;
|
file |
diff |
annotate
|
Tue, 09 Jan 2018 15:40:12 +0100 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
Sun, 24 Dec 2017 14:10:41 +0100 |
wenzelm |
check bibtex database on ML side -- for semantic PIDE editing;
|
file |
diff |
annotate
|
Sun, 24 Dec 2017 13:07:05 +0100 |
wenzelm |
clarified directories;
|
file |
diff |
annotate
|
Sat, 16 Dec 2017 16:46:01 +0100 |
wenzelm |
PIDE markup for session ROOT files;
|
file |
diff |
annotate
|
Thu, 14 Dec 2017 21:31:54 +0100 |
wenzelm |
clarified file name;
|
file |
diff |
annotate
|
Tue, 05 Dec 2017 15:29:37 +0100 |
wenzelm |
system option for default command tags;
|
file |
diff |
annotate
|
Tue, 18 Apr 2017 16:34:58 +0200 |
wenzelm |
exclude theories from other sessions;
|
file |
diff |
annotate
|
Tue, 18 Oct 2016 16:03:30 +0200 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
Wed, 21 Sep 2016 20:33:44 +0200 |
wenzelm |
more tight implementation of symbol explode operation (without support for raw symbols);
|
file |
diff |
annotate
|
Mon, 05 Sep 2016 23:11:00 +0200 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
Tue, 09 Aug 2016 14:41:27 +0200 |
wenzelm |
clarified bootstrap;
|
file |
diff |
annotate
|
Wed, 01 Jun 2016 16:02:02 +0200 |
wenzelm |
ML pp for Rat.rat;
|
file |
diff |
annotate
|
Tue, 31 May 2016 19:51:01 +0200 |
wenzelm |
rat.ML is now part of Pure to allow tigther integration with Isabelle/ML;
|
file |
diff |
annotate
|
Thu, 12 May 2016 22:06:18 +0200 |
wenzelm |
common entity definitions within a global or local theory context;
|
file |
diff |
annotate
|
Thu, 28 Apr 2016 09:43:11 +0200 |
wenzelm |
support 'assumes' in specifications, e.g. 'definition', 'inductive';
|
file |
diff |
annotate
|
Sun, 10 Apr 2016 21:30:48 +0200 |
wenzelm |
clarified files;
|
file |
diff |
annotate
|
Sat, 09 Apr 2016 20:31:46 +0200 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
Sat, 09 Apr 2016 16:16:05 +0200 |
wenzelm |
shared output primitives of physical/virtual Pure;
|
file |
diff |
annotate
|
Sat, 09 Apr 2016 14:00:23 +0200 |
wenzelm |
clarified bootstrap;
|
file |
diff |
annotate
|
Sat, 09 Apr 2016 11:21:38 +0200 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
Thu, 07 Apr 2016 22:09:23 +0200 |
wenzelm |
section headings for ROOT.ML;
|
file |
diff |
annotate
|
Thu, 07 Apr 2016 21:39:03 +0200 |
wenzelm |
back to dynamic conditional compilation (reverting 4764473c9b8d) via recursive ML name space;
|
file |
diff |
annotate
|
Thu, 07 Apr 2016 20:51:52 +0200 |
wenzelm |
clarified mode of ROOT.ML files;
|
file |
diff |
annotate
|
Thu, 07 Apr 2016 16:53:43 +0200 |
wenzelm |
more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use';
|
file |
diff |
annotate
|
Thu, 07 Apr 2016 11:17:57 +0200 |
wenzelm |
clarified editor mode;
|
file |
diff |
annotate
|
Wed, 06 Apr 2016 19:03:29 +0200 |
wenzelm |
virtual thread data via context, for proper support of Context.>> etc;
|
file |
diff |
annotate
|
Wed, 06 Apr 2016 16:51:52 +0200 |
wenzelm |
clarified bootstrap;
|
file |
diff |
annotate
|
Wed, 06 Apr 2016 16:33:33 +0200 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
Wed, 06 Apr 2016 11:37:37 +0200 |
wenzelm |
clarified ML bootstrap;
|
file |
diff |
annotate
|
Tue, 05 Apr 2016 21:51:14 +0200 |
wenzelm |
clarified files;
|
file |
diff |
annotate
|
Tue, 05 Apr 2016 21:23:32 +0200 |
wenzelm |
back to static conditional compilation -- simplified bootstrap;
|
file |
diff |
annotate
|
Tue, 05 Apr 2016 20:51:37 +0200 |
wenzelm |
clarified modules -- simplified bootstrap;
|
file |
diff |
annotate
|
Tue, 05 Apr 2016 18:25:42 +0200 |
wenzelm |
actually observe ML_system_unsafe, concerning the environment that is stored in theory ML_Root;
|
file |
diff |
annotate
|
Tue, 05 Apr 2016 17:25:11 +0200 |
wenzelm |
prefer antiquotations;
|
file |
diff |
annotate
|
Tue, 05 Apr 2016 17:16:46 +0200 |
wenzelm |
proper use_thy;
|
file |
diff |
annotate
|
Mon, 04 Apr 2016 23:58:48 +0200 |
wenzelm |
more uniform ML file commands;
|
file |
diff |
annotate
|
Mon, 04 Apr 2016 20:46:39 +0200 |
wenzelm |
clarified bootstrap -- avoid conditional compilation in ROOT.ML;
|
file |
diff |
annotate
|
Mon, 04 Apr 2016 20:28:17 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Mon, 04 Apr 2016 20:20:47 +0200 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
Mon, 04 Apr 2016 19:48:54 +0200 |
wenzelm |
clarified conditional compilation;
|
file |
diff |
annotate
|
Mon, 04 Apr 2016 17:25:53 +0200 |
wenzelm |
clarified bootstrap -- avoid 'ML_file' in Pure.thy for uniformity;
|
file |
diff |
annotate
|
Mon, 04 Apr 2016 17:02:34 +0200 |
wenzelm |
clarified bootstrap -- more uniform use of ML files;
|
file |
diff |
annotate
|
Mon, 04 Apr 2016 16:14:22 +0200 |
wenzelm |
clarified bootstrap;
|
file |
diff |
annotate
|
Mon, 04 Apr 2016 15:53:56 +0200 |
wenzelm |
clarified final setup of ML environment;
|
file |
diff |
annotate
|
Mon, 04 Apr 2016 15:35:24 +0200 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
Sat, 02 Apr 2016 23:14:08 +0200 |
wenzelm |
structure PolyML is sealed after bootstrap: all ML system access is managed by Isabelle;
|
file |
diff |
annotate
|
Sat, 02 Apr 2016 20:33:34 +0200 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
Sat, 02 Apr 2016 20:23:51 +0200 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
Sat, 26 Mar 2016 16:14:46 +0100 |
wenzelm |
explicit print_depth for the sake of Spec_Check.determine_type;
|
file |
diff |
annotate
|
Sat, 26 Mar 2016 12:17:02 +0100 |
wenzelm |
eliminated duplicate;
|
file |
diff |
annotate
|
Fri, 18 Mar 2016 17:58:19 +0100 |
wenzelm |
discontinued slightly odd "secure" mode;
|
file |
diff |
annotate
|
Fri, 18 Mar 2016 17:11:30 +0100 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
Fri, 18 Mar 2016 16:38:40 +0100 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
Thu, 17 Mar 2016 16:56:44 +0100 |
wenzelm |
@{make_string} is available during Pure bootstrap;
|
file |
diff |
annotate
|
Thu, 17 Mar 2016 13:44:18 +0100 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
Thu, 17 Mar 2016 10:54:28 +0100 |
wenzelm |
hide critical structures of Poly/ML, to make it harder to disrupt the ML environment;
|
file |
diff |
annotate
|
Thu, 17 Mar 2016 10:22:50 +0100 |
wenzelm |
obsolete;
|
file |
diff |
annotate
|