| #
4be542d9 |
|
01-Nov-2019 |
wenzelm <none@none> |
more scalable protocol_message: use XML.body directly (Output.output hook is not required);
|
| #
eb845a5f |
|
01-Apr-2019 |
wenzelm <none@none> |
tuned signature -- more exports;
|
| #
886a0067 |
|
30-Mar-2019 |
wenzelm <none@none> |
clarified signature: more explicit type Path.binding;
tuned;
|
| #
65ba4fbe |
|
29-Mar-2019 |
wenzelm <none@none> |
clarified 'file_prefix';
|
| #
ab0f6a9e |
|
28-Mar-2019 |
wenzelm <none@none> |
"export_code ... file_prefix ..." is the preferred way to produce output within the logical file-system within the theory context, as well as session exports;
"export_code ... file" is legacy, the empty name form has been discontinued;
updated examples;
|
| #
ddfa9f13 |
|
27-Mar-2019 |
wenzelm <none@none> |
proper local_theory command;
|
| #
7ba3c569 |
|
27-Mar-2019 |
wenzelm <none@none> |
more exports: avoid clones in AFP;
|
| #
ef9a579f |
|
27-Mar-2019 |
wenzelm <none@none> |
tuned;
|
| #
50eeaed0 |
|
27-Mar-2019 |
wenzelm <none@none> |
export_code/check_code formally updates the theory -- this opens further possibilities concerning Generated_Files;
tuned;
|
| #
3fbfd2a8 |
|
27-Mar-2019 |
wenzelm <none@none> |
tuned whitespace;
|
| #
a7c0e049 |
|
10-Mar-2019 |
haftmann <none@none> |
migrated from Nums to Zarith as library for OCaml integer arithmetic
--HG--
extra : rebase_source : 9da06716fa2cece20a04b2b74f042738c493e925
|
| #
7d8b7f49 |
|
02-Feb-2019 |
wenzelm <none@none> |
clarified signature: Path.T as in Generated_Files;
|
| #
dc79acad |
|
20-Jan-2019 |
haftmann <none@none> |
more conventional parsing of code_stmts antiquotation
--HG--
extra : rebase_source : 0cfb57d371901119b7774dbc79e8538a154bf03b
|
| #
a604f003 |
|
20-Jan-2019 |
haftmann <none@none> |
more conventional syntax for code_stmts antiquotation
--HG--
extra : rebase_source : bf1bb583f809bdfe860be5f44d3b5adf3f1d5390
|
| #
6893d5d3 |
|
14-Jan-2019 |
haftmann <none@none> |
canonical operation to typeset generated code makes dedicated environment obsolete
|
| #
048cf2a1 |
|
14-Jan-2019 |
wenzelm <none@none> |
clarified message;
|
| #
91df1ff7 |
|
13-Jan-2019 |
wenzelm <none@none> |
information with hyperlink to "isabelle-export:";
|
| #
6f48ebb9 |
|
13-Jan-2019 |
wenzelm <none@none> |
regular export with implicit compression: result is uncompressed;
|
| #
beffc0d0 |
|
13-Jan-2019 |
wenzelm <none@none> |
clarified -- removed pointless Parse.!!!;
|
| #
ea8a815a |
|
13-Jan-2019 |
wenzelm <none@none> |
tuned;
|
| #
0385a954 |
|
09-Jan-2019 |
haftmann <none@none> |
optional code export as theory export
|
| #
28b11dd3 |
|
09-Jan-2019 |
haftmann <none@none> |
explicit model concerning files of generated code
|
| #
a4bab154 |
|
04-Jan-2019 |
wenzelm <none@none> |
isabelle update -u control_cartouches;
|
| #
113328b7 |
|
29-Dec-2018 |
haftmann <none@none> |
more correct handling of symbols for includes
|
| #
43c8f19f |
|
19-Dec-2018 |
haftmann <none@none> |
proper attach mechanism for any kind of symbols, not just constants
--HG--
extra : rebase_source : 9d1fff48a7bf9ad88ee680634b8d508587fd59e6
|
| #
3940c305 |
|
19-Dec-2018 |
haftmann <none@none> |
disregard historic keyword
--HG--
extra : rebase_source : 5bd74dadc28a69241a93011615a90a30eb33f013
|
| #
0bcb05ae |
|
18-Jan-2018 |
wenzelm <none@none> |
clarified access to antiquotation options;
define explicit variants of antiquotations;
output proper Latex.text;
misc tuning and clarification;
|
| #
0ce84d08 |
|
09-Jan-2018 |
wenzelm <none@none> |
clarified modules;
|
| #
515bdf02 |
|
14-Dec-2017 |
haftmann <none@none> |
dedicated case option for code generation to Scala
--HG--
extra : rebase_source : f4d2da47982250c33b66f81d009da3f3d0b48bbd
|
| #
7f195800 |
|
31-Aug-2017 |
wenzelm <none@none> |
more PIDE markup;
|
| #
ff87130f |
|
27-Jan-2017 |
haftmann <none@none> |
ML antiquotation for generated computations
|
| #
9c2a5aeb |
|
26-Jan-2017 |
haftmann <none@none> |
tuned structure and terminology
--HG--
extra : rebase_source : 6302be51f0fe04b147a05d82b816c7a5aa4023ea
|
| #
e1b5cf61 |
|
26-May-2016 |
haftmann <none@none> |
optional timing for code generator conversions
|
| #
eec6cf97 |
|
26-May-2016 |
haftmann <none@none> |
clarified proof context vs. background theory
|
| #
10135f7d |
|
26-May-2016 |
haftmann <none@none> |
clarified naming conventions and code for code evaluation sandwiches
|
| #
1c0ca99b |
|
18-Apr-2016 |
haftmann <none@none> |
environment variable check has become pointless after 771b8ad5c7fc
--HG--
extra : rebase_source : 0725d5a5ce69e28d0ecbf0059e71f11525dc4521
|
| #
5dc803d8 |
|
13-Apr-2016 |
wenzelm <none@none> |
eliminated "xname" and variants;
|
| #
602a837c |
|
07-Mar-2016 |
wenzelm <none@none> |
tuned -- more standard operations;
|
| #
64ed947a |
|
07-Mar-2016 |
wenzelm <none@none> |
File.bash_string operations in ML as in Scala -- exclusively for GNU bash, not perl and not user output;
clarified treatment of whitespace in some bash scripts;
|
| #
4aa541f4 |
|
06-Apr-2015 |
wenzelm <none@none> |
@{command_spec} is superseded by @{command_keyword};
|
| #
8db7b8ac |
|
05-Feb-2015 |
haftmann <none@none> |
dropped obsolete external entrance point
|
| #
b4dc4d1c |
|
05-Feb-2015 |
haftmann <none@none> |
explicit error message for non-existing targets
|
| #
e6e7d73b |
|
24-Jan-2015 |
wenzelm <none@none> |
more direct Output.output;
avoid newline in Code_Printer/Pretty.str;
|
| #
8bc79546 |
|
09-Jan-2015 |
haftmann <none@none> |
prefer option for default code printing width
|
| #
0285f5b6 |
|
09-Jan-2015 |
haftmann <none@none> |
modernized and more uniform style
|
| #
0976a200 |
|
05-Dec-2014 |
haftmann <none@none> |
allow multiple inheritance of targets
--HG--
extra : rebase_source : 9d4980222d189226728427249e77a98373cb2011
|
| #
73336c34 |
|
04-Dec-2014 |
haftmann <none@none> |
tuned module structure
--HG--
extra : rebase_source : b00d44336a4cb5c02019294cc42c69ea8a448e6c
|
| #
9bc1e70f |
|
04-Dec-2014 |
haftmann <none@none> |
tuned data structures
--HG--
extra : rebase_source : 8bfb5e36479c2fea3adf854d18d5a388beeee3d7
|
| #
62b4ee76 |
|
04-Dec-2014 |
haftmann <none@none> |
tuned target inheritance bookkeeping: ancestry is always fully maintained at current entry using canonical merge;
n. b. merging of bidirectional dependencies results in effective join of involved nodes: no termination problem since ancestry is always kept explicitly normalized
--HG--
extra : rebase_source : 0194b074985fcbe9c611e2760285f884ec01db40
|
| #
7d5476ed |
|
04-Dec-2014 |
haftmann <none@none> |
tuned
--HG--
extra : rebase_source : 402db6db732a4e97e8347a780b30ce2fe1dc60d6
|
| #
35714a94 |
|
04-Dec-2014 |
haftmann <none@none> |
tuned names
--HG--
extra : rebase_source : b4bd4636d2b1583e1d7907ec9ccb917b4b1f0079
|
| #
91c3d5c1 |
|
03-Dec-2014 |
wenzelm <none@none> |
tuned signature;
|
| #
13ddea91 |
|
26-Nov-2014 |
wenzelm <none@none> |
renamed "pairself" to "apply2", in accordance to @{apply 2};
|
| #
c12ca051 |
|
07-Nov-2014 |
wenzelm <none@none> |
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
plain value Outer_Syntax within theory: parsing requires current theory context;
clarified name of Keyword.is_literal according to its semantics;
eliminated pointless type Keyword.T;
simplified @{command_spec};
clarified bootstrap keywords and syntax: take it as basis instead of side-branch;
|
| #
df4ccf3c |
|
05-Nov-2014 |
wenzelm <none@none> |
explicit type Keyword.keywords;
tuned signature;
|
| #
0da05f9f |
|
12-Aug-2014 |
wenzelm <none@none> |
tuned signature according to Scala version -- prefer explicit argument;
|
| #
71712946 |
|
12-Jun-2014 |
haftmann <none@none> |
formal variable name: IVar NONE is strictly spoken not supported on lhs of function definitions, e.g. in Scala
--HG--
extra : rebase_source : 5acb320209b0df291fe746e719728d8de1647e38
|
| #
89defae1 |
|
09-May-2014 |
haftmann <none@none> |
normalizing of type variables before evaluation with explicit resubstitution function: make nbe work with funny type variables like \<AA>;
tuned naming;
dropped dead parameters;
|
| #
b7f1a757 |
|
02-May-2014 |
haftmann <none@none> |
enforce case of identifiers only to accomodate strict language requirements (or clear separation of constructors from variables in the case of SML)
|
| #
9e3bb39c |
|
01-May-2014 |
haftmann <none@none> |
optional case enforcement
--HG--
extra : rebase_source : 9cdeaf7fca2e9c8512cef2a7a8af271ea0daed50
|
| #
7216e79c |
|
18-Mar-2014 |
wenzelm <none@none> |
clarifed module name;
--HG--
rename : src/Pure/Thy/thy_load.ML => src/Pure/PIDE/resources.ML
rename : src/Pure/Thy/thy_load.scala => src/Pure/PIDE/resources.scala
rename : src/Tools/jEdit/src/jedit_thy_load.scala => src/Tools/jEdit/src/jedit_resources.scala
|
| #
e50a7cf7 |
|
18-Mar-2014 |
wenzelm <none@none> |
tuned signature;
|
| #
3cb75ce2 |
|
09-Mar-2014 |
wenzelm <none@none> |
tuned signature;
|
| #
8decd8eb |
|
05-Mar-2014 |
wenzelm <none@none> |
tuned signature -- more uniform check_type_name/read_type_name;
proper reports for read_type_name (lost in 710bc66f432c);
|
| #
32a521c9 |
|
27-Feb-2014 |
haftmann <none@none> |
amended some slips, rolling back currently dysfunctional export minimimalisation for Scala
|
| #
e41a1507 |
|
26-Feb-2014 |
haftmann <none@none> |
prefer proof context over background theory
--HG--
extra : rebase_source : 307a2e54d5c0b89d8668ce99110df0538037668e
|
| #
217fdae1 |
|
23-Feb-2014 |
haftmann <none@none> |
keep only identifiers public which are explicitly requested or demanded by dependencies
|
| #
34a077b1 |
|
23-Feb-2014 |
haftmann <none@none> |
explicit option for "open" code generation
|
| #
f0637e3a |
|
09-Feb-2014 |
haftmann <none@none> |
dropped legacy finally
--HG--
extra : rebase_source : cc3d5b4eeefa467c96b4dd3e4a72a54b2c6b9f95
|
| #
b69fbd39 |
|
03-Feb-2014 |
wenzelm <none@none> |
more formal markup;
|
| #
42be5f7b |
|
03-Feb-2014 |
haftmann <none@none> |
tuned storage of code identifiers
--HG--
extra : rebase_source : 5e8c0cecdbf2a71e0bc8ffc2a3b7931aa243bfc5
|
| #
a3f9e497 |
|
30-Jan-2014 |
haftmann <none@none> |
reduced prominence of "permissive code generation"
--HG--
extra : rebase_source : 6e3c6c0e5bf55230da69faeeef775ffe97198728
|
| #
463293a2 |
|
26-Jan-2014 |
haftmann <none@none> |
more suitable names, without any notion of "activating"
|
| #
07ad0bb4 |
|
25-Jan-2014 |
haftmann <none@none> |
less clumsy namespace
|
| #
a01d18e2 |
|
25-Jan-2014 |
haftmann <none@none> |
immediate "activation" of const syntax at declaration time
|
| #
9250249f |
|
25-Jan-2014 |
haftmann <none@none> |
prefer explicit code symbol type over ad-hoc name mangling
|
| #
ecf8fa5d |
|
25-Jan-2014 |
haftmann <none@none> |
more abstract syntax passing
|
| #
6b54c1db |
|
11-Jan-2014 |
haftmann <none@none> |
dropped legacy alias feature
|
| #
e93b90ff |
|
31-Dec-2013 |
haftmann <none@none> |
fundamental treatment of undefined vs. universally partial replaces code_abort
|
| #
befed50f |
|
31-Dec-2013 |
haftmann <none@none> |
explicit distinction between empty code equations and no code equations, including convenient declaration attributes
|
| #
76888a6e |
|
07-Oct-2013 |
wenzelm <none@none> |
proper warning at run time, not in the parser;
|
| #
203ec60d |
|
05-Sep-2013 |
haftmann <none@none> |
check explicit module names for conformity
|
| #
62f7d300 |
|
30-Jul-2013 |
wenzelm <none@none> |
proper PIDE markup for codegen arguments;
|
| #
a7b3de52 |
|
23-Jun-2013 |
haftmann <none@none> |
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
--HG--
extra : rebase_source : ff8027ac9606264aa4b2d4f8da037c426a3db98b
|
| #
26220651 |
|
23-Jun-2013 |
haftmann <none@none> |
more appropriate cutting of input syntax
--HG--
extra : rebase_source : 040bd4bf2f433fa4f2d2fa9ae7e47e8a93df6c26
|
| #
f1710142 |
|
15-Jun-2013 |
haftmann <none@none> |
more consistent parsing and reading of classes and type constructors
|
| #
65b1eed9 |
|
29-May-2013 |
wenzelm <none@none> |
make SML/NJ happy;
|
| #
8fa4b40e |
|
26-May-2013 |
wenzelm <none@none> |
tuned;
|
| #
8efa9794 |
|
24-May-2013 |
haftmann <none@none> |
bookkeeping and input syntax for exact specification of names of symbols in generated code
--HG--
extra : rebase_source : 60e91890f26f4c44ec2fa3a5be594fa7f2c1bdd0
|
| #
64579d07 |
|
24-May-2013 |
haftmann <none@none> |
use generic data for code symbols for unified "code_printing" syntax for custom serialisations
--HG--
extra : rebase_source : bce13f16528e99c8a7a9be429782c1f1d3c29d49
|
| #
64639f8c |
|
19-May-2013 |
haftmann <none@none> |
tuned, including signature
|
| #
0fe14a59 |
|
10-Apr-2013 |
wenzelm <none@none> |
more standard module name Axclass (according to file name);
|
| #
10b17ef9 |
|
07-Jan-2013 |
wenzelm <none@none> |
tuned -- prefer high-level Table.merge with its slightly more conservative update;
|
| #
c3e8fd6a |
|
27-Jul-2012 |
haftmann <none@none> |
evaluation: allow multiple code modules
|
| #
e737add6 |
|
21-Jul-2012 |
haftmann <none@none> |
also consider current working directory (cf. 3a5a5a992519)
|
| #
3a5dde13 |
|
19-Jul-2012 |
haftmann <none@none> |
export code relatively to master directory
|
| #
d8b8c922 |
|
19-Apr-2012 |
haftmann <none@none> |
dropped dead code;
tuned
--HG--
extra : rebase_source : 3548e686e93188249306305b2ce26a36c18ce819
|
| #
10638423 |
|
23-Mar-2012 |
wenzelm <none@none> |
tuned;
|
| #
150d8520 |
|
16-Mar-2012 |
wenzelm <none@none> |
outer syntax command definitions based on formal command_spec derived from theory header declarations;
|
| #
de9fb383 |
|
15-Mar-2012 |
wenzelm <none@none> |
prefer formally checked @{keyword} parser;
|
| #
9986980f |
|
15-Mar-2012 |
wenzelm <none@none> |
declare minor keywords via theory header;
|
| #
9f564a6a |
|
23-Feb-2012 |
wenzelm <none@none> |
clarified Graph.restrict (formerly Graph.subgraph) based on public graph operations;
|
| #
a63a1640 |
|
06-Sep-2011 |
bulwahn <none@none> |
avoid "Code" as structure name (cf. 3bc39cfe27fe)
|
| #
d6f37a48 |
|
16-Jul-2011 |
wenzelm <none@none> |
moved bash operations to Isabelle_System (cf. Scala version);
|
| #
0b92d370 |
|
27-Jun-2011 |
wenzelm <none@none> |
document antiquotations are managed as theory data, with proper name space and entity markup;
|
| #
ec1196d6 |
|
09-Jun-2011 |
wenzelm <none@none> |
discontinued Name.variant to emphasize that this is old-style / indirect;
|
| #
6d2612c8 |
|
16-Apr-2011 |
wenzelm <none@none> |
modernized structure Proof_Context;
|
| #
e56c255d |
|
16-Apr-2011 |
wenzelm <none@none> |
prefer local name spaces;
tuned signatures;
tuned;
|
| #
9ad65a83 |
|
13-Mar-2011 |
wenzelm <none@none> |
allow spaces in executable names;
simplified generated bash scripts;
|
| #
1e0ee16a |
|
13-Mar-2011 |
wenzelm <none@none> |
tuned;
|
| #
1e07d24e |
|
21-Dec-2010 |
haftmann <none@none> |
tuned names
|
| #
5502b949 |
|
21-Dec-2010 |
haftmann <none@none> |
only depend on exisiting statements
|
| #
9a718ec5 |
|
21-Dec-2010 |
haftmann <none@none> |
evaluator separating static and dynamic operations
|
| #
69361ddc |
|
20-Dec-2010 |
haftmann <none@none> |
more explicit structure for serializer invocation
|
| #
d4167871 |
|
20-Dec-2010 |
wenzelm <none@none> |
slightly more standard Isabelle_System.with_tmp_file/with_tmp_dir (cf. Scala version);
more robust rm_tree -- somewhat dangerous and not exported;
tuned;
|
| #
f4de8ca6 |
|
01-Oct-2010 |
haftmann <none@none> |
check whole target hierarchy for existing reserved symbols
|
| #
44a24106 |
|
28-Sep-2010 |
haftmann <none@none> |
consider quick_and_dirty option before loading theory
|
| #
ef8441e1 |
|
24-Sep-2010 |
haftmann <none@none> |
dropped dead code
|
| #
1d76aa79 |
|
23-Sep-2010 |
haftmann <none@none> |
reverted cs 07549694e2f1 -- use re-printing with current print mode instead after code assembly, avoid Latex.output_typewriter
|
| #
1bb2f38d |
|
23-Sep-2010 |
haftmann <none@none> |
shifted abstraction over imperative print mode
|
| #
33ed10ee |
|
23-Sep-2010 |
haftmann <none@none> |
improved and tuned external codegen tool
|
| #
01b6b297 |
|
17-Sep-2010 |
haftmann <none@none> |
closures separate serializer initialization from serializer invocation as far as appropriate
|
| #
2045d9c2 |
|
16-Sep-2010 |
haftmann <none@none> |
added code_stmts antiquotation from doc-src/more_antiquote.ML
|
| #
e0e92b2c |
|
04-Sep-2010 |
haftmann <none@none> |
dropped names from serializer interface
|
| #
6d96da30 |
|
02-Sep-2010 |
haftmann <none@none> |
hand out deresolver from serializer invocation
|
| #
29dcd16b |
|
02-Sep-2010 |
haftmann <none@none> |
dropped superfluous presentation names
|
| #
c63f8622 |
|
02-Sep-2010 |
haftmann <none@none> |
manage statement selection for presentation wholly through markup
|
| #
760b2c60 |
|
02-Sep-2010 |
haftmann <none@none> |
formal markup of generated code for statements
|
| #
6d9e22df |
|
01-Sep-2010 |
haftmann <none@none> |
formal framework for presentation of selected statements
|
| #
54566e61 |
|
31-Aug-2010 |
haftmann <none@none> |
repaired casual accident; tuned names
|
| #
bc797659 |
|
31-Aug-2010 |
haftmann <none@none> |
avoid strange special treatment of empty module names
|
| #
0e4b5503 |
|
31-Aug-2010 |
haftmann <none@none> |
distinguish code production and code presentation
|
| #
13daea3e |
|
31-Aug-2010 |
haftmann <none@none> |
dropped single_module parameter
|
| #
ca33355f |
|
31-Aug-2010 |
haftmann <none@none> |
tuned
|
| #
c2bf7b3b |
|
31-Aug-2010 |
haftmann <none@none> |
record argument for serializers
|
| #
0889c7c2 |
|
31-Aug-2010 |
haftmann <none@none> |
tuned serializer argument interface
|
| #
df6809b2 |
|
31-Aug-2010 |
haftmann <none@none> |
removed serializer interface redundancies
|
| #
7a8d28bc |
|
31-Aug-2010 |
haftmann <none@none> |
more coherent naming of syntax data structures
|
| #
4c26294e |
|
31-Aug-2010 |
haftmann <none@none> |
dropped legacy interfaces
|
| #
96adab93 |
|
30-Aug-2010 |
haftmann <none@none> |
tuned
|
| #
fa2478b6 |
|
30-Aug-2010 |
haftmann <none@none> |
tuned
|
| #
0017b558 |
|
30-Aug-2010 |
haftmann <none@none> |
tuned
|
| #
aa385f9e |
|
30-Aug-2010 |
haftmann <none@none> |
tuned file interface
|
| #
7faeece9 |
|
30-Aug-2010 |
haftmann <none@none> |
tuned
|
| #
fa897977 |
|
30-Aug-2010 |
haftmann <none@none> |
eliminated some obscure higher-order arguments
|
| #
8ee2a45e |
|
30-Aug-2010 |
haftmann <none@none> |
width is a formal parameter of serialization
|
| #
fff44d90 |
|
30-Aug-2010 |
haftmann <none@none> |
whitespace tuning
|
| #
cdfb85d2 |
|
30-Aug-2010 |
haftmann <none@none> |
tuned comment
|
| #
93bcf928 |
|
30-Aug-2010 |
haftmann <none@none> |
code checking: compiler invocation happens in same directory as generated file -- avoid problem with different path representations on cygwin
|
| #
019ea561 |
|
26-Aug-2010 |
haftmann <none@none> |
proper passing of optional module name
|
| #
6ab291e0 |
|
26-Aug-2010 |
haftmann <none@none> |
tuned serializer interface
|
| #
7b38e58b |
|
26-Jul-2010 |
haftmann <none@none> |
restored unusual snd-biased merge/join policy -- required due to non-conservative code setups
|
| #
a89dbbb2 |
|
20-Jul-2010 |
wenzelm <none@none> |
discontinued pervasive val theory = Thy_Info.get_theory -- prefer antiquotations in most situations;
|
| #
ede59fb5 |
|
19-Jul-2010 |
haftmann <none@none> |
distinguish different classes of const syntax
|
| #
a9d10383 |
|
16-Jul-2010 |
haftmann <none@none> |
consolidate const_syntax naming
|
| #
4489d7bd |
|
16-Jul-2010 |
haftmann <none@none> |
tuned
|
| #
fa5707e7 |
|
16-Jul-2010 |
haftmann <none@none> |
restored long-broken syntax sanity checks
|
| #
4868c13a |
|
14-Jul-2010 |
haftmann <none@none> |
explicit optional checking
|
| #
efd79dee |
|
14-Jul-2010 |
haftmann <none@none> |
added Isar syntax for code checking
|
| #
6728ff4f |
|
14-Jul-2010 |
haftmann <none@none> |
use generic description slot for formal code checking
|
| #
c54f63c8 |
|
14-Jul-2010 |
haftmann <none@none> |
formal slot for code checker
|
| #
134c2b0f |
|
14-Jul-2010 |
haftmann <none@none> |
check without explicit path
|
| #
fb7ae1da |
|
14-Jul-2010 |
haftmann <none@none> |
redirect stderr to stdout
|
| #
b5520044 |
|
08-Jul-2010 |
haftmann <none@none> |
dropped ancient in-place compilation of SML
|
| #
515be4d6 |
|
08-Jul-2010 |
haftmann <none@none> |
checking generated code for various target languages
|
| #
3597bebf |
|
24-Jun-2010 |
wenzelm <none@none> |
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;
|
| #
7a6b0131 |
|
17-May-2010 |
wenzelm <none@none> |
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
eliminated old-style structure aliases K = Keyword, P = Parse;
|
| #
90cf947c |
|
17-May-2010 |
wenzelm <none@none> |
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
eliminated slightly odd alias structure T;
--HG--
rename : src/Pure/Isar/outer_lex.ML => src/Pure/Isar/token.ML
|
| #
73df3dfa |
|
29-Apr-2010 |
haftmann <none@none> |
repaired subtle misunderstanding: statement names are only passed for name resolution
|
| #
ef7550b4 |
|
28-Apr-2010 |
haftmann <none@none> |
exported cert_tyco, read_tyco
|
| #
cc434d26 |
|
21-Apr-2010 |
haftmann <none@none> |
optionally ignore errors during translation of equations
|
| #
a2520e32 |
|
13-Apr-2010 |
haftmann <none@none> |
dropped dead code
|
| #
2c0202c8 |
|
04-Jan-2010 |
haftmann <none@none> |
modernized
|
| #
b9199a91 |
|
23-Dec-2009 |
haftmann <none@none> |
reduced code generator cache to the baremost minimum
|
| #
a449d68f |
|
21-Dec-2009 |
haftmann <none@none> |
clarified various user-defined syntax issues
|
| #
d630566a |
|
14-Dec-2009 |
haftmann <none@none> |
made sml/nj happy
|
| #
0a04845e |
|
11-Dec-2009 |
haftmann <none@none> |
default_code_width is now proper theory data
|
| #
7e72b906 |
|
07-Dec-2009 |
haftmann <none@none> |
tuned inner structure
|
| #
71c651db |
|
29-Nov-2009 |
haftmann <none@none> |
dropped some unused bindings
--HG--
rename : src/HOL/Tools/Datatype/datatype.ML => src/HOL/Tools/Datatype/datatype_data.ML
extra : rebase_source : f9974e246b201df041a994a3a755319b83bce2a3
|
| #
71833c27 |
|
08-Nov-2009 |
wenzelm <none@none> |
adapted Theory_Data;
tuned;
|
| #
b2816004 |
|
17-Oct-2009 |
wenzelm <none@none> |
indicate CRITICAL nature of various setmp combinators;
|
| #
849f2c0f |
|
08-Oct-2009 |
haftmann <none@none> |
moved labelled_name to code_thingol
|
| #
1e5beb93 |
|
29-Sep-2009 |
wenzelm <none@none> |
explicit indication of Unsynchronized.ref;
|
| #
eb3d3d40 |
|
07-Jul-2009 |
haftmann <none@none> |
tuned interface of structure Code
|
| #
d18d6a07 |
|
22-Jun-2009 |
haftmann <none@none> |
uniformly capitialized names for subdirectories
--HG--
rename : src/HOL/Tools/datatype_package/datatype.ML => src/HOL/Tools/Datatype/datatype.ML
rename : src/HOL/Tools/datatype_package/datatype_abs_proofs.ML => src/HOL/Tools/Datatype/datatype_abs_proofs.ML
rename : src/HOL/Tools/datatype_package/datatype_aux.ML => src/HOL/Tools/Datatype/datatype_aux.ML
rename : src/HOL/Tools/datatype_package/datatype_case.ML => src/HOL/Tools/Datatype/datatype_case.ML
rename : src/HOL/Tools/datatype_package/datatype_codegen.ML => src/HOL/Tools/Datatype/datatype_codegen.ML
rename : src/HOL/Tools/datatype_package/datatype_prop.ML => src/HOL/Tools/Datatype/datatype_prop.ML
rename : src/HOL/Tools/datatype_package/datatype_realizer.ML => src/HOL/Tools/Datatype/datatype_realizer.ML
rename : src/HOL/Tools/datatype_package/datatype_rep_proofs.ML => src/HOL/Tools/Datatype/datatype_rep_proofs.ML
rename : src/HOL/Tools/function_package/auto_term.ML => src/HOL/Tools/Function/auto_term.ML
rename : src/HOL/Tools/function_package/context_tree.ML => src/HOL/Tools/Function/context_tree.ML
rename : src/HOL/Tools/function_package/decompose.ML => src/HOL/Tools/Function/decompose.ML
rename : src/HOL/Tools/function_package/descent.ML => src/HOL/Tools/Function/descent.ML
rename : src/HOL/Tools/function_package/fundef.ML => src/HOL/Tools/Function/fundef.ML
rename : src/HOL/Tools/function_package/fundef_common.ML => src/HOL/Tools/Function/fundef_common.ML
rename : src/HOL/Tools/function_package/fundef_core.ML => src/HOL/Tools/Function/fundef_core.ML
rename : src/HOL/Tools/function_package/fundef_datatype.ML => src/HOL/Tools/Function/fundef_datatype.ML
rename : src/HOL/Tools/function_package/fundef_lib.ML => src/HOL/Tools/Function/fundef_lib.ML
rename : src/HOL/Tools/function_package/induction_scheme.ML => src/HOL/Tools/Function/induction_scheme.ML
rename : src/HOL/Tools/function_package/inductive_wrap.ML => src/HOL/Tools/Function/inductive_wrap.ML
rename : src/HOL/Tools/function_package/lexicographic_order.ML => src/HOL/Tools/Function/lexicographic_order.ML
rename : src/HOL/Tools/function_package/measure_functions.ML => src/HOL/Tools/Function/measure_functions.ML
rename : src/HOL/Tools/function_package/mutual.ML => src/HOL/Tools/Function/mutual.ML
rename : src/HOL/Tools/function_package/pattern_split.ML => src/HOL/Tools/Function/pattern_split.ML
rename : src/HOL/Tools/function_package/scnp_reconstruct.ML => src/HOL/Tools/Function/scnp_reconstruct.ML
rename : src/HOL/Tools/function_package/scnp_solve.ML => src/HOL/Tools/Function/scnp_solve.ML
rename : src/HOL/Tools/function_package/size.ML => src/HOL/Tools/Function/size.ML
rename : src/HOL/Tools/function_package/sum_tree.ML => src/HOL/Tools/Function/sum_tree.ML
rename : src/HOL/Tools/function_package/termination.ML => src/HOL/Tools/Function/termination.ML
rename : src/Tools/code/code_haskell.ML => src/Tools/Code/code_haskell.ML
rename : src/Tools/code/code_ml.ML => src/Tools/Code/code_ml.ML
rename : src/Tools/code/code_preproc.ML => src/Tools/Code/code_preproc.ML
rename : src/Tools/code/code_printer.ML => src/Tools/Code/code_printer.ML
rename : src/Tools/code/code_target.ML => src/Tools/Code/code_target.ML
rename : src/Tools/code/code_thingol.ML => src/Tools/Code/code_thingol.ML
|