allow choice of target directory (again, see also 58e2d0cd81ae);

postinstall: recover Cygwin permissions;

clarified initial cd;

clarified Proofterm.proofs vs. Goal.skip_proofs;

clarified focus after dismiss;

tuned signature;

avoid repeated window popup when the mouse is moved over the same content (again, see also cb677987b7e3 and 0a1db0d02628);

more robust delayed invocation;

clarified tooltip timing of pending event and active state;

less intrusive border, notably on windows;

tighten tooltip size;

visually explicit focus (behaviour dependent on platform and look-and-feel);

tuned;

more uniform notion of disabled proofs -- NB: historic meaning of 1 for recording theorems is already included in 0;

discontinued system option "proofs" -- global state of Proofterm.proofs is persistently compiled into HOL-Proofs image; discontinued unused proofterms for FOL;

backout dedd7952a62c: static "proofs" value within theory prevents later inferencing with different configuration;

just one alternative proof syntax, which also works for Proof_Syntax.pretty_proof/Proof_Syntax.read_proof roundtrip;

CONTRIBUTORS

avoid potential race condition of focusLost/dismiss vs. popup.show;

more direct use of screen location: avoid misplacement if parent component has already disappeared asynchronously;

explicit Pretty_Tooltip.dismiss_all due to slightly changed focus mechanics;

update text only once;

tuned signature;

more aggresive ESCAPE handling, while retaining its regular meaning for jEdit;

manage popup windows via PopupFactory, which prefers light-weight JComponent, but might fall back on JWindow (despite JPanel of 0f88591478e6); more explicit tooltip hierarchy: manage exactly the visible stack -- caching is part of PopupFactory; auxiliary geometry measurement via single hidden window; tuned signature;

tuned signature;

yet another warning

sort out code equations headed by a projection of a abstract datatype

formally accept dictionary parameters for constants on left hand sides in equations

do not choke on type variables emerging during rewriting

load icons via options -- prefer IntelliJ IDEA for now;

support for idea-icons (using ideaIC-129.354/platform/icons/src from IntelliJ IDEA Community Edition 12.1.2);

manage option "proofs" within theory context -- with minor overhead for primitive inferences;

tuned signature;

proper bold versions of 00ac (logicalnot), 00b0 (degree);

tuned signature;

merged

tuned signature;

clarified printing of type constraints vs. annotations, notably in goal display with its Type_Annotation.ignore_free_types;

updated documentation;

actually use Data.sizef, not hardwired size_of_thm;

more scalable PARALLEL_GOALS, using more elementary retrofit; tuned signature;

tuned

merged

less intrusive SELECT_GOAL: merely rearrange subgoals without detaching goal state, and thus preserve maxidx context; even less intrusive PREFER_GOAL (without structural goal marker), e.g. relevant for generic_simp_tac; adapted ZF proof that broke for unknown reasons (potentially slight change of Drule.size_of_thm);

SOMEthing went utterly wrong;

tuned signature;

more position information for markup;

tuned: cleaned up data structure

simplified data structure

ommit trivial tfrees in annotations

Generalize trace_mult_sym to square products of non-square matrices.

prefer Safari for viewing PDF files, which appears to be better behaved than Preview concerning re-opening recent files (Mountain Lion);

recover command tags from 4cf3f6153eb8 -- important for document preparation;

clarified ISABELLE_DOC_FORMAT -- eliminated slightly odd fall-back;

more robust Doc.view invocation: avoid executing process on GUI thread, but show errors as dialog;

more robust options, notably for isatest mac-poly-M8-skip_proofs;

dockable window for Isabelle documentation;

slightly improved "isabelle doc" based on Isabelle/Scala; updated documentation of "isabelle display";

more formal isabelle_admin_build; tuned;