src/Tools/Code/code_target.ML
2011-03-13 wenzelm 2011-03-13 allow spaces in executable names; simplified generated bash scripts;
2011-03-13 wenzelm 2011-03-13 tuned;
2010-12-21 haftmann 2010-12-21 tuned names
2010-12-21 haftmann 2010-12-21 only depend on exisiting statements
2010-12-21 haftmann 2010-12-21 evaluator separating static and dynamic operations
2010-12-21 haftmann 2010-12-21 more explicit structure for serializer invocation
2010-12-20 wenzelm 2010-12-20 slightly more standard Isabelle_System.with_tmp_file/with_tmp_dir (cf. Scala version); more robust rm_tree -- somewhat dangerous and not exported; tuned;
2010-10-01 haftmann 2010-10-01 check whole target hierarchy for existing reserved symbols
2010-09-28 haftmann 2010-09-28 consider quick_and_dirty option before loading theory
2010-09-24 haftmann 2010-09-24 dropped dead code
2010-09-23 haftmann 2010-09-23 reverted cs 07549694e2f1 -- use re-printing with current print mode instead after code assembly, avoid Latex.output_typewriter
2010-09-23 haftmann 2010-09-23 shifted abstraction over imperative print mode
2010-09-23 haftmann 2010-09-23 improved and tuned external codegen tool
2010-09-17 haftmann 2010-09-17 closures separate serializer initialization from serializer invocation as far as appropriate
2010-09-16 haftmann 2010-09-16 added code_stmts antiquotation from doc-src/more_antiquote.ML
2010-09-04 haftmann 2010-09-04 dropped names from serializer interface
2010-09-02 haftmann 2010-09-02 hand out deresolver from serializer invocation
2010-09-02 haftmann 2010-09-02 dropped superfluous presentation names
2010-09-02 haftmann 2010-09-02 manage statement selection for presentation wholly through markup
2010-09-02 haftmann 2010-09-02 formal markup of generated code for statements
2010-09-02 haftmann 2010-09-02 formal framework for presentation of selected statements
2010-08-31 haftmann 2010-08-31 repaired casual accident; tuned names
2010-08-31 haftmann 2010-08-31 avoid strange special treatment of empty module names
2010-08-31 haftmann 2010-08-31 distinguish code production and code presentation
2010-08-31 haftmann 2010-08-31 dropped single_module parameter
2010-08-31 haftmann 2010-08-31 tuned
2010-08-31 haftmann 2010-08-31 record argument for serializers
2010-08-31 haftmann 2010-08-31 tuned serializer argument interface
2010-08-31 haftmann 2010-08-31 removed serializer interface redundancies
2010-08-31 haftmann 2010-08-31 more coherent naming of syntax data structures
2010-08-31 haftmann 2010-08-31 dropped legacy interfaces
2010-08-30 haftmann 2010-08-30 tuned
2010-08-30 haftmann 2010-08-30 tuned
2010-08-30 haftmann 2010-08-30 tuned
2010-08-30 haftmann 2010-08-30 tuned file interface
2010-08-30 haftmann 2010-08-30 tuned
2010-08-30 haftmann 2010-08-30 eliminated some obscure higher-order arguments
2010-08-30 haftmann 2010-08-30 width is a formal parameter of serialization
2010-08-30 haftmann 2010-08-30 whitespace tuning
2010-08-30 haftmann 2010-08-30 tuned comment
2010-08-30 haftmann 2010-08-30 code checking: compiler invocation happens in same directory as generated file -- avoid problem with different path representations on cygwin
2010-08-26 haftmann 2010-08-26 proper passing of optional module name
2010-08-26 haftmann 2010-08-26 tuned serializer interface
2010-07-26 haftmann 2010-07-26 restored unusual snd-biased merge/join policy -- required due to non-conservative code setups
2010-07-21 wenzelm 2010-07-21 merged
2010-07-19 haftmann 2010-07-19 distinguish different classes of const syntax
2010-07-16 haftmann 2010-07-16 consolidate const_syntax naming
2010-07-20 wenzelm 2010-07-20 discontinued pervasive val theory = Thy_Info.get_theory -- prefer antiquotations in most situations;
2010-07-16 haftmann 2010-07-16 tuned
2010-07-16 haftmann 2010-07-16 restored long-broken syntax sanity checks
2010-07-14 haftmann 2010-07-14 explicit optional checking
2010-07-14 haftmann 2010-07-14 added Isar syntax for code checking
2010-07-14 haftmann 2010-07-14 use generic description slot for formal code checking
2010-07-14 haftmann 2010-07-14 formal slot for code checker
2010-07-14 haftmann 2010-07-14 check without explicit path
2010-07-14 haftmann 2010-07-14 redirect stderr to stdout
2010-07-08 haftmann 2010-07-08 dropped ancient in-place compilation of SML
2010-07-08 haftmann 2010-07-08 checking generated code for various target languages
2010-06-24 wenzelm 2010-06-24 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;
2010-05-17 wenzelm 2010-05-17 prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax; eliminated old-style structure aliases K = Keyword, P = Parse;