| Thu, 21 Aug 2014 10:07:06 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 19 Aug 2014 23:17:51 +0200 |
wenzelm |
tuned signature -- moved type src to Token, without aliases;
|
file |
diff |
annotate
|
| Thu, 14 Aug 2014 16:20:14 +0200 |
wenzelm |
more informative Token.Fact: retain name of dynamic fact (without selection);
|
file |
diff |
annotate
|
| Thu, 14 Aug 2014 14:28:11 +0200 |
wenzelm |
localized command 'method_setup' and 'attribute_setup';
|
file |
diff |
annotate
|
| Thu, 14 Aug 2014 12:33:21 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 14 Aug 2014 12:13:24 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 14 Aug 2014 11:55:09 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Wed, 13 Aug 2014 13:57:55 +0200 |
wenzelm |
localized attribute definitions;
|
file |
diff |
annotate
|
| 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
|
| Sun, 06 Apr 2014 16:36:28 +0200 |
wenzelm |
more source positions;
|
file |
diff |
annotate
|
| Sun, 06 Apr 2014 15:43:45 +0200 |
wenzelm |
more source positions;
|
file |
diff |
annotate
|
| Mon, 31 Mar 2014 12:35:39 +0200 |
wenzelm |
some shortcuts for chunks, which sometimes avoid bulky string output;
|
file |
diff |
annotate
|
| Thu, 27 Mar 2014 17:12:40 +0100 |
wenzelm |
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
|
file |
diff |
annotate
|
| Tue, 25 Mar 2014 19:03:02 +0100 |
wenzelm |
proper configuration option "ML_print_depth";
|
file |
diff |
annotate
|
| Tue, 25 Mar 2014 16:54:38 +0100 |
wenzelm |
clarified options ML_source_trace and ML_exception_trace (NB: the latter needs to be a system option, since the context is sometimes not available, e.g. for 'theory' command);
|
file |
diff |
annotate
|
| Tue, 25 Mar 2014 16:11:00 +0100 |
wenzelm |
separate tokenization and language context for SML: no symbols, no antiquotes;
|
file |
diff |
annotate
|
| Mon, 24 Mar 2014 12:00:17 +0100 |
wenzelm |
discontinued Toplevel.debug in favour of system option "exception_trace";
|
file |
diff |
annotate
|
| Fri, 14 Mar 2014 10:08:36 +0100 |
wenzelm |
just one cumulative Proof_Context.facts, with uniform retrieval (including PIDE markup, completion etc.);
|
file |
diff |
annotate
|
| Tue, 11 Mar 2014 14:28:39 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Mon, 10 Mar 2014 20:27:08 +0100 |
wenzelm |
more markup;
|
file |
diff |
annotate
|
| Mon, 10 Mar 2014 18:06:23 +0100 |
wenzelm |
clarified Args.check_src: retain name space information for error output;
|
file |
diff |
annotate
|
| Mon, 10 Mar 2014 16:30:07 +0100 |
wenzelm |
clarified Args.src: more abstract type, position refers to name only;
|
file |
diff |
annotate
|
| Mon, 10 Mar 2014 15:20:41 +0100 |
wenzelm |
prefer Name_Space.pretty with its builtin markup;
|
file |
diff |
annotate
|
| Mon, 10 Mar 2014 15:04:01 +0100 |
wenzelm |
tuned signature -- prefer Name_Space.get with its builtin error;
|
file |
diff |
annotate
|
| Mon, 10 Mar 2014 13:55:03 +0100 |
wenzelm |
abstract type Name_Space.table;
|
file |
diff |
annotate
|
| Sat, 08 Mar 2014 21:31:12 +0100 |
wenzelm |
keep current context visibility for PIDE markup and completion (in contrast to 8e3e004f1c31): Attrib.check_src of 9dc5ce83202c should intern/report attributes once, which happens for local_theory in the (visible) auxiliary context;
|
file |
diff |
annotate
|
| Sat, 08 Mar 2014 21:08:10 +0100 |
wenzelm |
modernized Attrib.check_name/check_src similar to methods (see also a989bdaf8121);
|
file |
diff |
annotate
|
| Wed, 05 Mar 2014 13:11:08 +0100 |
wenzelm |
clarified init_assignable: make double-sure that initial values are reset;
|
file |
diff |
annotate
|
| Sat, 01 Mar 2014 22:46:31 +0100 |
wenzelm |
clarified language markup: added "delimited" property;
|
file |
diff |
annotate
|
| Tue, 25 Feb 2014 11:36:04 +0100 |
wenzelm |
more positions;
|
file |
diff |
annotate
|
| Sat, 25 Jan 2014 18:18:03 +0100 |
wenzelm |
define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
|
file |
diff |
annotate
|
| Fri, 23 Aug 2013 20:35:50 +0200 |
wenzelm |
added Theory.setup convenience;
|
file |
diff |
annotate
|
| Fri, 23 Aug 2013 17:01:12 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Fri, 16 Aug 2013 22:39:31 +0200 |
wenzelm |
more markup via Name_Space.check;
|
file |
diff |
annotate
|
| Fri, 19 Jul 2013 17:35:12 +0200 |
wenzelm |
turned pattern unify flag into configuration option (global only);
|
file |
diff |
annotate
|
| Wed, 17 Jul 2013 11:38:57 +0200 |
wenzelm |
more official Thm.eq_thm_strict, without demanding ML equality type;
|
file |
diff |
annotate
|
| Sun, 30 Jun 2013 11:37:34 +0200 |
wenzelm |
backout dedd7952a62c: static "proofs" value within theory prevents later inferencing with different configuration;
|
file |
diff |
annotate
|
| Thu, 27 Jun 2013 23:17:26 +0200 |
wenzelm |
manage option "proofs" within theory context -- with minor overhead for primitive inferences;
|
file |
diff |
annotate
|
| Fri, 17 May 2013 20:53:28 +0200 |
wenzelm |
renamed 'print_configs' to 'print_options';
|
file |
diff |
annotate
|
| Fri, 17 May 2013 20:41:45 +0200 |
wenzelm |
proper option quick_and_dirty;
|
file |
diff |
annotate
|
| Thu, 16 May 2013 20:33:01 +0200 |
wenzelm |
system options as context-sensitive configuration options within the attribute name space;
|
file |
diff |
annotate
|
| Thu, 16 May 2013 19:41:41 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Mon, 11 Feb 2013 11:38:16 +0100 |
webertj |
Typo in description of abs_def.
|
file |
diff |
annotate
|
| Tue, 08 Jan 2013 16:23:07 +0100 |
wenzelm |
allow negative argument in "consumes" source format;
|
file |
diff |
annotate
|
| Fri, 30 Nov 2012 22:38:06 +0100 |
wenzelm |
print formal entities with markup;
|
file |
diff |
annotate
|
| Sat, 29 Sep 2012 16:17:46 +0200 |
wenzelm |
turn constraints into Isabelle_Markup.typing, depending on show_markup options;
|
file |
diff |
annotate
|
| Wed, 29 Aug 2012 11:48:45 +0200 |
wenzelm |
renamed Position.str_of to Position.here;
|
file |
diff |
annotate
|
| Fri, 06 Jul 2012 16:20:54 +0200 |
wenzelm |
discontinued obsolete attribute "COMP";
|
file |
diff |
annotate
|
| Fri, 27 Apr 2012 22:58:29 +0200 |
wenzelm |
prefer Context_Position.report_generic, which observes is_visible flag and thus reduces number of echos;
|
file |
diff |
annotate
|
| Fri, 27 Apr 2012 22:47:30 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Sun, 01 Apr 2012 19:07:32 +0200 |
wenzelm |
added Attrib.global_notes/local_notes/generic_notes convenience;
|
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
|
| Tue, 13 Mar 2012 17:04:00 +0100 |
wenzelm |
suppress vacous notes elements, with subtle change of semantics: 'interpret' no longer pulls-in unnamed facts "by fact";
|
file |
diff |
annotate
|
| Tue, 13 Mar 2012 16:22:18 +0100 |
wenzelm |
improved attribute "abs_def" to handle object-equality as well;
|
file |
diff |
annotate
|
| Sat, 03 Mar 2012 21:43:59 +0100 |
wenzelm |
canonical argument order for attribute application;
|
file |
diff |
annotate
|
| Fri, 17 Feb 2012 15:42:26 +0100 |
wenzelm |
simplified configuration options for syntax ambiguity;
|
file |
diff |
annotate
|
| Thu, 16 Feb 2012 22:18:28 +0100 |
wenzelm |
simplified configuration options for syntax ambiguity;
|
file |
diff |
annotate
|
| Thu, 05 Jan 2012 20:26:01 +0100 |
wenzelm |
discontinued Syntax.positions -- atomic parse trees are always annotated;
|
file |
diff |
annotate
|
| Wed, 23 Nov 2011 22:07:55 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Mon, 21 Nov 2011 23:03:31 +0100 |
wenzelm |
drop vacuous decls;
|
file |
diff |
annotate
|