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
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
Tue, 18 Mar 2014 11:07:47 +0100 wenzelm tuned signature -- rearranged modules; file | diff | annotate
Wed, 12 Mar 2014 22:41:04 +0100 wenzelm ML_Context.check_antiquotation still required; file | diff | annotate
Wed, 12 Mar 2014 21:58:48 +0100 wenzelm simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser; file | diff | annotate
Mon, 10 Mar 2014 18:06:23 +0100 wenzelm clarified Args.check_src: retain name space information for error output; file | diff | annotate
Mon, 10 Mar 2014 16:30:07 +0100 wenzelm clarified Args.src: more abstract type, position refers to name only; file | diff | annotate
Sat, 01 Mar 2014 22:46:31 +0100 wenzelm clarified language markup: added "delimited" property; file | diff | annotate
Tue, 25 Feb 2014 14:56:58 +0100 wenzelm proper context for global data; file | diff | annotate
Mon, 17 Feb 2014 11:14:26 +0100 wenzelm more markup; file | diff | annotate
Fri, 23 Aug 2013 20:35:50 +0200 wenzelm added Theory.setup convenience; file | diff | annotate
Fri, 23 Aug 2013 19:53:27 +0200 wenzelm clarified type ML_Context.antiq: context parser maintains compilation context, declaration is applied to final context; file | diff | annotate
Fri, 23 Aug 2013 15:36:54 +0200 wenzelm discontinued unused antiquotation blocks; file | diff | annotate
Fri, 16 Aug 2013 22:39:31 +0200 wenzelm more markup via Name_Space.check; file | diff | annotate
Mon, 15 Jul 2013 19:23:19 +0200 wenzelm retain compile-time context visibility, which is particularly important for "apply tactic"; file | diff | annotate
Sun, 25 Nov 2012 19:49:24 +0100 wenzelm Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d; file | diff | annotate
Wed, 29 Aug 2012 11:48:45 +0200 wenzelm renamed Position.str_of to Position.here; file | diff | annotate
less more (0) -100 -60 tip
isabelle