isabelle: Graph

Mercurial Mercurial > repos > isabelle / graph

summary | shortlog | changelog | graph | tags | bookmarks | branches | files | gz | help
less more | (0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 tip

clarified modules;
2 months ago, by wenzelm
clarified margin operations (again, reverting 4794576828df);
2 months ago, by wenzelm
clarified modules;
2 months ago, by wenzelm
more reactive interrupts (via Future.cancel);
2 months ago, by wenzelm
Document.Snapshot: support for multiple snippet_commands;
2 months ago, by wenzelm
more robust: make double-sure that this is the correct output, not a different version from concurrent GUI_Thread.later;
2 months ago, by wenzelm
clarified signature: include standard margin in object equality;
2 months ago, by wenzelm
performance tuning: prefer asynchronous Pretty.formatted, which actually takes longer than Command.rich_text (see also 97964515a676, where Pretty.formatted was on the GUI thread, maybe for the sake of java.awt.FontMetrics at that time);
2 months ago, by wenzelm
The ceillog2 function (thanks to Manuel Eberl), replacing two copies of Ceil_Log2
2 months ago, by paulson
merged
2 months ago, by wenzelm
merged
2 months ago, by wenzelm
clarified signature: avoid pointless alias (see also c82a1620b274 and 22aeec526ffd);
2 months ago, by wenzelm
clarified signature;
2 months ago, by wenzelm
tuned GUI: avoid wasting space with proportional fonts;
2 months ago, by wenzelm
clarified signature;
2 months ago, by wenzelm
more accurate pretty_margin for proportional fonts;
2 months ago, by wenzelm
clarified signature: more uniform;
2 months ago, by wenzelm
tuned: fewer warnings in IntelliJ IDEA;
2 months ago, by wenzelm
tuned signature;
2 months ago, by wenzelm
tuned signature;
2 months ago, by wenzelm
clarified signature with subtle change of semantics: output consists of individual messages that are formatted (and separated) internally;
2 months ago, by wenzelm
more accurate message boundaries;
2 months ago, by wenzelm
tuned whitespace;
2 months ago, by wenzelm
clarified signature: more robust type XML.Elem;
2 months ago, by wenzelm
clarified signature;
2 months ago, by wenzelm
clarified signature;
2 months ago, by wenzelm
clarified output representation: postpone Pretty.separate;
2 months ago, by wenzelm
tuned;
2 months ago, by wenzelm
tuned: fewer warnings in IntelliJ IDEA;
2 months ago, by wenzelm
clarified signature: more accurate types;
2 months ago, by wenzelm
tuned signature: more standard names;
2 months ago, by wenzelm
more uniform pretty_text_area.zoom via its zoom_component;
2 months ago, by wenzelm
tuned signature;
2 months ago, by wenzelm
tuned signature: more standard names;
2 months ago, by wenzelm
tuned;
2 months ago, by wenzelm
clarified signature;
2 months ago, by wenzelm
clarified signature;
2 months ago, by wenzelm
tuned;
2 months ago, by wenzelm
revert 1206400b9b48: proper Node.unapply for Node.apply(null);
2 months ago, by wenzelm
tuned signature;
2 months ago, by wenzelm
clarified signature;
2 months ago, by wenzelm
clarified signature, with subtle change of semantics: proper non-null result;
2 months ago, by wenzelm
clarified modules;
2 months ago, by wenzelm
more robust and uniform metric, still with special treatment motivated by jEdit (see also 0cdfce0bf956);
2 months ago, by wenzelm
misc tuning;
2 months ago, by wenzelm
try0: avoid mapping background theory -- should be handled by Context_Position visibility;
2 months ago, by Fabian Huch
try0: stop early if more subgoals are created;
2 months ago, by Fabian Huch
try0: filter out untagged thms;
2 months ago, by Fabian Huch
try0: support literal facts;
2 months ago, by Fabian Huch
try0: add 'use' modifier for thms to insert;
2 months ago, by Fabian Huch
try0: use extra thms via insert;
2 months ago, by Fabian Huch
clarified: proper type for facts;
2 months ago, by Fabian Huch
clarified: proper type;
2 months ago, by Fabian Huch
tuned;
2 months ago, by Fabian Huch
tuned;
2 months ago, by Fabian Huch
try0: pass tagged thms for better control;
2 months ago, by Fabian Huch
clarified: proper return type;
2 months ago, by Fabian Huch
improve try0: solve multiple subgoals at once, if possible;
2 months ago, by Fabian Huch
tuned: unused parameter;
2 months ago, by Fabian Huch
tuned
2 months ago, by nipkow

less more | (0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 tip

isabelle