src/Tools/Code/code_thingol.ML
5 months ago wenzelm 2019-01-13 tuned;
5 months ago wenzelm 2019-01-04 isabelle update -u control_cartouches;
12 months ago wenzelm 2018-06-21 clarified signature;
2017-06-24 haftmann 2017-06-24 treat "undefined" constants internally as special form of case combinators
2017-04-13 haftmann 2017-04-13 for generated Haskell code, never use let-binds with pattern matching: irrefutable patterns destroy partial correctness
2017-01-26 haftmann 2017-01-26 tuned structure and terminology
2016-06-14 haftmann 2016-06-14 explicit resolution of ambiguous dictionaries
2016-05-29 haftmann 2016-05-29 explicit check that abstract constructors cannot be part of official interface
2016-05-26 haftmann 2016-05-26 optional timing for code generator conversions
2016-05-26 haftmann 2016-05-26 corrected closure scope of static_conv_thingol; clarified implementation and names
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-05-26 haftmann 2016-05-26 clarified names of variants
2016-05-09 wenzelm 2016-05-09 clarified context, notably for internal use of Simplifier;
2016-03-08 haftmann 2016-03-08 explicit record values for dictionary variables
2016-03-08 haftmann 2016-03-08 provide explicit hint concering uniqueness of derivation
2015-09-25 wenzelm 2015-09-25 moved remaining display.ML to more_thm.ML;
2015-09-25 wenzelm 2015-09-25 tuned signature: eliminated pointless type Context.pretty;
2015-07-09 wenzelm 2015-07-09 clarified context;
2015-04-27 wenzelm 2015-04-27 code equations as displayable content in code dependency graph
2015-04-27 wenzelm 2015-04-27 filtering of reflexive dependencies avoids problems with state-of-the-art graph browser; clarified
2015-04-16 wenzelm 2015-04-16 discontinued pointless warnings: commands are only defined inside a theory context;
2015-04-16 wenzelm 2015-04-16 let the system choose Graph_Display.display_graph_old: thm_deps needs tree hierarchy, code_deps needs cycles (!?);
2015-04-06 wenzelm 2015-04-06 @{command_spec} is superseded by @{command_keyword};
2015-03-24 wenzelm 2015-03-24 clarified input source;
2015-03-06 wenzelm 2015-03-06 clarified context;
2015-03-06 wenzelm 2015-03-06 Thm.cterm_of and Thm.ctyp_of operate on local context;
2015-02-15 haftmann 2015-02-15 tuned
2015-02-15 haftmann 2015-02-15 purge variables not mentioned in body from pattern
2015-02-14 haftmann 2015-02-14 only collapse patterns with disjunctive variable names
2015-02-14 haftmann 2015-02-14 clarified
2014-12-31 wenzelm 2014-12-31 clarified Graph_Display.graph etc.: sort_graph determines order from structure (and names); tuned;
2014-12-31 wenzelm 2014-12-31 for graph display, prefer graph data structure over list with dependencies; pragmatic distinction between (historically evolved) "session" nodes and (more abstract) "content" nodes
2014-12-31 wenzelm 2014-12-31 more explict and generic field names
2014-12-31 wenzelm 2014-12-31 uniform variable name for presentation graphs, to distinguish from values of type Graph.T
2014-11-26 wenzelm 2014-11-26 renamed "pairself" to "apply2", in accordance to @{apply 2};
2014-11-03 wenzelm 2014-11-03 eliminated unused int_only flag (see also c12484a27367); just proper commands;
2014-09-18 haftmann 2014-09-18 tuned data structure
2014-05-15 haftmann 2014-05-15 syntactic means to prevent accidental mixup of static and dynamic context
2014-05-15 haftmann 2014-05-15 dropped obsolete hand-waving adjustion of type variables: safely done in preprocessor
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-01 haftmann 2014-05-01 optional case enforcement
2014-03-21 wenzelm 2014-03-21 more qualified names;
2014-03-12 wenzelm 2014-03-12 tuned signature;
2014-03-10 wenzelm 2014-03-10 abstract type Name_Space.table; clarified pretty_locale_deps: sort strings; clarified Proof_Context.update_cases: Name_Space.del_table hides name space entry as well;
2014-03-01 wenzelm 2014-03-01 clarified language markup: added "delimited" property; type Symbol_Pos.source preserves information about delimited outer tokens (e.g string, cartouche); observe Completion.Language_Context only for delimited languages, which is important to complete keywords after undelimited inner tokens, e.g. "lemma A pro";
2014-02-26 haftmann 2014-02-26 prefer proof context over background theory
2014-01-30 haftmann 2014-01-30 dependency reporting for code generation errors
2014-01-30 haftmann 2014-01-30 more abstract dictionary construction
2014-01-30 haftmann 2014-01-30 reduced prominence of "permissive code generation"
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-06 haftmann 2014-01-06 special treatment of ==> and == solely as constants
2014-01-06 haftmann 2014-01-06 uniform orientation of instances as (type constructor, type class)
2014-01-01 haftmann 2014-01-01 explicit distinction between empty code equations and no code equations, including convenient declaration attributes
2013-07-30 wenzelm 2013-07-30 proper PIDE markup for codegen arguments;
2013-07-04 haftmann 2013-07-04 explicit hint for domain of class parameters in instance statements
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-04-10 wenzelm 2013-04-10 more standard module name Axclass (according to file name);