| Mon, 03 Jul 2017 09:12:13 +0200 |
wenzelm |
unused;
|
file |
diff |
annotate
|
| Fri, 25 Sep 2015 19:13:47 +0200 |
wenzelm |
tuned signature: eliminated pointless type Context.pretty;
|
file |
diff |
annotate
|
| Tue, 31 Mar 2015 21:12:22 +0200 |
wenzelm |
subtle change of long-standing name space policy: unknown entries are treated as hidden, consequently "private" is understood in the strict sense;
|
file |
diff |
annotate
|
| Tue, 31 Mar 2015 20:18:10 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sun, 29 Mar 2015 19:24:07 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Wed, 26 Nov 2014 20:05:34 +0100 |
wenzelm |
renamed "pairself" to "apply2", in accordance to @{apply 2};
|
file |
diff |
annotate
|
| Sat, 08 Nov 2014 17:39:01 +0100 |
wenzelm |
clarified name of Type.unified, to emphasize its connection to the "unify" family;
|
file |
diff |
annotate
|
| Sat, 08 Nov 2014 15:01:05 +0100 |
wenzelm |
recovered type matching, which was broken in 8a765db7e0f8 (see also 8a765db7e0f8, 2db1d3d2ed54);
|
file |
diff |
annotate
|
| Thu, 13 Mar 2014 17:26:22 +0100 |
wenzelm |
more frugal recording of changes: join merely requires information from one side;
|
file |
diff |
annotate
|
| Tue, 11 Mar 2014 22:49:28 +0100 |
wenzelm |
more efficient local theory operations, by imposing a linear change discipline on the main types/consts tables, in order to speed-up Proof_Context.transfer_syntax required for Local_Theory.raw_theory_result;
|
file |
diff |
annotate
|
| Tue, 11 Mar 2014 10:14:45 +0100 |
wenzelm |
minor performance tuning via fast matching filter;
|
file |
diff |
annotate
|
| Mon, 10 Mar 2014 13:55:03 +0100 |
wenzelm |
abstract type Name_Space.table;
|
file |
diff |
annotate
|
| Sun, 09 Mar 2014 17:43:40 +0100 |
wenzelm |
unused;
|
file |
diff |
annotate
|
| Thu, 06 Mar 2014 16:12:26 +0100 |
wenzelm |
reject internal term names outright, and complete consts instead;
|
file |
diff |
annotate
|
| Wed, 05 Mar 2014 18:26:35 +0100 |
wenzelm |
more markup for inner syntax class/type names (notably for completion);
|
file |
diff |
annotate
|
| Sun, 02 Mar 2014 21:02:27 +0100 |
wenzelm |
prefer Name_Space.check with its builtin reports (including completion);
|
file |
diff |
annotate
|
| Sat, 11 May 2013 16:57:18 +0200 |
wenzelm |
prefer explicitly qualified exceptions, which is particular important for robust handlers;
|
file |
diff |
annotate
|
| Fri, 12 Apr 2013 15:30:38 +0200 |
wenzelm |
tuned exceptions -- avoid composing error messages in low-level situations;
|
file |
diff |
annotate
|
| Sun, 25 Nov 2012 19:49:24 +0100 |
wenzelm |
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
|
file |
diff |
annotate
|
| Wed, 03 Oct 2012 16:42:36 +0200 |
wenzelm |
use explicit Type.strip_sorts_dummy to suppress sort constraints in output;
|
file |
diff |
annotate
|
| Wed, 29 Aug 2012 11:48:45 +0200 |
wenzelm |
renamed Position.str_of to Position.here;
|
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
|
| Fri, 24 Feb 2012 18:14:06 +0100 |
wenzelm |
clarifed name space "type name", which covers logical and non-logical types, and often occurs inside outer syntax "type" markup;
|
file |
diff |
annotate
|
| Mon, 28 Nov 2011 22:05:32 +0100 |
wenzelm |
separate module for concrete Isabelle markup;
|
file |
diff |
annotate
|
| Sun, 20 Nov 2011 15:21:22 +0100 |
wenzelm |
clarified certify vs. sharing;
|
file |
diff |
annotate
|
| Thu, 10 Nov 2011 22:32:10 +0100 |
wenzelm |
pass term positions into check phase, where resulting types are reported accordingly, and eventually shown as tooltips;
|
file |
diff |
annotate
|
| Wed, 10 Aug 2011 19:21:28 +0200 |
wenzelm |
avoid OldTerm operations -- with subtle changes of semantics;
|
file |
diff |
annotate
|
| Sat, 25 Jun 2011 19:38:35 +0200 |
wenzelm |
entity markup for "type", "constant";
|
file |
diff |
annotate
|
| Sat, 25 Jun 2011 18:15:36 +0200 |
wenzelm |
type classes: entity markup instead of old-style token markup;
|
file |
diff |
annotate
|
| Thu, 09 Jun 2011 17:51:49 +0200 |
wenzelm |
simplified Name.variant -- discontinued builtin fold_map;
|
file |
diff |
annotate
|