| Wed, 17 Apr 2024 23:12:21 +0200 |
wenzelm |
update to jdk-21.0.3;
|
file |
diff |
annotate
|
| Thu, 21 Mar 2024 14:45:15 +0100 |
wenzelm |
enforce rebuild of Isabelle/ML;
|
file |
diff |
annotate
|
| Fri, 01 Mar 2024 21:23:47 +0100 |
wenzelm |
update to scala-3.3.3;
|
file |
diff |
annotate
|
| Thu, 29 Feb 2024 21:06:50 +0100 |
wenzelm |
rebuild bash_process executables on current reference platforms, including native arm64-darwin;
|
file |
diff |
annotate
|
| Wed, 24 Jan 2024 22:43:41 +0100 |
wenzelm |
update to jdk-21.0.2;
|
file |
diff |
annotate
|
| Sat, 20 Jan 2024 22:27:30 +0100 |
wenzelm |
enforce rebuild of Isabelle/Scala + Isabelle/ML;
|
file |
diff |
annotate
|
| Sat, 20 Jan 2024 16:23:51 +0100 |
wenzelm |
clarified bootstrap;
|
file |
diff |
annotate
|
| Sat, 20 Jan 2024 16:09:35 +0100 |
wenzelm |
clarified directories;
|
file |
diff |
annotate
|
| Sat, 20 Jan 2024 15:07:41 +0100 |
wenzelm |
clarified directories;
|
file |
diff |
annotate
|
| Thu, 21 Dec 2023 21:03:02 +0100 |
wenzelm |
proper thm_name for stored zproof;
|
file |
diff |
annotate
|
| Fri, 01 Dec 2023 16:10:09 +0100 |
wenzelm |
clarified bootstrap --- modules related to proofterm.ML;
|
file |
diff |
annotate
|
| Thu, 30 Nov 2023 23:15:18 +0100 |
wenzelm |
tight representation of types / terms / proof terms (presently unused);
|
file |
diff |
annotate
|
| Wed, 29 Nov 2023 00:07:54 +0100 |
wenzelm |
compact representation of sets of integers;
|
file |
diff |
annotate
|
| Fri, 24 Nov 2023 15:58:24 +0100 |
wenzelm |
support for Unix-domain sockets, using java.nio.channels.ServerSocketChannel;
|
file |
diff |
annotate
|
| Mon, 20 Nov 2023 19:52:46 +0100 |
wenzelm |
update to jdk-21.0.1;
|
file |
diff |
annotate
|
| Sat, 21 Oct 2023 21:19:02 +0200 |
wenzelm |
simprocs may be distinguished via 'identifier': only works for ML antiquotation (see also 13252110a6fe);
|
file |
diff |
annotate
|
| Sun, 15 Oct 2023 13:36:48 +0200 |
wenzelm |
updated to stack-2.13.1: include arm64-darwin, although it does not quite work yet (e.g. session "Haskell");
|
file |
diff |
annotate
|
| Mon, 25 Sep 2023 21:30:46 +0200 |
wenzelm |
clarified order of modules: early access to interrupt management of Isabelle_Threads;
|
file |
diff |
annotate
|
| Thu, 21 Sep 2023 17:04:56 +0200 |
wenzelm |
more robust: prefer linear data flow;
|
file |
diff |
annotate
|
| Mon, 04 Sep 2023 17:25:16 +0200 |
wenzelm |
tuned whitespace;
|
file |
diff |
annotate
|
| Wed, 30 Aug 2023 21:03:30 +0200 |
wenzelm |
update to "scalac -source 3.3" (from 3.1);
|
file |
diff |
annotate
|
| Wed, 31 May 2023 11:14:15 +0200 |
wenzelm |
enable scala-3.3.0, with forced rebuild of Isabelle/Scala and Isabelle/ML;
|
file |
diff |
annotate
|
| Tue, 09 May 2023 23:12:09 +0200 |
wenzelm |
enforce rebuild of Isabelle/ML + Isabelle/Scala;
|
file |
diff |
annotate
|
| Wed, 19 Apr 2023 23:27:33 +0200 |
wenzelm |
more operations, following Isabelle/ML conventions;
|
file |
diff |
annotate
|
| Fri, 14 Apr 2023 21:34:51 +0200 |
wenzelm |
more operations, following Isabelle/ML conventions;
|
file |
diff |
annotate
|
| Fri, 14 Apr 2023 20:42:17 +0200 |
wenzelm |
more operations, following Isabelle/ML conventions;
|
file |
diff |
annotate
|
| Thu, 13 Apr 2023 23:16:18 +0200 |
wenzelm |
compact representation of long name "chunks", with bitmask to suppress elements (i.e. "accesses" in name space terminology);
|
file |
diff |
annotate
|
| Sat, 01 Apr 2023 13:04:59 +0200 |
wenzelm |
tuned: prefer "build" combinator;
|
file |
diff |
annotate
|
| Mon, 27 Mar 2023 19:41:18 +0200 |
wenzelm |
efficient representation of sets: more compact than Table.set;
|
file |
diff |
annotate
|
| Tue, 14 Mar 2023 20:31:30 +0100 |
wenzelm |
enforce rebuild of Isabelle/ML;
|
file |
diff |
annotate
|
| Mon, 13 Mar 2023 22:21:33 +0100 |
wenzelm |
enforce rebuild of Isabelle/ML;
|
file |
diff |
annotate
|
| Thu, 09 Mar 2023 14:29:46 +0100 |
wenzelm |
enforce rebuild of Isabelle/ML;
|
file |
diff |
annotate
|
| Wed, 08 Mar 2023 22:43:04 +0100 |
wenzelm |
enforce rebuild of Isabelle/ML;
|
file |
diff |
annotate
|
| Sun, 05 Mar 2023 20:41:45 +0100 |
wenzelm |
enforce rebuild of Isabelle/ML, after various changes to build database management;
|
file |
diff |
annotate
|
| Sun, 05 Mar 2023 12:52:04 +0100 |
wenzelm |
enforce rebuild of Isabelle/ML, after various changes to build database management;
|
file |
diff |
annotate
|
| Sun, 26 Feb 2023 20:27:11 +0100 |
wenzelm |
enforce rebuild of Isabelle/ML, after various changes to build database management;
|
file |
diff |
annotate
|
| Fri, 27 Jan 2023 15:22:26 +0100 |
wenzelm |
back to Scala 3.2.0 for now, since 3.2.1 causes odd crash of REPL concerning value classes (e.g. "isabelle.Time.now()");
|
file |
diff |
annotate
|
| Sun, 22 Jan 2023 23:29:34 +0100 |
wenzelm |
update to jdk-17.0.6;
|
file |
diff |
annotate
|
| Fri, 06 Jan 2023 17:59:56 +0100 |
wenzelm |
enforce rebuild of Isabelle/ML to update build databases;
|
file |
diff |
annotate
|
| Sun, 01 Jan 2023 21:44:08 +0100 |
wenzelm |
store session sources within build database: timing e.g. 150ms for HOL and < 50ms for common sessions;
|
file |
diff |
annotate
|
| Wed, 28 Dec 2022 16:02:12 +0100 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Fri, 25 Nov 2022 21:58:40 +0100 |
wenzelm |
update to scala-3.2.1;
|
file |
diff |
annotate
|
| Sun, 13 Nov 2022 20:28:39 +0100 |
wenzelm |
ML support for the Prism.js syntax highlighter -- via Isabelle/Scala;
|
file |
diff |
annotate
|
| Fri, 21 Oct 2022 16:39:31 +0200 |
wenzelm |
generic support for XZ and Zstd compression in Isabelle/Scala;
|
file |
diff |
annotate
|
| Thu, 20 Oct 2022 23:46:49 +0200 |
wenzelm |
enforce fresh build;
|
file |
diff |
annotate
|
| Fri, 16 Sep 2022 16:34:45 +0200 |
wenzelm |
update to scala-3.2.0;
|
file |
diff |
annotate
|
| Mon, 05 Sep 2022 21:18:40 +0200 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Fri, 26 Aug 2022 21:25:35 +0200 |
wenzelm |
tuned whitespace;
|
file |
diff |
annotate
|
| Thu, 25 Aug 2022 15:30:21 +0200 |
wenzelm |
maintain "uuid" column in session build database, to identity the original build process uniquely;
|
file |
diff |
annotate
|
| Sat, 23 Jul 2022 11:26:28 +0200 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Fri, 22 Jul 2022 15:15:26 +0200 |
wenzelm |
command 'scala_build_generated_files' with proper management of source dependencies;
|
file |
diff |
annotate
|
| Thu, 21 Jul 2022 14:26:53 +0200 |
wenzelm |
support for Java language;
|
file |
diff |
annotate
|
| Fri, 08 Jul 2022 22:29:26 +0200 |
wenzelm |
support for Isabelle/Scala/Java modules in Isabelle/ML;
|
file |
diff |
annotate
|
| Sat, 25 Jun 2022 16:51:24 +0200 |
wenzelm |
prefer antiquotations;
|
file |
diff |
annotate
|
| Sat, 25 Jun 2022 13:19:15 +0200 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Fri, 24 Jun 2022 23:31:28 +0200 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Tue, 21 Jun 2022 13:14:09 +0200 |
wenzelm |
support for scalable byte strings, with incremental construction;
|
file |
diff |
annotate
|
| Thu, 28 Oct 2021 11:37:49 +0200 |
wenzelm |
tuned modules;
|
file |
diff |
annotate
|
| Tue, 26 Oct 2021 16:01:05 +0200 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Wed, 20 Oct 2021 16:45:10 +0200 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Thu, 09 Sep 2021 15:45:27 +0200 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| 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
|
| Thu, 17 Mar 2016 10:21:43 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Wed, 16 Mar 2016 22:06:05 +0100 |
wenzelm |
eliminated without magic name;
|
file |
diff |
annotate
|
| Thu, 10 Mar 2016 09:56:29 +0100 |
wenzelm |
clarified files;
|
file |
diff |
annotate
|
| Thu, 10 Mar 2016 09:50:53 +0100 |
wenzelm |
clarified files;
|
file |
diff |
annotate
|
| Wed, 09 Mar 2016 19:30:09 +0100 |
wenzelm |
isabelle.Build uses ML_Process directly;
|
file |
diff |
annotate
|
| Mon, 07 Mar 2016 21:53:21 +0100 |
wenzelm |
discontinued cd, pwd;
|
file |
diff |
annotate
|
| Sat, 05 Mar 2016 17:01:45 +0100 |
wenzelm |
tuned signature -- clarified modules;
|
file |
diff |
annotate
|
| Sat, 05 Mar 2016 13:51:21 +0100 |
wenzelm |
tuned signature -- clarified modules;
|
file |
diff |
annotate
|
| Thu, 03 Mar 2016 21:59:21 +0100 |
wenzelm |
discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM;
|
file |
diff |
annotate
|
| Thu, 03 Mar 2016 11:12:02 +0100 |
wenzelm |
discontinued polyml-5.3.0;
|
file |
diff |
annotate
|
| Wed, 02 Mar 2016 19:43:31 +0100 |
wenzelm |
support for ML_exception_debugger;
|
file |
diff |
annotate
|
| Tue, 01 Mar 2016 22:11:36 +0100 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Tue, 01 Mar 2016 21:10:29 +0100 |
wenzelm |
load secure.ML earlier;
|
file |
diff |
annotate
|
| Tue, 01 Mar 2016 19:42:59 +0100 |
wenzelm |
ML debugger support in Pure (again, see 3565c9f407ec);
|
file |
diff |
annotate
|
| Sun, 28 Feb 2016 21:20:51 +0100 |
wenzelm |
support only polyml-5.3.0 and polyml-5.6;
|
file |
diff |
annotate
|
| Thu, 18 Feb 2016 23:10:28 +0100 |
wenzelm |
unconditional Multithreading;
|
file |
diff |
annotate
|
| Wed, 17 Feb 2016 23:28:58 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 17 Feb 2016 23:15:47 +0100 |
wenzelm |
clarified file names;
|
file |
diff |
annotate
|
| Wed, 17 Feb 2016 23:06:24 +0100 |
wenzelm |
SML/NJ is no longer supported;
|
file |
diff |
annotate
|
| Sun, 06 Dec 2015 23:10:08 +0100 |
wenzelm |
discontinued intermediate polyml-5.5.3, assuming the coming release will be polyml-5.6;
|
file |
diff |
annotate
|
| Fri, 20 Nov 2015 21:52:05 +0100 |
wenzelm |
speculative support for polyml-5.6, according to git commit 3527f4ba7b8b;
|
file |
diff |
annotate
|
| Sat, 14 Nov 2015 08:45:51 +0100 |
haftmann |
separate ML module for interpretation
|
file |
diff |
annotate
|
| Tue, 10 Nov 2015 21:31:14 +0100 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Tue, 03 Nov 2015 13:54:34 +0100 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Thu, 15 Oct 2015 17:29:37 +0200 |
wenzelm |
load markdown.ML into Pure;
|
file |
diff |
annotate
|
| Fri, 25 Sep 2015 20:37:59 +0200 |
wenzelm |
moved remaining display.ML to more_thm.ML;
|
file |
diff |
annotate
|
| Thu, 24 Sep 2015 23:33:29 +0200 |
wenzelm |
more explicit Defs.context: use proper name spaces as far as possible;
|
file |
diff |
annotate
|
| Mon, 17 Aug 2015 23:45:12 +0200 |
wenzelm |
basic setup for native Windows (RAW session without image);
|
file |
diff |
annotate
|
| Mon, 17 Aug 2015 21:32:41 +0200 |
wenzelm |
no ML_debugger support in Pure -- too complicated;
|
file |
diff |
annotate
|
| Mon, 17 Aug 2015 21:22:55 +0200 |
wenzelm |
more careful propagation of ML_debugger option to Pure;
|
file |
diff |
annotate
|
| Mon, 17 Aug 2015 19:34:15 +0200 |
wenzelm |
support for ML files with/without debugger information;
|
file |
diff |
annotate
|
| Mon, 17 Aug 2015 16:27:12 +0200 |
wenzelm |
explicit debug flag for ML compiler;
|
file |
diff |
annotate
|
| Sat, 15 Aug 2015 19:42:35 +0200 |
wenzelm |
clarified context;
|
file |
diff |
annotate
|
| Wed, 12 Aug 2015 01:39:31 +0200 |
wenzelm |
default ML context for forks, e.g. relevant for debugging and toplevel pretty-printing;
|
file |
diff |
annotate
|
| Thu, 02 Jul 2015 12:39:08 +0200 |
wenzelm |
clarified module;
|
file |
diff |
annotate
|
| Wed, 01 Apr 2015 22:08:06 +0200 |
wenzelm |
added command 'experiment';
|
file |
diff |
annotate
|
| Mon, 16 Mar 2015 11:30:54 +0100 |
wenzelm |
tuned protocol -- resolve command positions in ML;
|
file |
diff |
annotate
|
| Thu, 29 Jan 2015 16:16:01 +0100 |
wenzelm |
tuned bootstrap;
|
file |
diff |
annotate
|
| Wed, 14 Jan 2015 11:52:08 +0100 |
wenzelm |
added Path.decode in ML, in correspondence to Path.encode in Scala;
|
file |
diff |
annotate
|
| Tue, 30 Dec 2014 23:45:03 +0100 |
wenzelm |
explicit message channel for "legacy", which is nonetheless a variant of "warning";
|
file |
diff |
annotate
|
| Mon, 29 Dec 2014 15:38:59 +0100 |
wenzelm |
more toplevel pretty printing;
|
file |
diff |
annotate
|
| Mon, 22 Dec 2014 14:33:53 +0100 |
wenzelm |
separate module Random;
|
file |
diff |
annotate
|
| Wed, 03 Dec 2014 22:34:28 +0100 |
wenzelm |
node-specific keywords, with session base syntax as default;
|
file |
diff |
annotate
|
| Sun, 30 Nov 2014 12:24:56 +0100 |
wenzelm |
more abstract type Input.source;
|
file |
diff |
annotate
|
| Wed, 26 Nov 2014 11:43:51 +0100 |
wenzelm |
load simple_thread.ML later, such that it benefits from redefined print_exception_trace;
|
file |
diff |
annotate
|
| Fri, 21 Nov 2014 18:14:39 +0100 |
wenzelm |
removed some add-ons from modules that are relevant for the inference kernel;
|
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
|
| Wed, 05 Nov 2014 20:20:57 +0100 |
wenzelm |
explicit type Keyword.keywords;
|
file |
diff |
annotate
|
| Fri, 31 Oct 2014 16:03:45 +0100 |
wenzelm |
discontinued Isar TTY loop;
|
file |
diff |
annotate
|
| Fri, 31 Oct 2014 11:18:17 +0100 |
wenzelm |
discontinued Proof General;
|
file |
diff |
annotate
|
| Mon, 13 Oct 2014 20:51:48 +0200 |
wenzelm |
obsolete;
|
file |
diff |
annotate
|
| Mon, 13 Oct 2014 19:34:10 +0200 |
wenzelm |
clarified load order;
|
file |
diff |
annotate
|
| Mon, 29 Sep 2014 09:57:34 +0200 |
wenzelm |
pro-forma support for polyml-5.5.3 (presently SVN 1960);
|
file |
diff |
annotate
|
| Fri, 22 Aug 2014 12:05:47 +0200 |
wenzelm |
clarified ML toplevel pp: avoid ML output to be attached to inlined binding positions;
|
file |
diff |
annotate
|
| Tue, 19 Aug 2014 18:11:04 +0200 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Thu, 14 Aug 2014 10:48:40 +0200 |
wenzelm |
tuned signature -- prefer self-contained user-space tool;
|
file |
diff |
annotate
|
| Wed, 13 Aug 2014 13:30:28 +0200 |
wenzelm |
load local_theory.ML before attrib.ML, with subtle change of semantics due to canonical Local_Theory.map_contexts instead of private Local_Theory.map_top;
|
file |
diff |
annotate
|
| Tue, 12 Aug 2014 00:08:32 +0200 |
wenzelm |
separate module Command_Span: mostly syntactic representation;
|
file |
diff |
annotate
|
| Thu, 24 Jul 2014 15:54:56 +0200 |
wenzelm |
further distinction of Isabelle distribution: alert for identified release candidates;
|
file |
diff |
annotate
|