2016-08-12 wenzelm 2016-08-12 liberal name as in document antiquotations;
2016-04-13 wenzelm 2016-04-13 eliminated "xname" and variants;
2016-04-09 wenzelm 2016-04-09 flags as in 'ML' command;
2016-04-08 wenzelm 2016-04-08 eliminated unused simproc identifier;
2016-04-07 wenzelm 2016-04-07 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; avoid slowdown of Resources.loaded_files due to command name 'use' in Pure base syntax;
2016-04-07 wenzelm 2016-04-07 simplified default print_depth: context is usually available, in contrast to 0d295e339f52;
2016-04-06 wenzelm 2016-04-06 clarified modules; tuned signature;
2016-04-05 wenzelm 2016-04-05 clarified modules -- simplified bootstrap;
2016-04-05 wenzelm 2016-04-05 clarified modules -- simplified bootstrap;
2016-04-05 wenzelm 2016-04-05 support bootstrap from fresh SML environment, with syntax of Isabelle/ML or SML;
2016-04-04 wenzelm 2016-04-04 clarified conditional compilation;
2015-12-09 wenzelm 2015-12-09 clarified type Token.src: plain token list, with usual implicit value assignment; clarified type Token.name_value, notably for head of Token.src; clarified Attrib/Method check_src vs. parser;
2015-11-07 wenzelm 2015-11-07 ML cartouches via control antiquotation;
2015-11-06 wenzelm 2015-11-06 more formal treatment of control symbols;
2015-10-18 wenzelm 2015-10-18 clarified control antiquotations: decode control symbol to get name; document antiquotations @{emph}, @{bold}; symbol interpretation for \<^emph>; tuned;
2015-10-18 wenzelm 2015-10-18 support control symbol antiquotations;
2015-04-03 wenzelm 2015-04-03 more uniform "verbose" option to print name space;
2014-12-10 wenzelm 2014-12-10 more careful handling of auxiliary environment structure -- allow nested ML evaluation;
2014-12-08 wenzelm 2014-12-08 expand ML cartouches to Input.source; tuned signature;
2014-11-30 wenzelm 2014-11-30 tuned signature;
2014-11-30 wenzelm 2014-11-30 more abstract type Input.source;
2014-11-26 wenzelm 2014-11-26 renamed "pairself" to "apply2", in accordance to @{apply 2};
2014-11-12 wenzelm 2014-11-12 more careful ML source positions, for improved PIDE markup;
2014-11-11 wenzelm 2014-11-11 more careful ML source positions, for improved PIDE markup;
2014-11-11 wenzelm 2014-11-11 more position information, e.g. relevant for errors in generated ML source;
2014-11-07 wenzelm 2014-11-07 plain value Keywords.keywords, which might be used outside theory for bootstrap purposes; plain value Outer_Syntax within theory: parsing requires current theory context; clarified name of Keyword.is_literal according to its semantics; eliminated pointless type Keyword.T; simplified @{command_spec}; clarified bootstrap keywords and syntax: take it as basis instead of side-branch;
2014-11-05 wenzelm 2014-11-05 explicit type Keyword.keywords; tuned signature;
2014-08-19 wenzelm 2014-08-19 tuned signature -- moved type src to Token, without aliases;
2014-07-31 wenzelm 2014-07-31 prefer dynamic ML_print_depth if context happens to be available;
2014-07-31 wenzelm 2014-07-31 clarified compile-time use of ML_print_depth;
2014-04-06 wenzelm 2014-04-06 clarified ML bootstrap;
2014-03-27 wenzelm 2014-03-27 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); more explicit ML_Compiler.flags;
2014-03-27 wenzelm 2014-03-27 clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
2014-03-26 wenzelm 2014-03-26 prefer Context_Position where a context is available; prefer explicit Context_Position.is_visible -- avoid redundant message composition; tuned signature;
2014-03-25 wenzelm 2014-03-25 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);
2014-03-25 wenzelm 2014-03-25 separate tokenization and language context for SML: no symbols, no antiquotes;
2014-03-25 wenzelm 2014-03-25 added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
2014-03-20 wenzelm 2014-03-20 tuned error, according to "use" in General/secure.ML;
2014-03-18 wenzelm 2014-03-18 clarified modules; more antiquotations for antiquotations;
2014-03-18 wenzelm 2014-03-18 clarified bootstrap process: switch to ML with context and antiquotations earlier;
2014-03-18 wenzelm 2014-03-18 tuned signature;
2014-03-18 wenzelm 2014-03-18 tuned signature -- rearranged modules;
2014-03-12 wenzelm 2014-03-12 ML_Context.check_antiquotation still required;
2014-03-12 wenzelm 2014-03-12 simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser; added command 'print_ML_antiquotations';
2014-03-10 wenzelm 2014-03-10 clarified Args.check_src: retain name space information for error output; tuned signature;
2014-03-10 wenzelm 2014-03-10 clarified Args.src: more abstract type, position refers to name only; prefer self-contained Args.check_src;
2014-03-01 wenzelm 2014-03-01 clarified language markup: added "delimited" property; type Symbol_Pos.source preserves information about delimited outer tokens (e.g string, cartouche); observe Completion.Language_Context only for delimited languages, which is important to complete keywords after undelimited inner tokens, e.g. "lemma A pro";
2014-02-25 wenzelm 2014-02-25 proper context for global data;
2014-02-17 wenzelm 2014-02-17 more markup;
2013-08-23 wenzelm 2013-08-23 added Theory.setup convenience;
2013-08-23 wenzelm 2013-08-23 clarified type ML_Context.antiq: context parser maintains compilation context, declaration is applied to final context; subtle change of semantics of ML_Context.add_antiq: need to avoid accidental update of context due to concrete syntax parser (cf. Scan.pass);
2013-08-23 wenzelm 2013-08-23 discontinued unused antiquotation blocks;
2013-08-16 wenzelm 2013-08-16 more markup via Name_Space.check; tuned signature;
2013-07-15 wenzelm 2013-07-15 retain compile-time context visibility, which is particularly important for "apply tactic";
2012-11-25 wenzelm 2012-11-25 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
2012-08-29 wenzelm 2012-08-29 renamed Position.str_of to;
2012-08-12 wenzelm 2012-08-12 more static antiquotations;
2012-08-11 wenzelm 2012-08-11 faster compilation of ML with antiquotations: static ML_context is bound once in auxiliary structure Isabelle;
2012-03-18 wenzelm 2012-03-18 maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming); more explicit Context.generic for Name_Space.declare/define and derivatives (NB: naming changed after Proof_Context.init_global); prefer Context.pretty in low-level operations of structure Sorts/Type (defer full Syntax.init_pretty until error output); simplified signatures;
2011-11-28 wenzelm 2011-11-28 separate module for concrete Isabelle markup;