src/Tools/Code/code_ml.ML
3 months ago haftmann 2019-03-10 migrated from Nums to Zarith as library for OCaml integer arithmetic
4 months ago haftmann 2019-01-25 prefer proper strings in OCaml
5 months ago haftmann 2019-01-10 explicit model concerning files of generated code
7 months ago wenzelm 2018-10-30 clarified signature;
13 months ago haftmann 2018-04-24 proper datatype for 8-bit characters
18 months ago haftmann 2017-12-14 dedicated case option for code generation to Scala
22 months ago haftmann 2017-08-03 tuned
22 months ago haftmann 2017-08-03 work around weakness in export calculation when generating OCaml code
2016-06-14 haftmann 2016-06-14 explicit resolution of ambiguous dictionaries
2016-05-29 haftmann 2016-05-29 do not export abstract constructors in code_reflect
2016-04-18 haftmann 2016-04-18 environment variable check has become pointless after 771b8ad5c7fc
2016-04-13 wenzelm 2016-04-13 tuned;
2016-03-16 wenzelm 2016-03-16 less physical "logic" argument, with option -l like "isabelle console" etc.;
2016-03-10 wenzelm 2016-03-10 isabelle_process is superseded by "isabelle process" tool; tuned tool usage; misc updates and tuning of "system" manual;
2016-03-09 wenzelm 2016-03-09 merged
2016-03-09 wenzelm 2016-03-09 isabelle.Build uses ML_Process directly; isabelle_process is for batch mode only; removed unused feeder (already part of "isabelle console");
2016-03-08 haftmann 2016-03-08 explicit record values for dictionary variables
2016-03-03 wenzelm 2016-03-03 simplified;
2016-02-29 wenzelm 2016-02-29 isabelle_process executable no longer supports writable heap images;
2015-09-06 haftmann 2015-09-06 parenthesing let-expressions in OCaml similar to case expressions avoids precendence problems due to ambiguous scope; with explicit regression setup
2015-01-28 haftmann 2015-01-28 string printing conformant to both (S)ML and Isabelle/ML
2015-01-09 haftmann 2015-01-09 modernized and more uniform style
2014-12-05 haftmann 2014-12-05 allow multiple inheritance of targets
2014-05-02 haftmann 2014-05-02 enforce case of identifiers only to accomodate strict language requirements (or clear separation of constructors from variables in the case of SML)
2014-05-01 haftmann 2014-05-01 centralized upper/lowercase name mangling
2014-02-27 haftmann 2014-02-27 amended some slips, rolling back currently dysfunctional export minimimalisation for Scala
2014-02-23 haftmann 2014-02-23 keep only identifiers public which are explicitly requested or demanded by dependencies
2014-02-23 haftmann 2014-02-23 explicit option for "open" code generation
2014-02-23 haftmann 2014-02-23 tuned
2014-02-23 haftmann 2014-02-23 more fine-grain notion of export
2014-02-23 haftmann 2014-02-23 formal markup for public ingredients
2014-02-23 haftmann 2014-02-23 dropped long-unused option
2014-02-21 haftmann 2014-02-21 dropped dead code
2014-01-25 haftmann 2014-01-25 less clumsy namespace
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-07-04 haftmann 2013-07-04 explicit hint for domain of class parameters in instance statements
2013-06-23 haftmann 2013-06-23 migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
2013-05-24 haftmann 2013-05-24 bookkeeping and input syntax for exact specification of names of symbols in generated code
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
2013-02-13 haftmann 2013-02-13 another attempt for a uniform abort on code generation errors
2012-12-27 haftmann 2012-12-27 more explicit name
2012-11-17 wenzelm 2012-11-17 more portable process exit;
2012-11-07 haftmann 2012-11-07 restored SML code check which got unintentionally broken: must explicitly check for error during compilation; restore more conventional namespace during check (relevant for Imperative-HOL)
2012-07-27 haftmann 2012-07-27 evaluation: allow multiple code modules
2012-06-05 haftmann 2012-06-05 prefer records with speaking labels over deeply nested tuples
2012-05-28 haftmann 2012-05-28 dropped sort constraints on datatype specifications
2012-04-19 haftmann 2012-04-19 dropped dead code
2012-04-19 haftmann 2012-04-19 dropped dead code; tuned
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-06-09 wenzelm 2011-06-09 merged
2011-06-09 bulwahn 2011-06-09 resolving an issue with class instances that are pseudo functions in the OCaml code serializer
2011-06-09 wenzelm 2011-06-09 simplified Name.variant -- discontinued builtin fold_map;
2011-05-02 bulwahn 2011-05-02 improving naming of fresh variables in OCaml serializer
2011-03-13 wenzelm 2011-03-13 cleanup of former settings GHC_PATH, EXEC_GHC, EXEC_OCAML, EXEC_SWIPL, EXEC_YAP -- discontinued implicit detection; determine swipl_version at runtime;
2011-03-13 wenzelm 2011-03-13 allow spaces in executable names; simplified generated bash scripts;
2010-12-21 haftmann 2010-12-21 program is separate argument to serializer
2010-12-13 haftmann 2010-12-13 separated dictionary weakning into separate type