| Thu, 12 Sep 2024 20:15:28 +0200 |
wenzelm |
tuned signature: more operations;
|
file |
diff |
annotate
|
| Thu, 12 Sep 2024 19:52:01 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Thu, 05 Sep 2024 17:39:45 +0200 |
wenzelm |
clarified signature: type ML_Pretty.pretty coincides with PolyML.pretty;
|
file |
diff |
annotate
|
| Thu, 04 May 2023 11:42:04 +0200 |
wenzelm |
more accurate treatment of traditional name space accesses (refining 948f5dc4d694, fcd85e04a948, 238307775d52);
|
file |
diff |
annotate
|
| Tue, 02 May 2023 11:38:53 +0200 |
wenzelm |
minor performance tuning: no storage of accesses, produce Binding.full_name_spec on the spot;
|
file |
diff |
annotate
|
| Tue, 02 May 2023 10:30:03 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Fri, 14 Apr 2023 22:19:28 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 13 Apr 2023 23:08:39 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Mon, 02 Dec 2019 13:33:45 +0100 |
wenzelm |
more robust;
|
file |
diff |
annotate
|
| Fri, 09 Aug 2019 17:14:49 +0200 |
wenzelm |
formal position for PThm nodes;
|
file |
diff |
annotate
|
| Mon, 04 Jul 2016 11:11:19 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Thu, 23 Jun 2016 11:01:14 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Tue, 21 Jun 2016 10:41:29 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sun, 17 Apr 2016 22:38:50 +0200 |
wenzelm |
clarified bindings;
|
file |
diff |
annotate
|
| Sun, 17 Apr 2016 20:11:02 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Sat, 02 Apr 2016 21:10:07 +0200 |
wenzelm |
careful export of type-dependent functions, without losing their special status;
|
file |
diff |
annotate
|
| Fri, 18 Mar 2016 16:26:35 +0100 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Sun, 24 Jan 2016 15:02:56 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Mon, 28 Dec 2015 16:30:24 +0100 |
wenzelm |
suppress irrelevant position reports;
|
file |
diff |
annotate
|
| Sun, 20 Dec 2015 13:06:26 +0100 |
wenzelm |
renamed Pretty.str_of to Pretty.unformatted_string_of to emphasize its meaning;
|
file |
diff |
annotate
|
| Thu, 09 Apr 2015 20:42:32 +0200 |
wenzelm |
clarified keyword 'qualified' in accordance to a similar keyword from Haskell (despite unrelated Binding.qualified in Isabelle/ML);
|
file |
diff |
annotate
|
| Mon, 06 Apr 2015 22:11:01 +0200 |
wenzelm |
support for 'restricted' modifier: only qualified accesses outside the local scope;
|
file |
diff |
annotate
|
| Tue, 31 Mar 2015 22:31:05 +0200 |
wenzelm |
support for explicit scope of private entries;
|
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 11:16:55 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Tue, 31 Mar 2015 00:11:54 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Mon, 30 Mar 2015 22:34:59 +0200 |
wenzelm |
support for strictly private name space entries;
|
file |
diff |
annotate
|
| Fri, 22 Aug 2014 12:05:47 +0200 |
wenzelm |
clarified ML toplevel pp: avoid ML output to be attached to inlined binding positions;
|
file |
diff |
annotate
|
| Tue, 03 Sep 2013 19:58:00 +0200 |
wenzelm |
cases: formal binding of 'assumes', with position provided via invoke_case;
|
file |
diff |
annotate
|
| Mon, 26 Nov 2012 21:46:04 +0100 |
wenzelm |
tuned signature;
|
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, 29 Aug 2012 11:48:45 +0200 |
wenzelm |
renamed Position.str_of to Position.here;
|
file |
diff |
annotate
|
| Tue, 13 Mar 2012 12:51:52 +0100 |
wenzelm |
proper printing of empty binding (again, cf. 93f6f24010c2);
|
file |
diff |
annotate
|
| Mon, 28 Nov 2011 22:05:32 +0100 |
wenzelm |
separate module for concrete Isabelle markup;
|
file |
diff |
annotate
|
| Fri, 15 Jul 2011 13:28:16 +0200 |
wenzelm |
more robust Binding.pretty/print in typical error sitations with spaces etc. (NB: markup can only provide *additional* emphasis and is occasionally suppressed in TTY mode or tooltips);
|
file |
diff |
annotate
|
| Fri, 15 Jul 2011 00:49:38 +0200 |
wenzelm |
more visible printing of empty binding;
|
file |
diff |
annotate
|
| Sat, 25 Jun 2011 17:17:49 +0200 |
wenzelm |
clarified Binding.pretty/print: no quotes, only markup -- Binding.str_of is rendered obsolete;
|
file |
diff |
annotate
|
| Sat, 25 Jun 2011 15:08:58 +0200 |
wenzelm |
clarified Binding.str_of/print: show full prefix + qualifier, which is relevant for print_locale, for example;
|
file |
diff |
annotate
|
| Sun, 17 Apr 2011 21:42:47 +0200 |
wenzelm |
added Binding.print convenience, which includes quote already;
|
file |
diff |
annotate
|
| Fri, 17 Dec 2010 22:23:56 +0100 |
wenzelm |
extra checking of name bindings for classes, types, consts;
|
file |
diff |
annotate
|
| Fri, 17 Sep 2010 17:11:43 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 18 Feb 2010 20:46:46 +0100 |
wenzelm |
more systematic treatment of qualified names derived from binding;
|
file |
diff |
annotate
|
| Sun, 25 Oct 2009 12:27:21 +0100 |
wenzelm |
allow name space entries to be "concealed" -- via binding/naming/local_theory;
|
file |
diff |
annotate
|
| Wed, 16 Sep 2009 21:14:08 +0200 |
wenzelm |
replaced opaque signature matching by plain old abstype (again, cf. ac4498f95d1c) -- this recovers pretty printing in SML/NJ and Poly/ML 5.3;
|
file |
diff |
annotate
|
| Mon, 30 Mar 2009 19:51:10 +0200 |
wenzelm |
qualified_name_of: observe empty case;
|
file |
diff |
annotate
|
| Thu, 12 Mar 2009 11:07:22 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Tue, 10 Mar 2009 16:44:20 +0100 |
wenzelm |
added qualified_name_of;
|
file |
diff |
annotate
|
| Sun, 08 Mar 2009 17:03:07 +0100 |
wenzelm |
added qualified_name -- emulates old-style qualified bstring;
|
file |
diff |
annotate
|
| Sat, 07 Mar 2009 21:18:37 +0100 |
wenzelm |
added prefix_name, suffix_name;
|
file |
diff |
annotate
|
| Sat, 07 Mar 2009 11:32:31 +0100 |
wenzelm |
Binding.str_of: removed verbose feature, include qualifier in output;
|
file |
diff |
annotate
|
| Thu, 05 Mar 2009 10:52:07 +0100 |
wenzelm |
added prefix_of;
|
file |
diff |
annotate
|
| Wed, 04 Mar 2009 11:05:29 +0100 |
blanchet |
Merge.
|
file |
diff |
annotate
|
| Wed, 04 Mar 2009 10:45:52 +0100 |
blanchet |
Merge.
|
file |
diff |
annotate
|
| Tue, 03 Mar 2009 21:49:34 +0100 |
wenzelm |
tuned str_of, now subject to verbose flag;
|
file |
diff |
annotate
|
| Tue, 03 Mar 2009 18:31:59 +0100 |
wenzelm |
moved type bstring from name_space.ML to binding.ML -- it is the primitive concept behind bindings;
|
file |
diff |
annotate
|
| Tue, 03 Mar 2009 15:09:07 +0100 |
wenzelm |
renamed Binding.display to Binding.str_of, which is slightly more canonical;
|
file |
diff |
annotate
|
| Tue, 03 Mar 2009 14:52:13 +0100 |
wenzelm |
moved name space externalization flags back to name_space.ML;
|
file |
diff |
annotate
|
| Thu, 22 Jan 2009 11:23:15 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Wed, 21 Jan 2009 16:47:32 +0100 |
haftmann |
binding is alias for Binding.T
|
file |
diff |
annotate
|
| Sat, 03 Jan 2009 08:39:18 +0100 |
haftmann |
separator, is_qualified
|
file |
diff |
annotate
|