2013-07-05 wenzelm 2013-07-05 tuned signature; tuned comments;
2013-07-05 wenzelm 2013-07-05 tuned signature -- eliminated pointless type synonym;
2013-07-05 wenzelm 2013-07-05 tuned signature; tuned;
2013-07-05 wenzelm 2013-07-05 clarified type Command.eval;
2013-07-05 wenzelm 2013-07-05 tuned signature;
2013-07-05 wenzelm 2013-07-05 tuned signature;
2013-07-05 wenzelm 2013-07-05 explicit module Document_ID as source of globally unique identifiers across ML/Scala;
2013-07-05 nipkow 2013-07-05 improved proof automation for numerals
2013-07-05 wenzelm 2013-07-05 merged
2013-07-04 wenzelm 2013-07-04 separate exec_id assignment for Command.print states, without affecting result of eval; tuned signature; tuned;
2013-07-04 wenzelm 2013-07-04 more Command.memo operations; more explicit types Command.eval vs. Command.print vs. Document.exec; clarified print function parameters;
2013-07-05 nipkow 2013-07-05 tund proofs
2013-07-04 wenzelm 2013-07-04 tuned;
2013-07-04 wenzelm 2013-07-04 made SML/NJ happy;
2013-07-04 Andreas Lochbihler 2013-07-04 merged
2013-07-03 krauss 2013-07-03 more robust instantiation: extract vars from conclusion instead of relying on fixed overall ordering
2013-07-04 haftmann 2013-07-04 consider explicit hint for domain of class parameters when printing instance statements
2013-07-04 haftmann 2013-07-04 explicit hint for domain of class parameters in instance statements
2013-07-03 wenzelm 2013-07-03 merged
2013-07-03 wenzelm 2013-07-03 tuned message;
2013-07-03 wenzelm 2013-07-03 more exception handling -- make print functions total;
2013-07-03 wenzelm 2013-07-03 more print function parameters; check command_visible statically in assignment, instead of dynamically in execution;
2013-07-03 wenzelm 2013-07-03 tuned;
2013-07-03 wenzelm 2013-07-03 discontinued odd workaround for some old Poly/ML, which is still supported but of little practical relevance;
2013-07-03 wenzelm 2013-07-03 tuned;
2013-07-03 wenzelm 2013-07-03 allow multiple print functions;
2013-07-03 wenzelm 2013-07-03 tuned signature;
2013-07-03 wenzelm 2013-07-03 tuned signature;
2013-07-03 wenzelm 2013-07-03 tuned;
2013-07-03 wenzelm 2013-07-03 tuned signature;
2013-07-03 traytel 2013-07-03 use long goal format in rel_induct theorem
2013-07-03 traytel 2013-07-03 share some code between codatatypes, datatypes and eventually prim(co)rec
2013-07-03 nipkow 2013-07-03 tuned names
2013-07-02 wenzelm 2013-07-02 tuned;
2013-07-02 wenzelm 2013-07-02 allow choice of target directory (again, see also 58e2d0cd81ae);
2013-07-02 wenzelm 2013-07-02 postinstall: recover Cygwin permissions;
2013-07-02 wenzelm 2013-07-02 clarified initial cd;
2013-07-02 wenzelm 2013-07-02 clarified Proofterm.proofs vs. Goal.skip_proofs;
2013-07-01 wenzelm 2013-07-01 clarified focus after dismiss;
2013-07-01 wenzelm 2013-07-01 tuned signature;
2013-07-01 wenzelm 2013-07-01 avoid repeated window popup when the mouse is moved over the same content (again, see also cb677987b7e3 and 0a1db0d02628);
2013-07-01 wenzelm 2013-07-01 more robust delayed invocation;
2013-07-01 wenzelm 2013-07-01 clarified tooltip timing of pending event and active state;
2013-07-01 wenzelm 2013-07-01 less intrusive border, notably on windows;
2013-07-01 wenzelm 2013-07-01 tighten tooltip size;
2013-07-01 wenzelm 2013-07-01 visually explicit focus (behaviour dependent on platform and look-and-feel);
2013-06-30 wenzelm 2013-06-30 tuned;
2013-06-30 wenzelm 2013-06-30 more uniform notion of disabled proofs -- NB: historic meaning of 1 for recording theorems is already included in 0;
2013-06-30 wenzelm 2013-06-30 discontinued system option "proofs" -- global state of Proofterm.proofs is persistently compiled into HOL-Proofs image; discontinued unused proofterms for FOL;
2013-06-30 wenzelm 2013-06-30 backout dedd7952a62c: static "proofs" value within theory prevents later inferencing with different configuration;
2013-06-30 wenzelm 2013-06-30 just one alternative proof syntax, which also works for Proof_Syntax.pretty_proof/Proof_Syntax.read_proof roundtrip;
2013-06-30 haftmann 2013-06-30 CONTRIBUTORS
2013-06-29 wenzelm 2013-06-29 avoid potential race condition of focusLost/dismiss vs. popup.show;
2013-06-29 wenzelm 2013-06-29 more direct use of screen location: avoid misplacement if parent component has already disappeared asynchronously;
2013-06-29 wenzelm 2013-06-29 explicit Pretty_Tooltip.dismiss_all due to slightly changed focus mechanics;
2013-06-29 wenzelm 2013-06-29 update text only once;
2013-06-29 wenzelm 2013-06-29 tuned signature;
2013-06-29 wenzelm 2013-06-29 more aggresive ESCAPE handling, while retaining its regular meaning for jEdit;
2013-06-29 wenzelm 2013-06-29 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;
2013-06-29 wenzelm 2013-06-29 tuned signature;