| Fri, 27 Jul 2012 22:26:38 +0200 |
haftmann |
evaluation: allow multiple code modules
|
file |
diff |
annotate
|
| Sat, 21 Jul 2012 20:01:16 +0200 |
haftmann |
also consider current working directory (cf. 3a5a5a992519)
|
file |
diff |
annotate
|
| Thu, 19 Jul 2012 22:21:59 +0200 |
haftmann |
export code relatively to master directory
|
file |
diff |
annotate
|
| Thu, 19 Apr 2012 10:16:51 +0200 |
haftmann |
dropped dead code;
|
file |
diff |
annotate
|
| Fri, 23 Mar 2012 20:32:43 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 16 Mar 2012 18:20:12 +0100 |
wenzelm |
outer syntax command definitions based on formal command_spec derived from theory header declarations;
|
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
|
| Thu, 23 Feb 2012 15:49:40 +0100 |
wenzelm |
clarified Graph.restrict (formerly Graph.subgraph) based on public graph operations;
|
file |
diff |
annotate
|
| Tue, 06 Sep 2011 16:40:22 +0200 |
bulwahn |
avoid "Code" as structure name (cf. 3bc39cfe27fe)
|
file |
diff |
annotate
|
| Sat, 16 Jul 2011 20:52:41 +0200 |
wenzelm |
moved bash operations to Isabelle_System (cf. Scala version);
|
file |
diff |
annotate
|
| Mon, 27 Jun 2011 22:20:49 +0200 |
wenzelm |
document antiquotations are managed as theory data, with proper name space and entity markup;
|
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, 16 Apr 2011 16:15:37 +0200 |
wenzelm |
modernized structure Proof_Context;
|
file |
diff |
annotate
|
| Sat, 16 Apr 2011 15:25:25 +0200 |
wenzelm |
prefer local name spaces;
|
file |
diff |
annotate
|
| Sun, 13 Mar 2011 14:51:38 +0100 |
wenzelm |
allow spaces in executable names;
|
file |
diff |
annotate
|
| Sun, 13 Mar 2011 13:57:20 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 21 Dec 2010 15:15:55 +0100 |
haftmann |
tuned names
|
file |
diff |
annotate
|
| Tue, 21 Dec 2010 10:20:33 +0100 |
haftmann |
only depend on exisiting statements
|
file |
diff |
annotate
|
| Tue, 21 Dec 2010 08:40:39 +0100 |
haftmann |
evaluator separating static and dynamic operations
|
file |
diff |
annotate
|
| Tue, 21 Dec 2010 07:45:04 +0100 |
haftmann |
more explicit structure for serializer invocation
|
file |
diff |
annotate
|
| Mon, 20 Dec 2010 14:44:00 +0100 |
wenzelm |
slightly more standard Isabelle_System.with_tmp_file/with_tmp_dir (cf. Scala version);
|
file |
diff |
annotate
|
| Fri, 01 Oct 2010 11:46:09 +0200 |
haftmann |
check whole target hierarchy for existing reserved symbols
|
file |
diff |
annotate
|
| Tue, 28 Sep 2010 09:14:37 +0200 |
haftmann |
consider quick_and_dirty option before loading theory
|
file |
diff |
annotate
|
| Fri, 24 Sep 2010 14:03:44 +0200 |
haftmann |
dropped dead code
|
file |
diff |
annotate
|
| Thu, 23 Sep 2010 13:23:22 +0200 |
haftmann |
reverted cs 07549694e2f1 -- use re-printing with current print mode instead after code assembly, avoid Latex.output_typewriter
|
file |
diff |
annotate
|
| Thu, 23 Sep 2010 11:29:22 +0200 |
haftmann |
shifted abstraction over imperative print mode
|
file |
diff |
annotate
|
| Thu, 23 Sep 2010 10:37:28 +0200 |
haftmann |
improved and tuned external codegen tool
|
file |
diff |
annotate
|
| Fri, 17 Sep 2010 09:21:49 +0200 |
haftmann |
closures separate serializer initialization from serializer invocation as far as appropriate
|
file |
diff |
annotate
|
| Thu, 16 Sep 2010 17:31:51 +0200 |
haftmann |
added code_stmts antiquotation from doc-src/more_antiquote.ML
|
file |
diff |
annotate
|
| Sat, 04 Sep 2010 21:10:48 +0200 |
haftmann |
dropped names from serializer interface
|
file |
diff |
annotate
|
| Thu, 02 Sep 2010 19:08:48 +0200 |
haftmann |
hand out deresolver from serializer invocation
|
file |
diff |
annotate
|
| Thu, 02 Sep 2010 14:59:28 +0200 |
haftmann |
dropped superfluous presentation names
|
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 12:30:22 +0200 |
haftmann |
formal framework for presentation of selected statements
|
file |
diff |
annotate
|
| Tue, 31 Aug 2010 19:14:18 +0200 |
haftmann |
repaired casual accident; tuned names
|
file |
diff |
annotate
|
| Tue, 31 Aug 2010 16:51:29 +0200 |
haftmann |
avoid strange special treatment of empty module names
|
file |
diff |
annotate
|
| Tue, 31 Aug 2010 15:21:42 +0200 |
haftmann |
distinguish code production and code presentation
|
file |
diff |
annotate
|
| Tue, 31 Aug 2010 15:08:04 +0200 |
haftmann |
dropped single_module parameter
|
file |
diff |
annotate
|
| Tue, 31 Aug 2010 14:43:27 +0200 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Tue, 31 Aug 2010 14:21:06 +0200 |
haftmann |
record argument for serializers
|
file |
diff |
annotate
|
| Tue, 31 Aug 2010 14:06:20 +0200 |
haftmann |
tuned serializer argument interface
|
file |
diff |
annotate
|
| Tue, 31 Aug 2010 13:55:54 +0200 |
haftmann |
removed serializer interface redundancies
|
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:08:58 +0200 |
haftmann |
dropped legacy interfaces
|
file |
diff |
annotate
|
| Mon, 30 Aug 2010 17:20:33 +0200 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Mon, 30 Aug 2010 16:42:54 +0200 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Mon, 30 Aug 2010 16:33:06 +0200 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Mon, 30 Aug 2010 16:25:04 +0200 |
haftmann |
tuned file interface
|
file |
diff |
annotate
|
| Mon, 30 Aug 2010 16:21:47 +0200 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Mon, 30 Aug 2010 16:17:10 +0200 |
haftmann |
eliminated some obscure higher-order arguments
|
file |
diff |
annotate
|
| Mon, 30 Aug 2010 16:00:41 +0200 |
haftmann |
width is a formal parameter of serialization
|
file |
diff |
annotate
|
| Mon, 30 Aug 2010 15:01:32 +0200 |
haftmann |
whitespace tuning
|
file |
diff |
annotate
|
| Mon, 30 Aug 2010 14:48:25 +0200 |
haftmann |
tuned comment
|
file |
diff |
annotate
|
| Mon, 30 Aug 2010 09:28:02 +0200 |
haftmann |
code checking: compiler invocation happens in same directory as generated file -- avoid problem with different path representations on cygwin
|
file |
diff |
annotate
|
| Thu, 26 Aug 2010 20:14:24 +0200 |
haftmann |
proper passing of optional module name
|
file |
diff |
annotate
|
| Thu, 26 Aug 2010 13:50:58 +0200 |
haftmann |
tuned serializer interface
|
file |
diff |
annotate
|
| Mon, 26 Jul 2010 11:15:10 +0200 |
haftmann |
restored unusual snd-biased merge/join policy -- required due to non-conservative code setups
|
file |
diff |
annotate
|
| Wed, 21 Jul 2010 16:50:42 +0200 |
wenzelm |
merged
|
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
|
| Tue, 20 Jul 2010 23:09:49 +0200 |
wenzelm |
discontinued pervasive val theory = Thy_Info.get_theory -- prefer antiquotations in most situations;
|
file |
diff |
annotate
|
| Fri, 16 Jul 2010 14:11:08 +0200 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Fri, 16 Jul 2010 13:57:29 +0200 |
haftmann |
restored long-broken syntax sanity checks
|
file |
diff |
annotate
|
| Wed, 14 Jul 2010 16:02:50 +0200 |
haftmann |
explicit optional checking
|
file |
diff |
annotate
|
| Wed, 14 Jul 2010 15:49:29 +0200 |
haftmann |
added Isar syntax for code checking
|
file |
diff |
annotate
|
| Wed, 14 Jul 2010 15:08:02 +0200 |
haftmann |
use generic description slot for formal code checking
|
file |
diff |
annotate
|
| Wed, 14 Jul 2010 14:53:44 +0200 |
haftmann |
formal slot for code checker
|
file |
diff |
annotate
|
| Wed, 14 Jul 2010 14:20:47 +0200 |
haftmann |
check without explicit path
|
file |
diff |
annotate
|
| Wed, 14 Jul 2010 09:42:44 +0200 |
haftmann |
redirect stderr to stdout
|
file |
diff |
annotate
|
| Thu, 08 Jul 2010 16:41:57 +0200 |
haftmann |
dropped ancient in-place compilation of SML
|
file |
diff |
annotate
|
| Thu, 08 Jul 2010 16:19:24 +0200 |
haftmann |
checking generated code for various target languages
|
file |
diff |
annotate
|
| Thu, 24 Jun 2010 14:31:01 +0200 |
wenzelm |
slightly more standard data merge: Symtax.merge (K true) avoids equality on abstract type Pretty.T and gracefully accepts overriding, Symtab.join prefers first entry as usual;
|
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
|
| Thu, 29 Apr 2010 15:00:43 +0200 |
haftmann |
repaired subtle misunderstanding: statement names are only passed for name resolution
|
file |
diff |
annotate
|
| Wed, 28 Apr 2010 15:17:13 +0200 |
haftmann |
exported cert_tyco, read_tyco
|
file |
diff |
annotate
|
| Wed, 21 Apr 2010 15:20:57 +0200 |
haftmann |
optionally ignore errors during translation of equations
|
file |
diff |
annotate
|
| Tue, 13 Apr 2010 11:13:52 +0200 |
haftmann |
dropped dead code
|
file |
diff |
annotate
|
| Mon, 04 Jan 2010 14:09:58 +0100 |
haftmann |
modernized
|
file |
diff |
annotate
|
| Wed, 23 Dec 2009 08:31:15 +0100 |
haftmann |
reduced code generator cache to the baremost minimum
|
file |
diff |
annotate
|
| Mon, 21 Dec 2009 08:32:04 +0100 |
haftmann |
clarified various user-defined syntax issues
|
file |
diff |
annotate
|
| Mon, 14 Dec 2009 10:13:06 +0100 |
haftmann |
made sml/nj happy
|
file |
diff |
annotate
|
| Fri, 11 Dec 2009 20:32:49 +0100 |
haftmann |
default_code_width is now proper theory data
|
file |
diff |
annotate
|
| Mon, 07 Dec 2009 11:48:40 +0100 |
haftmann |
tuned inner structure
|
file |
diff |
annotate
|
| Mon, 30 Nov 2009 12:28:12 +0100 |
haftmann |
dropped some unused bindings
|
file |
diff |
annotate
|
| Sun, 08 Nov 2009 18:43:42 +0100 |
wenzelm |
adapted Theory_Data;
|
file |
diff |
annotate
|
| Sat, 17 Oct 2009 15:57:51 +0200 |
wenzelm |
indicate CRITICAL nature of various setmp combinators;
|
file |
diff |
annotate
|
| Thu, 08 Oct 2009 15:59:16 +0200 |
haftmann |
moved labelled_name to code_thingol
|
file |
diff |
annotate
|
| Tue, 29 Sep 2009 16:24:36 +0200 |
wenzelm |
explicit indication of Unsynchronized.ref;
|
file |
diff |
annotate
|
| Tue, 07 Jul 2009 17:21:27 +0200 |
haftmann |
tuned interface of structure Code
|
file |
diff |
annotate
|
| Tue, 23 Jun 2009 12:09:30 +0200 |
haftmann |
uniformly capitialized names for subdirectories
|
file |
diff |
annotate
| base
|