src/Tools/Code/code_printer.ML
5 months ago haftmann 2019-01-14 tuned
5 months ago wenzelm 2019-01-04 isabelle update -u control_cartouches;
6 months ago haftmann 2018-12-20 proper attach mechanism for any kind of symbols, not just constants
14 months ago haftmann 2018-04-24 proper datatype for 8-bit characters
2015-09-25 wenzelm 2015-09-25 moved remaining display.ML to more_thm.ML;
2014-12-04 haftmann 2014-12-04 tuned module structure
2014-10-31 wenzelm 2014-10-31 discontinued obsolete \<^sync> marker;
2014-05-01 haftmann 2014-05-01 centralized upper/lowercase name mangling
2014-02-01 wenzelm 2014-02-01 proper context for printing;
2014-01-26 haftmann 2014-01-26 more suitable names, without any notion of "activating"
2014-01-25 haftmann 2014-01-25 less clumsy namespace
2014-01-25 haftmann 2014-01-25 avoid (now superfluous) indirect passing of constant names
2014-01-25 haftmann 2014-01-25 prefer explicit code symbol type over ad-hoc name mangling
2014-01-25 haftmann 2014-01-25 more abstract declaration of unqualified constant names in code printing context
2013-06-23 haftmann 2013-06-23 tuned variable names
2013-05-24 haftmann 2013-05-24 dedicated module for code symbol data
2013-05-24 haftmann 2013-05-24 symbol data covers class relations also
2013-05-21 wenzelm 2013-05-21 make SML/NJ happy;
2013-05-20 wenzelm 2013-05-20 tuned signature;
2013-05-19 haftmann 2013-05-19 infrastructure for generic data for code symbols (constants, type constructors, classes, instances)
2013-05-19 haftmann 2013-05-19 tuned and clarified
2013-05-19 haftmann 2013-05-19 tuned, including signature
2013-02-15 haftmann 2013-02-15 two target language numeral types: integer and natural, as replacement for code_numeral; former theory HOL/Library/Code_Numeral_Types replaces HOL/Code_Numeral; refined stack of theories implementing int and/or nat by target language numerals; reduced number of target language numeral types to exactly one
2012-12-28 haftmann 2012-12-28 formally corrected
2012-12-27 haftmann 2012-12-27 tuned
2012-12-27 haftmann 2012-12-27 uniform parentheses for constructor -- necessary to accomodate scala 10
2012-12-27 haftmann 2012-12-27 tuned
2012-06-05 haftmann 2012-06-05 prefer records with speaking labels over deeply nested tuples
2012-04-19 haftmann 2012-04-19 dropped dead code; tuned
2012-03-15 wenzelm 2012-03-15 prefer formally checked @{keyword} parser;
2012-03-15 wenzelm 2012-03-15 declare minor keywords via theory header;
2011-09-20 bulwahn 2011-09-20 syntactic improvements and tuning names in the code generator due to Florian's code review
2011-09-07 bulwahn 2011-09-07 adding the body type as well to the code generation for constants as it is required for type annotations of constants
2011-09-07 bulwahn 2011-09-07 changing const type to pass along if typing annotations are necessary for disambigous terms
2011-07-23 wenzelm 2011-07-23 defer evaluation of Scan.message, for improved performance in the frequent situation where failure is handled later (e.g. via ||);
2011-06-09 wenzelm 2011-06-09 simplified Name.variant -- discontinued builtin fold_map;
2011-06-09 wenzelm 2011-06-09 discontinued Name.variant to emphasize that this is old-style / indirect;
2010-11-20 wenzelm 2010-11-20 renamed raw "explode" function to "raw_explode" to emphasize its meaning;
2010-09-24 haftmann 2010-09-24 always add trailing newline for presentation
2010-09-23 haftmann 2010-09-23 reverted cs 07549694e2f1
2010-09-23 haftmann 2010-09-23 shifted abstraction over imperative print mode
2010-09-20 haftmann 2010-09-20 use buffers instead of string concatenation
2010-09-17 haftmann 2010-09-17 less intermediate data structures
2010-09-02 haftmann 2010-09-02 set printmode while marking
2010-09-02 haftmann 2010-09-02 corrected printmode handling
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 removed namespace stuff from code_printer
2010-09-02 haftmann 2010-09-02 formal framework for presentation of selected statements
2010-08-31 haftmann 2010-08-31 more coherent naming of syntax data structures
2010-08-31 haftmann 2010-08-31 Code_Printer.tuplify
2010-08-30 haftmann 2010-08-30 trailing newline by default
2010-08-26 haftmann 2010-08-26 private version of commas, cf. printmode
2010-07-24 haftmann 2010-07-24 another refinement chapter in the neverending numeral story
2010-07-21 wenzelm 2010-07-21 made SML/NJ happy;
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-08 haftmann 2010-07-08 tuned titles
2010-06-30 haftmann 2010-06-30 explicit printing function for applify
2010-06-17 haftmann 2010-06-17 more precise code