src/HOL/ex/Cartouche_Examples.thy
2014-04-09 wenzelm 2014-04-09 proper Args.name vs. Args.text as documented (in contrast to adhoc union in 75aaee32893d, which had to cope with more limited Args.T);
2014-04-09 wenzelm 2014-04-09 allow text cartouches in regular outer syntax categories "text" and "altstring";
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-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-12 wenzelm 2014-03-12 tuned signature -- clarified module name;
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-01-25 wenzelm 2014-01-25 simplified inner syntax;
2014-01-22 wenzelm 2014-01-22 avoid breakdown of document preparation, which does not understand cartouche tokens yet;
2014-01-22 wenzelm 2014-01-22 more cartouche examples, including uniform nesting of sub-languages;
2014-01-19 wenzelm 2014-01-19 implicit "cartouche" method (experimental, undocumented);
2014-01-19 wenzelm 2014-01-19 more examples;
2014-01-18 wenzelm 2014-01-18 proper \<newline>;
2014-01-18 wenzelm 2014-01-18 support for nested text cartouches; clarified Symbol.is_symbolic: exclude \<open> and \<close>;