NEWS;

non-focusable button, to avoid second interpretation of SPACE in C+e SPACE (isabelle.set-node-required);

more thorough read_pid with extra delay, to give external process a chance to write pid file before attempting to terminate it -- especially relevant for PIDE document processing, where interrupts can happen in the range of milliseconds;

Added tag Isabelle2013-2-RC2 for changeset 99b9249b3e05

more official task context via Task_Queue.enroll, which is required to participate in group cancellation (e.g. to terminate command exec); tuned signature;

NEWS;

more defensive order of Markup.failed vs. Markup.finished -- more informative status in Isabelle/Scala, although it is not rendered in Isabelle/jEdit;

more robust status reports: avoid loosing information about physical events (see also 28d207ba9340, 2bc5924b117f, 9edfd36a0355) -- NB: TTY and Proof General ignore Output.status and Output.report; more defensive order of Markup.failed vs. Markup.finished, to allow breakdown of ML execution context (see also d7a1973b063c);

more robust and portable invocation of kill as bash builtin, instead of external executable -- NB: /bin/kill on Mac OS X Mountain Lion chokes on Linux workaround from 3610ae73cfdb;

Added tag Isabelle2013-2-RC1 for changeset 57aefb80b639

more on GTK;

reintroduced e2d08b9c9047, lost in 54e290da6da8 + e13b0c88c798 (clone of f6ffe53387ef);

NEWS;

back to Status.FINISHED and immediate remove_overlay (reverting 6e69f9ca8f1c), which is important to avoid restart of print function after edits + re-assignment of located command; resolve sendback wrt. static command id, to allow active area even after exec_id is removed (cf. prune_delay);

updated to Isabelle2013-2;

compile on Windows (clone of d04576557400);

register actual group of nested worker context -- relevant for insulated cancellation of exec_ids (see also 78693e46a237, e0169f13bd37); tuned signature;

updated mirror script for Cambridge

proper code generation for discriminators/selectors

reverted 141cb34744de and e78e7df36690 -- better provide nicer "eta-expanded" definitions for discriminators and selectors, since users might want to unfold them

experiment

make sure acyclicity axiom gets generated in the case where the problem involves mutually recursive datatypes

news

restrict admissibility to non-empty chains to allow more syntax-directed proof rules

merge

generate "code" theorems for incomplete definitions

updated keywords

added 'no_code' option

killed obsolete artifact

revert making 'map_cong' a 'cong' -- it breaks too many proofs in the AFP

avoid user-level 'Specification.definition' for low-level definitions

repaired inconsistency introduced in transiting to 'Local_Theory.define'

docs for forgotten BNF theorems

tuning

added 'cong' attribute to 'map_cong'

avoid user-level 'Specification.definition' for internal constructions (to avoid e.g. automatic code generation behavior)

don't try to register code equations in a locale with assumptions

minor doc update

generalized datatype code generation code so that it works with old-style and new-style (co)datatypes (as long as they are not local)

simpler code

more work towards "exhaustive"

Backed out changeset: a8ad7f6dd217---bypassing Main breaks theories that use \<inf> or \<sup>

set_comprehension_pointfree simproc causes to many surprises if enabled by default

tuned

updated docs

added Riss3g

reduce dependency (toward move to 'HOL')

cleaned up indirect dependency

tuned

prefer sort-stripping const_typ over Sign.the_const_type whenever appropriate

prefer name-normalizing devarify over unvarifyT whenever appropriate

some documentation

command for axiomatic declaration of bnfs---allow theoreticians to fix an arbitrary type with functorial structure and work abstractly on it

remove junk

revert 4af7c82463d3 and document type class problem in Haskell

merged

no ord instance for String.literal in Haskell when list is also ordered lexicographically

implement comparisons on String.literal by target-language comparisons

instantiate linorder for String.literal by lexicographic order

setup lifting/transfer for String.literal