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;
Sat, 07 Nov 2015 00:28:42 +0100 wenzelm ML cartouches via control antiquotation;
Fri, 06 Nov 2015 23:31:50 +0100 wenzelm more formal treatment of control symbols;
Sun, 18 Oct 2015 20:28:29 +0200 wenzelm clarified control antiquotations: decode control symbol to get name;
Sun, 18 Oct 2015 17:24:24 +0200 wenzelm support control symbol antiquotations;
Fri, 03 Apr 2015 19:56:51 +0200 wenzelm more uniform "verbose" option to print name space;
Wed, 10 Dec 2014 19:24:54 +0100 wenzelm more careful handling of auxiliary environment structure -- allow nested ML evaluation;
Mon, 08 Dec 2014 22:42:12 +0100 wenzelm expand ML cartouches to Input.source;
Sun, 30 Nov 2014 14:02:48 +0100 wenzelm tuned signature;
Sun, 30 Nov 2014 12:24:56 +0100 wenzelm more abstract type Input.source;
Wed, 26 Nov 2014 20:05:34 +0100 wenzelm renamed "pairself" to "apply2", in accordance to @{apply 2};
Wed, 12 Nov 2014 10:30:59 +0100 wenzelm more careful ML source positions, for improved PIDE markup;
Tue, 11 Nov 2014 20:11:38 +0100 wenzelm more careful ML source positions, for improved PIDE markup;
Tue, 11 Nov 2014 18:16:25 +0100 wenzelm more position information, e.g. relevant for errors in generated ML source;
Fri, 07 Nov 2014 16:36:55 +0100 wenzelm plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
Wed, 05 Nov 2014 20:20:57 +0100 wenzelm explicit type Keyword.keywords;
Tue, 19 Aug 2014 23:17:51 +0200 wenzelm tuned signature -- moved type src to Token, without aliases;
Thu, 31 Jul 2014 22:02:21 +0200 wenzelm prefer dynamic ML_print_depth if context happens to be available;
Thu, 31 Jul 2014 20:59:10 +0200 wenzelm clarified compile-time use of ML_print_depth;
Sun, 06 Apr 2014 15:19:22 +0200 wenzelm clarified ML bootstrap;
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);
Thu, 27 Mar 2014 17:12:40 +0100 wenzelm clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
Wed, 26 Mar 2014 14:41:52 +0100 wenzelm prefer Context_Position where a context is available;
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);
Tue, 25 Mar 2014 16:11:00 +0100 wenzelm separate tokenization and language context for SML: no symbols, no antiquotes;
Tue, 25 Mar 2014 13:18:10 +0100 wenzelm added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
Thu, 20 Mar 2014 19:24:51 +0100 wenzelm tuned error, according to "use" in General/secure.ML;
Tue, 18 Mar 2014 16:16:28 +0100 wenzelm clarified modules;
Tue, 18 Mar 2014 13:36:28 +0100 wenzelm clarified bootstrap process: switch to ML with context and antiquotations earlier;
Tue, 18 Mar 2014 11:27:09 +0100 wenzelm tuned signature;
Tue, 18 Mar 2014 11:07:47 +0100 wenzelm tuned signature -- rearranged modules;
Wed, 12 Mar 2014 22:41:04 +0100 wenzelm ML_Context.check_antiquotation still required;
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;
Mon, 10 Mar 2014 18:06:23 +0100 wenzelm clarified Args.check_src: retain name space information for error output;
Mon, 10 Mar 2014 16:30:07 +0100 wenzelm clarified Args.src: more abstract type, position refers to name only;
Sat, 01 Mar 2014 22:46:31 +0100 wenzelm clarified language markup: added "delimited" property;
Tue, 25 Feb 2014 14:56:58 +0100 wenzelm proper context for global data;
Mon, 17 Feb 2014 11:14:26 +0100 wenzelm more markup;
Fri, 23 Aug 2013 20:35:50 +0200 wenzelm added Theory.setup convenience;
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;
Fri, 23 Aug 2013 15:36:54 +0200 wenzelm discontinued unused antiquotation blocks;
Fri, 16 Aug 2013 22:39:31 +0200 wenzelm more markup via Name_Space.check;
Mon, 15 Jul 2013 19:23:19 +0200 wenzelm retain compile-time context visibility, which is particularly important for "apply tactic";
Sun, 25 Nov 2012 19:49:24 +0100 wenzelm Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
Wed, 29 Aug 2012 11:48:45 +0200 wenzelm renamed Position.str_of to Position.here;
Sun, 12 Aug 2012 19:09:55 +0200 wenzelm more static antiquotations;
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;
Sun, 18 Mar 2012 13:04:22 +0100 wenzelm maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
Mon, 28 Nov 2011 22:05:32 +0100 wenzelm separate module for concrete Isabelle markup;
Fri, 08 Jul 2011 11:50:58 +0200 wenzelm clarified Thy_Load.digest_file -- read ML files only once;
Mon, 27 Jun 2011 17:51:28 +0200 wenzelm proper checking of @{ML_antiquotation};
Mon, 27 Jun 2011 16:53:31 +0200 wenzelm ML antiquotations are managed as theory data, with proper name space and entity markup;
Sat, 16 Apr 2011 15:47:52 +0200 wenzelm modernized structure Proof_Context;
Sun, 09 Jan 2011 19:58:08 +0100 wenzelm ML_trace: observe context visibility flag (import for Latex mode, for example);
Tue, 21 Dec 2010 19:35:36 +0100 wenzelm configuration option "ML_trace";
Fri, 01 Oct 2010 17:06:49 +0200 haftmann moved ML_Context.value to Code_Runtime
Thu, 30 Sep 2010 09:45:18 +0200 haftmann value uses bare compiler invocation: generated code does not contain antiquotations
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;
Fri, 17 Sep 2010 20:18:27 +0200 wenzelm tuned signature of (Context_)Position.report variants;
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
less more (0) -100 -60 tip