Tue, 05 Aug 2014 11:06:36 +0200 |
wenzelm |
refined context visibility again (amending f5f9fad3321c, 8e3e004f1c31): avoid spurious warning due to global config options;
|
file |
diff |
annotate
|
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;
|
file |
diff |
annotate
|
Wed, 26 Mar 2014 14:41:52 +0100 |
wenzelm |
prefer Context_Position where a context is available;
|
file |
diff |
annotate
|
Wed, 05 Mar 2014 19:52:28 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Sat, 22 Feb 2014 20:52:43 +0100 |
wenzelm |
support for completion within the formal context;
|
file |
diff |
annotate
|
Thu, 18 Jul 2013 21:57:27 +0200 |
wenzelm |
provide global operations as well;
|
file |
diff |
annotate
|
Thu, 18 Jul 2013 21:20:09 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Sat, 11 Aug 2012 17:23:09 +0200 |
wenzelm |
reports with body text, not just markup;
|
file |
diff |
annotate
|
Fri, 27 Apr 2012 21:44:44 +0200 |
wenzelm |
made Context_Position independent from Config;
|
file |
diff |
annotate
|
Sun, 18 Mar 2012 13:04:22 +0100 |
wenzelm |
maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
|
file |
diff |
annotate
|
Mon, 12 Mar 2012 15:31:30 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Tue, 06 Sep 2011 20:37:07 +0200 |
wenzelm |
bulk reports for improved message throughput;
|
file |
diff |
annotate
|
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);
|
file |
diff |
annotate
|
Fri, 17 Sep 2010 20:42:26 +0200 |
wenzelm |
simplified some internal flags using Config.T instead of full-blown Proof_Data;
|
file |
diff |
annotate
|
Fri, 17 Sep 2010 20:18:27 +0200 |
wenzelm |
tuned signature of (Context_)Position.report variants;
|
file |
diff |
annotate
|
Fri, 17 Sep 2010 17:09:31 +0200 |
wenzelm |
simplified/clarified (Context_)Position.markup/reported_text;
|
file |
diff |
annotate
|
Fri, 27 Aug 2010 19:43:28 +0200 |
wenzelm |
more careful treatment of context visibility flag wrt. spurious warnings;
|
file |
diff |
annotate
|
Thu, 19 Aug 2010 11:28:51 +0200 |
wenzelm |
Output_Position.report_text -- markup with potential "arguments";
|
file |
diff |
annotate
|
Sun, 08 Aug 2010 19:54:54 +0200 |
wenzelm |
prefer Context_Position.report where a proper context is available -- notably for "inner" entities;
|
file |
diff |
annotate
|
Sun, 08 Nov 2009 16:30:41 +0100 |
wenzelm |
adapted Generic_Data, Proof_Data;
|
file |
diff |
annotate
|
Mon, 02 Nov 2009 20:30:40 +0100 |
wenzelm |
modernized structure Context_Position;
|
file |
diff |
annotate
|
Wed, 21 Jan 2009 23:21:44 +0100 |
wenzelm |
removed Ids;
|
file |
diff |
annotate
|
Mon, 29 Sep 2008 21:26:26 +0200 |
wenzelm |
renamed report to report_visible;
|
file |
diff |
annotate
|
Mon, 29 Sep 2008 14:41:23 +0200 |
wenzelm |
Context position visibility.
|
file |
diff |
annotate
|
Mon, 01 Oct 2007 15:14:53 +0200 |
wenzelm |
turned into generic context data;
|
file |
diff |
annotate
|
Sun, 30 Sep 2007 16:20:35 +0200 |
wenzelm |
added properties_of;
|
file |
diff |
annotate
|
Wed, 13 Jun 2007 00:01:57 +0200 |
wenzelm |
Context positions.
|
file |
diff |
annotate
|