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
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
Sun, 12 Aug 2012 19:09:55 +0200 wenzelm more static antiquotations; file | diff | annotate
Sat, 11 Aug 2012 22:17:46 +0200 wenzelm faster compilation of ML with antiquotations: static ML_context is bound once in auxiliary structure Isabelle; file | diff | annotate
Sun, 18 Mar 2012 13:04:22 +0100 wenzelm maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming); file | diff | annotate
Mon, 28 Nov 2011 22:05:32 +0100 wenzelm separate module for concrete Isabelle markup; file | diff | annotate
Fri, 08 Jul 2011 11:50:58 +0200 wenzelm clarified Thy_Load.digest_file -- read ML files only once; file | diff | annotate
Mon, 27 Jun 2011 17:51:28 +0200 wenzelm proper checking of @{ML_antiquotation}; file | diff | annotate
Mon, 27 Jun 2011 16:53:31 +0200 wenzelm ML antiquotations are managed as theory data, with proper name space and entity markup; file | diff | annotate
Sat, 16 Apr 2011 15:47:52 +0200 wenzelm modernized structure Proof_Context; file | diff | annotate
Sun, 09 Jan 2011 19:58:08 +0100 wenzelm ML_trace: observe context visibility flag (import for Latex mode, for example); file | diff | annotate
Tue, 21 Dec 2010 19:35:36 +0100 wenzelm configuration option "ML_trace"; file | diff | annotate
Fri, 01 Oct 2010 17:06:49 +0200 haftmann moved ML_Context.value to Code_Runtime file | diff | annotate
Thu, 30 Sep 2010 09:45:18 +0200 haftmann value uses bare compiler invocation: generated code does not contain antiquotations file | diff | annotate
Mon, 20 Sep 2010 16:05:25 +0200 wenzelm renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only; file | diff | annotate
Fri, 17 Sep 2010 20:18:27 +0200 wenzelm tuned signature of (Context_)Position.report variants; file | diff | annotate
Wed, 15 Sep 2010 11:30:32 +0200 haftmann replaced ML_Context.evaluate by ML_Context.value -- using context data instead of bare metal references file | diff | annotate
less more (0) -100 -60 tip
isabelle