| Thu, 19 Apr 2012 10:16:51 +0200 |
haftmann |
dropped dead code;
|
file |
diff |
annotate
|
| Thu, 15 Mar 2012 20:07:00 +0100 |
wenzelm |
prefer formally checked @{keyword} parser;
|
file |
diff |
annotate
|
| Thu, 15 Mar 2012 19:02:34 +0100 |
wenzelm |
declare minor keywords via theory header;
|
file |
diff |
annotate
|
| Tue, 20 Sep 2011 09:30:19 +0200 |
bulwahn |
syntactic improvements and tuning names in the code generator due to Florian's code review
|
file |
diff |
annotate
|
| Wed, 07 Sep 2011 13:51:32 +0200 |
bulwahn |
adding the body type as well to the code generation for constants as it is required for type annotations of constants
|
file |
diff |
annotate
|
| Wed, 07 Sep 2011 13:51:30 +0200 |
bulwahn |
changing const type to pass along if typing annotations are necessary for disambigous terms
|
file |
diff |
annotate
|
| Sat, 23 Jul 2011 16:37:17 +0200 |
wenzelm |
defer evaluation of Scan.message, for improved performance in the frequent situation where failure is handled later (e.g. via ||);
|
file |
diff |
annotate
|
| Thu, 09 Jun 2011 17:51:49 +0200 |
wenzelm |
simplified Name.variant -- discontinued builtin fold_map;
|
file |
diff |
annotate
|
| Thu, 09 Jun 2011 16:34:49 +0200 |
wenzelm |
discontinued Name.variant to emphasize that this is old-style / indirect;
|
file |
diff |
annotate
|
| Sat, 20 Nov 2010 00:53:26 +0100 |
wenzelm |
renamed raw "explode" function to "raw_explode" to emphasize its meaning;
|
file |
diff |
annotate
|
| Fri, 24 Sep 2010 14:03:44 +0200 |
haftmann |
always add trailing newline for presentation
|
file |
diff |
annotate
|
| Thu, 23 Sep 2010 13:23:21 +0200 |
haftmann |
reverted cs 07549694e2f1
|
file |
diff |
annotate
|
| Thu, 23 Sep 2010 11:29:22 +0200 |
haftmann |
shifted abstraction over imperative print mode
|
file |
diff |
annotate
|
| Mon, 20 Sep 2010 14:36:54 +0200 |
haftmann |
use buffers instead of string concatenation
|
file |
diff |
annotate
|
| Fri, 17 Sep 2010 17:17:56 +0200 |
haftmann |
less intermediate data structures
|
file |
diff |
annotate
|
| Thu, 02 Sep 2010 16:53:23 +0200 |
haftmann |
set printmode while marking
|
file |
diff |
annotate
|
| Thu, 02 Sep 2010 16:14:13 +0200 |
haftmann |
corrected printmode handling
|
file |
diff |
annotate
|
| Thu, 02 Sep 2010 14:36:49 +0200 |
haftmann |
manage statement selection for presentation wholly through markup
|
file |
diff |
annotate
|
| Thu, 02 Sep 2010 13:58:16 +0200 |
haftmann |
formal markup of generated code for statements
|
file |
diff |
annotate
|
| Thu, 02 Sep 2010 13:43:38 +0200 |
haftmann |
removed namespace stuff from code_printer
|
file |
diff |
annotate
|
| Thu, 02 Sep 2010 12:30:22 +0200 |
haftmann |
formal framework for presentation of selected statements
|
file |
diff |
annotate
|
| Tue, 31 Aug 2010 13:29:38 +0200 |
haftmann |
more coherent naming of syntax data structures
|
file |
diff |
annotate
|
| Tue, 31 Aug 2010 13:15:35 +0200 |
haftmann |
Code_Printer.tuplify
|
file |
diff |
annotate
|
| Mon, 30 Aug 2010 16:11:09 +0200 |
haftmann |
trailing newline by default
|
file |
diff |
annotate
|
| Thu, 26 Aug 2010 12:30:43 +0200 |
haftmann |
private version of commas, cf. printmode
|
file |
diff |
annotate
|
| Sat, 24 Jul 2010 18:08:41 +0200 |
haftmann |
another refinement chapter in the neverending numeral story
|
file |
diff |
annotate
|
| Wed, 21 Jul 2010 17:46:36 +0200 |
wenzelm |
made SML/NJ happy;
|
file |
diff |
annotate
|
| Mon, 19 Jul 2010 11:55:44 +0200 |
haftmann |
distinguish different classes of const syntax
|
file |
diff |
annotate
|
| Fri, 16 Jul 2010 15:55:32 +0200 |
haftmann |
consolidate const_syntax naming
|
file |
diff |
annotate
|
| Thu, 08 Jul 2010 16:19:24 +0200 |
haftmann |
tuned titles
|
file |
diff |
annotate
|
| Wed, 30 Jun 2010 11:38:51 +0200 |
haftmann |
explicit printing function for applify
|
file |
diff |
annotate
|
| Thu, 17 Jun 2010 15:59:47 +0200 |
haftmann |
more precise code
|
file |
diff |
annotate
|
| Tue, 01 Jun 2010 13:52:11 +0200 |
haftmann |
brackify_infix etc.: no break before infix operator -- eases survival in Scala
|
file |
diff |
annotate
|
| Thu, 27 May 2010 18:10:37 +0200 |
wenzelm |
renamed structure PrintMode to Print_Mode, keeping the old name as legacy alias for some time;
|
file |
diff |
annotate
|
| Mon, 17 May 2010 23:54:15 +0200 |
wenzelm |
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
|
file |
diff |
annotate
|
| Mon, 17 May 2010 15:11:25 +0200 |
wenzelm |
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
|
file |
diff |
annotate
|
| Sat, 08 May 2010 19:14:13 +0200 |
wenzelm |
unified/simplified Pretty.margin_default;
|
file |
diff |
annotate
|
| Fri, 19 Feb 2010 11:06:22 +0100 |
haftmann |
context theorem is optional
|
file |
diff |
annotate
|
| Fri, 22 Jan 2010 13:38:28 +0100 |
haftmann |
code literals: distinguish numeral classes by different entries
|
file |
diff |
annotate
|
| Mon, 04 Jan 2010 14:09:57 +0100 |
haftmann |
added applify combinator
|
file |
diff |
annotate
|
| Wed, 23 Dec 2009 11:32:08 +0100 |
haftmann |
take care for destructive print mode properly using dedicated pretty builders
|
file |
diff |
annotate
|
| Wed, 23 Dec 2009 10:09:06 +0100 |
haftmann |
made sml/nj happy
|
file |
diff |
annotate
|
| Mon, 21 Dec 2009 08:32:04 +0100 |
haftmann |
clarified various user-defined syntax issues
|
file |
diff |
annotate
|
| Fri, 11 Dec 2009 20:32:49 +0100 |
haftmann |
default_code_width is now proper theory data
|
file |
diff |
annotate
|
| Fri, 04 Dec 2009 18:51:15 +0100 |
haftmann |
merged, resolving minor conflicts
|
file |
diff |
annotate
|
| Fri, 04 Dec 2009 18:19:31 +0100 |
haftmann |
more speaking function names for Code_Printer; added doublesemicolon
|
file |
diff |
annotate
|
| Wed, 25 Nov 2009 09:13:46 +0100 |
haftmann |
normalized uncurry take/drop
|
file |
diff |
annotate
|
| Tue, 24 Nov 2009 17:28:25 +0100 |
haftmann |
curried take/drop
|
file |
diff |
annotate
|
| Wed, 14 Oct 2009 11:56:44 +0200 |
haftmann |
dropped Code_Printer prefix where feasible; fixed whitespace issues; more coherent terminology
|
file |
diff |
annotate
|
| Mon, 12 Oct 2009 15:46:38 +0200 |
haftmann |
intro_base_names combinator
|
file |
diff |
annotate
|
| Mon, 12 Oct 2009 12:19:19 +0200 |
haftmann |
factored out Code_Printer.aux_params
|
file |
diff |
annotate
|
| Tue, 21 Jul 2009 01:03:18 +0200 |
wenzelm |
proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
|
file |
diff |
annotate
|
| Tue, 30 Jun 2009 17:33:30 +0200 |
haftmann |
all variable names are optional
|
file |
diff |
annotate
|
| Tue, 30 Jun 2009 14:54:00 +0200 |
haftmann |
simplified binding concept
|
file |
diff |
annotate
|
| Tue, 23 Jun 2009 12:09:30 +0200 |
haftmann |
uniformly capitialized names for subdirectories
|
file |
diff |
annotate
| base
|