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;

misc tuning and clarification;

need to run isabelle update_keywords, but not to check it (cf. 4cf3f6153eb8);

obsolete -- cf. isabelle.Keywords in Scala;

improved "isabelle keywords" and "isabelle update_keywords" based on Isabelle/Scala, without requiring to build sessions first; tuned signature;

back to keyword 'pr' :: diag as required for ProofGeneral command line -- reject this TTY command in Isabelle/jEdit by other means;

more formal ProofGeneral command setup within theory Pure; consider 'ProofGeneral.pr' as control command as well;

tuned;

migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier

more appropriate cutting of input syntax

tuned variable names

tuned message -- more markup;

tuned message;

proper diagnostic command 'print_state';

detach process more reliably -- NB: viewer might be synchronous or asynchronous depending on settings;

clones of increase-font-size / decrease-font-size to allow two further shortcuts for various keyboard layouts;

Scala version of "isabelle doc"; discontinued slightly odd / unused ">>" comments within Contents (see also b077b79061b6);

ML pretty printer for proof terms, with specifica treatment of infix application (similar to terms);

actually observe print_depth for outer term structure;

support for XML data representation of proof terms;

updated to scala-2.10.2;

tuned;

clarified strings of symbols, including ML string literals;

more on managed evaluation;

more on managed evaluation;

updated to Isabelle2013;

tuned;

tuned;

eliminated old "ref" manual;

more on built-in syntax transformations, based on reduced version of old material;

misc tuning and clarification;

more on concrete syntax of proof terms;

more on reconstructing and checking proof terms;

more examples on proof terms;

obsolete;

updated operations on proof terms;

more on proof terms;

updated documentation of sort hypotheses;

Explain to beginners why Complex_Main