src/Tools/Code/code_target.ML
3 months ago haftmann 2019-03-10 migrated from Nums to Zarith as library for OCaml integer arithmetic
4 months ago wenzelm 2019-02-02 clarified signature: Path.T as in Generated_Files;
5 months ago haftmann 2019-01-20 more conventional parsing of code_stmts antiquotation
5 months ago haftmann 2019-01-20 more conventional syntax for code_stmts antiquotation
5 months ago haftmann 2019-01-14 canonical operation to typeset generated code makes dedicated environment obsolete
5 months ago wenzelm 2019-01-14 clarified message;
5 months ago wenzelm 2019-01-13 information with hyperlink to "isabelle-export:";
5 months ago wenzelm 2019-01-13 regular export with implicit compression: result is uncompressed;
5 months ago wenzelm 2019-01-13 clarified -- removed pointless Parse.!!!;
5 months ago wenzelm 2019-01-13 tuned;
5 months ago haftmann 2019-01-10 optional code export as theory export
5 months ago haftmann 2019-01-10 explicit model concerning files of generated code
5 months ago wenzelm 2019-01-04 isabelle update -u control_cartouches;
5 months ago haftmann 2018-12-29 more correct handling of symbols for includes
6 months ago haftmann 2018-12-20 proper attach mechanism for any kind of symbols, not just constants
6 months ago haftmann 2018-12-20 disregard historic keyword
17 months ago wenzelm 2018-01-18 clarified access to antiquotation options; define explicit variants of antiquotations; output proper Latex.text; misc tuning and clarification;
17 months ago wenzelm 2018-01-09 clarified modules;
18 months ago haftmann 2017-12-14 dedicated case option for code generation to Scala
22 months ago wenzelm 2017-09-01 more PIDE markup;
2017-01-27 haftmann 2017-01-27 ML antiquotation for generated computations
2017-01-26 haftmann 2017-01-26 tuned structure and terminology
2016-05-26 haftmann 2016-05-26 optional timing for code generator conversions
2016-05-26 haftmann 2016-05-26 clarified proof context vs. background theory
2016-05-26 haftmann 2016-05-26 clarified naming conventions and code for code evaluation sandwiches
2016-04-18 haftmann 2016-04-18 environment variable check has become pointless after 771b8ad5c7fc
2016-04-13 wenzelm 2016-04-13 eliminated "xname" and variants;
2016-03-07 wenzelm 2016-03-07 tuned -- more standard operations;
2016-03-07 wenzelm 2016-03-07 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;
2015-04-06 wenzelm 2015-04-06 @{command_spec} is superseded by @{command_keyword};
2015-02-05 haftmann 2015-02-05 dropped obsolete external entrance point
2015-02-05 haftmann 2015-02-05 explicit error message for non-existing targets
2015-01-24 wenzelm 2015-01-24 more direct Output.output; avoid newline in Code_Printer/Pretty.str;
2015-01-09 haftmann 2015-01-09 prefer option for default code printing width
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-12-04 haftmann 2014-12-04 tuned module structure
2014-12-04 haftmann 2014-12-04 tuned data structures
2014-12-04 haftmann 2014-12-04 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
2014-12-04 haftmann 2014-12-04 tuned
2014-12-04 haftmann 2014-12-04 tuned names
2014-12-03 wenzelm 2014-12-03 tuned signature;
2014-11-26 wenzelm 2014-11-26 renamed "pairself" to "apply2", in accordance to @{apply 2};
2014-11-07 wenzelm 2014-11-07 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;
2014-11-05 wenzelm 2014-11-05 explicit type Keyword.keywords; tuned signature;
2014-08-12 wenzelm 2014-08-12 tuned signature according to Scala version -- prefer explicit argument;
2014-06-12 haftmann 2014-06-12 formal variable name: IVar NONE is strictly spoken not supported on lhs of function definitions, e.g. in Scala
2014-05-09 haftmann 2014-05-09 normalizing of type variables before evaluation with explicit resubstitution function: make nbe work with funny type variables like \<AA>; tuned naming; dropped dead parameters;
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 optional case enforcement
2014-03-18 wenzelm 2014-03-18 clarifed module name;
2014-03-18 wenzelm 2014-03-18 tuned signature;
2014-03-09 wenzelm 2014-03-09 tuned signature;
2014-03-06 wenzelm 2014-03-06 tuned signature -- more uniform check_type_name/read_type_name; proper reports for read_type_name (lost in 710bc66f432c);
2014-02-27 haftmann 2014-02-27 amended some slips, rolling back currently dysfunctional export minimimalisation for Scala
2014-02-26 haftmann 2014-02-26 prefer proof context over background theory
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-09 haftmann 2014-02-09 dropped legacy finally
2014-02-03 wenzelm 2014-02-03 merged;