src/Pure/context_position.ML
2016-04-20 wenzelm 2016-04-20 avoid massive multiplication of reports due to interpretation;
2015-08-06 wenzelm 2015-08-06 evaluate ML expressions within debugger context; redirected writeln/warning for ML compiler;
2014-08-05 wenzelm 2014-08-05 refined context visibility again (amending f5f9fad3321c, 8e3e004f1c31): avoid spurious warning due to global config options;
2014-03-31 wenzelm 2014-03-31 support bulk messages consisting of small string segments, which are more healthy to the Poly/ML RTS and might prevent spurious GC crashes such as MTGCProcessMarkPointers::ScanAddressesInObject;
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-05 wenzelm 2014-03-05 tuned;
2014-02-22 wenzelm 2014-02-22 support for completion within the formal context; tuned signature;
2013-07-18 wenzelm 2013-07-18 provide global operations as well;
2013-07-18 wenzelm 2013-07-18 tuned signature;
2012-08-11 wenzelm 2012-08-11 reports with body text, not just markup;
2012-04-27 wenzelm 2012-04-27 made Context_Position independent from Config;
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-12 wenzelm 2012-03-12 tuned signature;
2011-09-06 wenzelm 2011-09-06 bulk reports for improved message throughput;
2011-01-08 wenzelm 2011-01-08 added Context_Position.is_visible_proof, which treats a global theory as invisible (unlike the default);
2010-09-17 wenzelm 2010-09-17 simplified some internal flags using Config.T instead of full-blown Proof_Data;
2010-09-17 wenzelm 2010-09-17 tuned signature of (Context_)Position.report variants;
2010-09-17 wenzelm 2010-09-17 simplified/clarified (Context_)Position.markup/reported_text;
2010-08-27 wenzelm 2010-08-27 more careful treatment of context visibility flag wrt. spurious warnings;
2010-08-19 wenzelm 2010-08-19 Output_Position.report_text -- markup with potential "arguments";
2010-08-08 wenzelm 2010-08-08 prefer Context_Position.report where a proper context is available -- notably for "inner" entities;
2009-11-08 wenzelm 2009-11-08 adapted Generic_Data, Proof_Data; tuned;
2009-11-02 wenzelm 2009-11-02 modernized structure Context_Position;
2009-01-21 wenzelm 2009-01-21 removed Ids;
2008-09-29 wenzelm 2008-09-29 renamed report to report_visible; tuned comments;
2008-09-29 wenzelm 2008-09-29 Context position visibility.
2007-10-01 wenzelm 2007-10-01 turned into generic context data;
2007-09-30 wenzelm 2007-09-30 added properties_of;
2007-06-13 wenzelm 2007-06-13 Context positions.