2014-03-10 wenzelm 2014-03-10 some Markup.language_path to prevent completion of symbols (notably "~") -- always "delimited" for simplicity in contrast to 42ac3cfb89f6;
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-10 wenzelm 2014-03-10 tuned signature;
2014-03-09 wenzelm 2014-03-09 tuned signature;
2014-03-06 wenzelm 2014-03-06 more uniform check_const/read_const;
2014-03-06 wenzelm 2014-03-06 tuned signature -- more uniform check_type_name/read_type_name; proper reports for read_type_name (lost in 710bc66f432c);
2014-03-02 wenzelm 2014-03-02 clarified names of antiquotations and markup; more documentation;
2014-03-01 wenzelm 2014-03-01 tuned signature;
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-28 wenzelm 2014-02-28 tuned errors -- in accordance to ML antiquotations;
2014-02-28 wenzelm 2014-02-28 more explicit method reports; avoid combinator parsers with observable effect -- unreliable due to backtracking (Scan.FAIL) and incremental input (Scan.MORE);
2014-02-26 wenzelm 2014-02-26 method language markup, e.g. relevant to prevent outer keyword completion;
2014-02-25 wenzelm 2014-02-25 proper context for global data;
2014-02-25 wenzelm 2014-02-25 more markup;
2014-02-19 wenzelm 2014-02-19 prefer guarded where feasible;
2014-02-18 wenzelm 2014-02-18 more markup;
2014-02-18 wenzelm 2014-02-18 generic markup for embedded languages;
2014-02-17 wenzelm 2014-02-17 more markup;
2014-01-22 wenzelm 2014-01-22 tuned signature;
2013-12-09 wenzelm 2013-12-09 added document antiquotation @{url}, which produces formal markup for LaTeX and PIDE;
2013-08-23 wenzelm 2013-08-23 added Theory.setup convenience;
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-05-16 wenzelm 2013-05-16 Thy_Output.modes as proper option;
2013-05-16 wenzelm 2013-05-16 some system options as context-sensitive config options;
2013-05-13 wenzelm 2013-05-13 retain goal display options when printing error messages, to avoid breakdown for huge goals;
2013-04-05 wenzelm 2013-04-05 tuned signature -- agree with markup terminology;
2013-04-05 wenzelm 2013-04-05 unified terminology with Markup.DOCUMENT_SOURCE in Scala, which is unused but displayed as "document source" entity in Isabelle/jEdit;
2013-03-27 wenzelm 2013-03-27 more liberal handling of skipped proofs;
2013-02-24 wenzelm 2013-02-24 tuned;
2012-12-18 haftmann 2012-12-18 discontinued legacy antiquotations and styles
2012-11-30 wenzelm 2012-11-30 print formal entities with markup;
2012-11-25 wenzelm 2012-11-25 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
2012-10-13 wenzelm 2012-10-13 some attempts to unify/simplify pretty_goal;
2012-09-12 wenzelm 2012-09-12 avoid spaces in markup names, which might cause problems in boundary situations (e.g. HTML class);
2012-09-10 wenzelm 2012-09-10 formal markup for @{file} (for hyperlinks etc.) -- interpret path wrt. master directory as usual;
2012-08-29 wenzelm 2012-08-29 renamed Position.str_of to;
2012-08-26 wenzelm 2012-08-26 theory def/ref position reports, which enable hyperlinks etc.; more official header command parsing;
2012-08-24 wenzelm 2012-08-24 check side-comments of command spans (normally filtered out in Outer_Syntax.toplevel_source);
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;
2012-03-16 wenzelm 2012-03-16 define keywords early when processing the theory header, before running the body commands;
2012-03-16 wenzelm 2012-03-16 clarified Keyword.is_keyword: union of minor and major; misc tuning and simplification;
2012-03-15 wenzelm 2012-03-15 declare command keywords via theory header, including strict checking outside Pure;
2012-03-15 wenzelm 2012-03-15 declare minor keywords via theory header;
2012-03-14 wenzelm 2012-03-14 tuned;
2012-03-14 wenzelm 2012-03-14 source positions for locale and class expressions;
2012-03-04 wenzelm 2012-03-04 clarified command span: include trailing whitespace/comments and thus reduce number of ignored spans with associated transactions and states (factor 2); simplified signatures;
2012-01-25 wenzelm 2012-01-25 document antiquotations for ML infix operators;
2012-01-12 wenzelm 2012-01-12 tuned;
2011-11-28 wenzelm 2011-11-28 separate module for concrete Isabelle markup;
2011-07-23 wenzelm 2011-07-23 defer evaluation of Scan.message, for improved performance in the frequent situation where failure is handled later (e.g. via ||);
2011-06-27 wenzelm 2011-06-27 document antiquotations are managed as theory data, with proper name space and entity markup;
2011-05-03 wenzelm 2011-05-03 more conventional naming scheme: names_long, names_short, names_unique;
2011-05-02 wenzelm 2011-05-02 added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory; proper name bindings;
2011-04-30 wenzelm 2011-04-30 allow nested @{antiq} (nonterminal) and @@{antiq} terminal;
2011-04-18 wenzelm 2011-04-18 pretty_abbrev: read abbreviation more directly;
2011-04-16 wenzelm 2011-04-16 modernized structure Proof_Context;
2011-04-16 wenzelm 2011-04-16 prefer local name spaces; tuned signatures; tuned;
2011-04-16 wenzelm 2011-04-16 Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;