src/HOL/Tools/Nitpick/nitpick.ML
2016-08-14 blanchet 2016-08-14 removed trailing final stops in Nitpick messages
2016-04-02 wenzelm 2016-04-02 prefer infix operations;
2016-03-05 wenzelm 2016-03-05 tuned signature -- clarified modules;
2016-02-15 blanchet 2016-02-15 rephrased message
2015-10-08 blanchet 2015-10-08 made TPTP SZS status more compliant
2015-10-02 blanchet 2015-10-02 removed Nitpick nonblocking mode, that was never really used
2015-10-02 blanchet 2015-10-02 better compliance with TPTP SZS standard
2015-08-16 wenzelm 2015-08-16 prefer theory_id operations; tuned signature;
2015-05-29 blanchet 2015-05-29 removed model checks from Nitpick
2015-04-11 wenzelm 2015-04-11 proper Pretty.brk -- redundant spaces do not survive Pretty.text (see also 42b7b76b37b8, e06eabc421e7);
2015-04-08 wenzelm 2015-04-08 proper context for Object_Logic operations;
2015-03-04 wenzelm 2015-03-04 tuned signature -- prefer qualified names;
2015-01-24 wenzelm 2015-01-24 tuned;
2015-01-24 wenzelm 2015-01-24 avoid newline in Pretty.str;
2014-12-23 wenzelm 2014-12-23 explicit message channels for "state", "information"; separate state_message_color;
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-03 wenzelm 2014-11-03 eliminated obsolete Proof.goal_message -- print outcome more directly;
2014-10-31 wenzelm 2014-10-31 discontinued obsolete Output.urgent_message;
2014-08-19 blanchet 2014-08-19 reduced dependency on 'Datatype' theory and ML module
2014-03-21 wenzelm 2014-03-21 more qualified names;
2014-03-03 blanchet 2014-03-03 tuned ML names
2014-03-03 blanchet 2014-03-03 tuned code
2014-03-03 blanchet 2014-03-03 removed nonstandard models from Nitpick
2014-02-17 blanchet 2014-02-17 simplified data structure by reducing the incidence of clumsy indices
2013-12-19 blanchet 2013-12-19 made timeouts in Sledgehammer not be 'option's -- simplified lots of code
2013-09-24 blanchet 2013-09-24 encode goal digest in spying log (to detect duplicates)
2013-09-23 blanchet 2013-09-23 added "spy" option to Nitpick
2013-09-03 wenzelm 2013-09-03 cases: formal binding of 'assumes', with position provided via invoke_case; allow literal equality on type Binding.binding;
2013-09-03 wenzelm 2013-09-03 cases: more position information and PIDE markup;
2013-07-18 wenzelm 2013-07-18 explicit padding on command boundary for "auto" generated sendback -- do not replace the corresponding goal command, but append to it;
2013-07-13 wenzelm 2013-07-13 gutter icon for information messages; avoid redundant Pretty.chunks to keep Markup.information node topmost;
2013-07-13 wenzelm 2013-07-13 more explicit Markup.information for messages produced by "auto" tools;
2013-05-28 blanchet 2013-05-28 no confusing special behavior in debug mode
2013-05-16 blanchet 2013-05-16 tuning -- renamed '_from_' to '_of_' in Sledgehammer
2013-01-11 blanchet 2013-01-11 updated messages
2012-12-12 blanchet 2012-12-12 got rid of support for Kodkodi < 1.2.14
2012-12-10 wenzelm 2012-12-10 generalized notion of active area, where sendback is just one application; some support for graphview via active area;
2012-11-26 wenzelm 2012-11-26 more general sendback properties; support for padding of line boundary, e.g. for ad-hoc insertion of commands via 'help';
2012-11-26 wenzelm 2012-11-26 tuned signature;
2012-11-25 wenzelm 2012-11-25 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
2012-11-22 wenzelm 2012-11-22 more abstract Sendback operations, with explicit id/exec_id properties; purge result messages (again), cf. db58490a68ac, 7b61a539721e;
2012-09-14 wenzelm 2012-09-14 clarified markup names;
2012-08-30 blanchet 2012-08-30 updated Java-related error message
2012-07-18 blanchet 2012-07-18 optimized MaSh output by chunking it
2012-04-25 wenzelm 2012-04-25 merged
2012-04-25 blanchet 2012-04-25 output SZS status as early as possible
2012-04-25 wenzelm 2012-04-25 back to mature jdk1.6.0_31, to avoid issues like Sidekick TAB completion and generic ListCellRenderer;
2012-04-24 blanchet 2012-04-24 add a timeout on the monotonicity check
2012-04-24 blanchet 2012-04-24 handle TPTP definitions as definitions in Nitpick rather than as axioms
2012-04-22 blanchet 2012-04-22 added timeout argument to TPTP tools
2012-04-18 blanchet 2012-04-18 more standard SZS output
2012-04-18 blanchet 2012-04-18 tuned SZS status output
2012-04-18 blanchet 2012-04-18 added SZS status wrappers in TPTP mode
2012-04-18 blanchet 2012-04-18 fixed Auto Nitpick's output
2012-04-16 wenzelm 2012-04-16 more precise handling of java failure, due to missing ISABELLE_JDK_HOME;
2012-03-25 huffman 2012-03-25 merged fork with new numeral representation (see NEWS)
2012-01-17 blanchet 2012-01-17 updated message
2012-01-04 blanchet 2012-01-04 remove subtlety whose justification got lost in time -- the new code is possibly less precise but sounder
2012-01-03 blanchet 2012-01-03 always treat "unit" as a deep datatype, so that we get a good interaction with the record syntax (2.7 of the Nitpick manual)
2012-01-03 blanchet 2012-01-03 rationalized output (a bit)