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;