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