Mercurial Mercurial > repos > isabelle / file revisions
summary | shortlog | changelog | graph | tags | bookmarks | branches | file | revisions | annotate | diff | comparison | rss | help
(0) -100 -60 tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Pure/ML/ml_context.ML
Fri, 20 Oct 2023 16:40:41 +0200 wenzelm clarified signature; file | diff | annotate
Thu, 28 Sep 2023 20:07:30 +0200 wenzelm explicitly reject 'handle' with catch-all patterns; file | diff | annotate
Sun, 24 Sep 2023 15:14:45 +0200 wenzelm clarified signature; file | diff | annotate
Thu, 11 May 2023 21:32:22 +0200 wenzelm proper position for ML-like commands; file | diff | annotate
Tue, 03 Jan 2023 16:05:07 +0100 wenzelm clarified modules; file | diff | annotate
Tue, 03 Jan 2023 14:00:59 +0100 wenzelm tuned signature: avoid too many aliases (see also 72daee8a39ca); file | diff | annotate
Thu, 21 Oct 2021 18:10:51 +0200 wenzelm clarified modules; file | diff | annotate
Wed, 20 Oct 2021 20:04:28 +0200 wenzelm clarified modules; file | diff | annotate
Wed, 20 Oct 2021 18:13:17 +0200 wenzelm discontinued obsolete "val extend = I" for data slots; file | diff | annotate
Sat, 10 Apr 2021 14:55:50 +0200 wenzelm proper treatment of nested antiquotations; file | diff | annotate
Fri, 09 Apr 2021 21:07:11 +0200 wenzelm clarified signature: more detailed token positions for antiquotations; file | diff | annotate
Fri, 04 Jan 2019 21:49:06 +0100 wenzelm support for isabelle update -u control_cartouches; file | diff | annotate
Wed, 31 Oct 2018 15:53:32 +0100 wenzelm clarified ML_Context.expression: it is a closed expression, not a let-declaration -- thus source positions are more accurate (amending d8849cfad60f, 162a4c2e97bc); file | diff | annotate
Thu, 25 Oct 2018 21:29:08 +0200 wenzelm clarified ML position: proper markup for def/ref scopes (see also 162a4c2e97bc); file | diff | annotate
Fri, 31 Aug 2018 22:25:58 +0200 wenzelm support multiple inheritance of ML environments, with canonical merge order as in Context.begin_theory; file | diff | annotate
Mon, 27 Aug 2018 20:43:01 +0200 wenzelm clarified signature; file | diff | annotate
Mon, 27 Aug 2018 19:12:48 +0200 wenzelm explicit setup of operations: avoid hardwired stuff; file | diff | annotate
Mon, 27 Aug 2018 17:30:13 +0200 wenzelm clarified environment: allow "read>write" specification; file | diff | annotate
Mon, 27 Aug 2018 14:42:24 +0200 wenzelm support named ML environments, notably "Isabelle", "SML"; file | diff | annotate
Fri, 12 Aug 2016 11:54:36 +0200 wenzelm liberal name as in document antiquotations; file | diff | annotate
Wed, 13 Apr 2016 18:01:05 +0200 wenzelm eliminated "xname" and variants; file | diff | annotate
Sat, 09 Apr 2016 19:09:11 +0200 wenzelm flags as in 'ML' command; file | diff | annotate
Fri, 08 Apr 2016 20:15:20 +0200 wenzelm eliminated unused simproc identifier; 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 13:54:02 +0200 wenzelm simplified default print_depth: context is usually available, in contrast to 0d295e339f52; file | diff | annotate
Wed, 06 Apr 2016 16:33:33 +0200 wenzelm clarified modules; file | diff | annotate
Tue, 05 Apr 2016 20:51:37 +0200 wenzelm clarified modules -- simplified bootstrap; file | diff | annotate
Tue, 05 Apr 2016 20:03:24 +0200 wenzelm clarified modules -- simplified bootstrap; file | diff | annotate
Tue, 05 Apr 2016 18:20:25 +0200 wenzelm support bootstrap from fresh SML environment, with syntax of Isabelle/ML or SML; file | diff | annotate
Mon, 04 Apr 2016 19:48:54 +0200 wenzelm clarified conditional compilation; file | diff | annotate
Wed, 09 Dec 2015 16:36:26 +0100 wenzelm clarified type Token.src: plain token list, with usual implicit value assignment; file | diff | annotate
Sat, 07 Nov 2015 00:28:42 +0100 wenzelm ML cartouches via control antiquotation; file | diff | annotate
Fri, 06 Nov 2015 23:31:50 +0100 wenzelm more formal treatment of control symbols; file | diff | annotate
Sun, 18 Oct 2015 20:28:29 +0200 wenzelm clarified control antiquotations: decode control symbol to get name; file | diff | annotate
Sun, 18 Oct 2015 17:24:24 +0200 wenzelm support control symbol antiquotations; file | diff | annotate
Fri, 03 Apr 2015 19:56:51 +0200 wenzelm more uniform "verbose" option to print name space; file | diff | annotate
Wed, 10 Dec 2014 19:24:54 +0100 wenzelm more careful handling of auxiliary environment structure -- allow nested ML evaluation; file | diff | annotate
Mon, 08 Dec 2014 22:42:12 +0100 wenzelm expand ML cartouches to Input.source; file | diff | annotate
Sun, 30 Nov 2014 14:02:48 +0100 wenzelm tuned signature; file | diff | annotate
Sun, 30 Nov 2014 12:24:56 +0100 wenzelm more abstract type Input.source; file | diff | annotate
Wed, 26 Nov 2014 20:05:34 +0100 wenzelm renamed "pairself" to "apply2", in accordance to @{apply 2}; file | diff | annotate
Wed, 12 Nov 2014 10:30:59 +0100 wenzelm more careful ML source positions, for improved PIDE markup; file | diff | annotate
Tue, 11 Nov 2014 20:11:38 +0100 wenzelm more careful ML source positions, for improved PIDE markup; file | diff | annotate
Tue, 11 Nov 2014 18:16:25 +0100 wenzelm more position information, e.g. relevant for errors in generated ML source; 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
Tue, 19 Aug 2014 23:17:51 +0200 wenzelm tuned signature -- moved type src to Token, without aliases; file | diff | annotate
Thu, 31 Jul 2014 22:02:21 +0200 wenzelm prefer dynamic ML_print_depth if context happens to be available; file | diff | annotate
Thu, 31 Jul 2014 20:59:10 +0200 wenzelm clarified compile-time use of ML_print_depth; file | diff | annotate
Sun, 06 Apr 2014 15:19:22 +0200 wenzelm clarified ML bootstrap; file | diff | annotate
Thu, 27 Mar 2014 17:56:13 +0100 wenzelm redirect ML_Compiler reports more directly: only the (big) parse tree report is deferred via Execution.print (NB: this does not work for asynchronous "diag" commands); file | diff | annotate
Thu, 27 Mar 2014 17:12:40 +0100 wenzelm clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler; file | diff | annotate
Wed, 26 Mar 2014 14:41:52 +0100 wenzelm prefer Context_Position where a context is available; file | diff | annotate
Tue, 25 Mar 2014 16:54:38 +0100 wenzelm clarified options ML_source_trace and ML_exception_trace (NB: the latter needs to be a system option, since the context is sometimes not available, e.g. for 'theory' command); file | diff | annotate
Tue, 25 Mar 2014 16:11:00 +0100 wenzelm separate tokenization and language context for SML: no symbols, no antiquotes; file | diff | annotate
Tue, 25 Mar 2014 13:18:10 +0100 wenzelm added command 'SML_file' for Standard ML without Isabelle/ML add-ons; file | diff | annotate
Thu, 20 Mar 2014 19:24:51 +0100 wenzelm tuned error, according to "use" in General/secure.ML; file | diff | annotate
Tue, 18 Mar 2014 16:16:28 +0100 wenzelm clarified modules; file | diff | annotate
Tue, 18 Mar 2014 13:36:28 +0100 wenzelm clarified bootstrap process: switch to ML with context and antiquotations earlier; file | diff | annotate
Tue, 18 Mar 2014 11:27:09 +0100 wenzelm tuned signature; file | diff | annotate
less more (0) -100 -60 tip
isabelle