src/Tools/Code/code_target.ML
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;
2014-02-03 wenzelm 2014-02-03 more formal markup;
2014-02-03 haftmann 2014-02-03 tuned storage of code identifiers
2014-01-30 haftmann 2014-01-30 reduced prominence of "permissive code generation"
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 immediate "activation" of const syntax at declaration time
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 syntax passing
2014-01-11 haftmann 2014-01-11 dropped legacy alias feature
2014-01-01 haftmann 2014-01-01 fundamental treatment of undefined vs. universally partial replaces code_abort
2014-01-01 haftmann 2014-01-01 explicit distinction between empty code equations and no code equations, including convenient declaration attributes
2013-10-07 wenzelm 2013-10-07 proper warning at run time, not in the parser;
2013-09-05 haftmann 2013-09-05 check explicit module names for conformity
2013-07-30 wenzelm 2013-07-30 proper PIDE markup for codegen arguments;
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-06-23 haftmann 2013-06-23 more appropriate cutting of input syntax
2013-06-15 haftmann 2013-06-15 more consistent parsing and reading of classes and type constructors
2013-05-29 wenzelm 2013-05-29 make SML/NJ happy;
2013-05-26 wenzelm 2013-05-26 tuned;
2013-05-24 haftmann 2013-05-24 bookkeeping and input syntax for exact specification of names of symbols in generated code
2013-05-24 haftmann 2013-05-24 use generic data for code symbols for unified "code_printing" syntax for custom serialisations
2013-05-19 haftmann 2013-05-19 tuned, including signature
2013-04-10 wenzelm 2013-04-10 more standard module name Axclass (according to file name);
2013-01-08 wenzelm 2013-01-08 tuned -- prefer high-level Table.merge with its slightly more conservative update;
2012-07-27 haftmann 2012-07-27 evaluation: allow multiple code modules
2012-07-21 haftmann 2012-07-21 also consider current working directory (cf. 3a5a5a992519)
2012-07-19 haftmann 2012-07-19 export code relatively to master directory
2012-04-19 haftmann 2012-04-19 dropped dead code; tuned
2012-03-23 wenzelm 2012-03-23 tuned;
2012-03-16 wenzelm 2012-03-16 outer syntax command definitions based on formal command_spec derived from theory header declarations;
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;
2012-02-23 wenzelm 2012-02-23 clarified Graph.restrict (formerly Graph.subgraph) based on public graph operations;
2011-09-06 bulwahn 2011-09-06 avoid "Code" as structure name (cf. 3bc39cfe27fe)
2011-07-16 wenzelm 2011-07-16 moved bash operations to Isabelle_System (cf. Scala version);