src/Pure/context_position.ML
Mon, 31 Mar 2014 10:28:08 +0200 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;
Wed, 26 Mar 2014 14:41:52 +0100 wenzelm prefer Context_Position where a context is available;
Wed, 05 Mar 2014 19:52:28 +0100 wenzelm tuned;
Sat, 22 Feb 2014 20:52:43 +0100 wenzelm support for completion within the formal context;
Thu, 18 Jul 2013 21:57:27 +0200 wenzelm provide global operations as well;
Thu, 18 Jul 2013 21:20:09 +0200 wenzelm tuned signature;
Sat, 11 Aug 2012 17:23:09 +0200 wenzelm reports with body text, not just markup;
Fri, 27 Apr 2012 21:44:44 +0200 wenzelm made Context_Position independent from Config;
Sun, 18 Mar 2012 13:04:22 +0100 wenzelm maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
Mon, 12 Mar 2012 15:31:30 +0100 wenzelm tuned signature;
Tue, 06 Sep 2011 20:37:07 +0200 wenzelm bulk reports for improved message throughput;
Sat, 08 Jan 2011 14:32:55 +0100 wenzelm added Context_Position.is_visible_proof, which treats a global theory as invisible (unlike the default);
Fri, 17 Sep 2010 20:42:26 +0200 wenzelm simplified some internal flags using Config.T instead of full-blown Proof_Data;
Fri, 17 Sep 2010 20:18:27 +0200 wenzelm tuned signature of (Context_)Position.report variants;
Fri, 17 Sep 2010 17:09:31 +0200 wenzelm simplified/clarified (Context_)Position.markup/reported_text;
less more (0) -15 tip