isabelle: Graph

tuned signature: more operations;
10 months ago, by wenzelm
tuned: more direct use of Name.context operations;
10 months ago, by wenzelm
tuned;
10 months ago, by wenzelm
misc tuning and clarification: more direct use of Name.context operations;
10 months ago, by wenzelm
tuned signature: more operations;
10 months ago, by wenzelm
tuned: more direct use of Name.context operations;
10 months ago, by wenzelm
clarified signature: shorten common cases;
10 months ago, by wenzelm
tuned: more standard Name.build_context, although that is a bit longer;
10 months ago, by wenzelm
clarified signature: more uniform;
10 months ago, by wenzelm
omit redundant combinators (amending 7456a64bc4f6);
10 months ago, by wenzelm
tuned signature;
10 months ago, by wenzelm
fixed bugs found by Stepan Holub
10 months ago, by blanchet
merged
10 months ago, by nipkow
added lemmas
10 months ago, by nipkow
merged
10 months ago, by wenzelm
more ambitious Search_Result.gui_text, using Swing HTML3 (NB: TreeCellRenderer cannot do this, because it is not updated for each entry);
10 months ago, by wenzelm
clarified signature and object initialization;
10 months ago, by wenzelm
clarified default: avoid copies;
10 months ago, by wenzelm
suppress odd icons for documents and folders;
10 months ago, by wenzelm
support for modified tree cell renderer;
10 months ago, by wenzelm
clarified signature: avoid implicit functionality;
10 months ago, by wenzelm
re-use Output_Area;
10 months ago, by wenzelm
re-use Output_Area;
10 months ago, by wenzelm
re-use Output_Area;
10 months ago, by wenzelm
re-use Output_Area with search results;
10 months ago, by wenzelm
re-use Output_Area with search results;
10 months ago, by wenzelm
more thorough init;
10 months ago, by wenzelm
clarified signature: prefer defaults for Output_Dockable (and its variants);
10 months ago, by wenzelm
unused;
10 months ago, by wenzelm
tuned output: formatting is pointless for proportional font;
10 months ago, by wenzelm
clarified Tree_View.init_model: more uniform;
10 months ago, by wenzelm
more robust update;
10 months ago, by wenzelm
handle tree selection;
10 months ago, by wenzelm
Output_Dockable: show search results as tree view;
10 months ago, by wenzelm
clarified modules;
10 months ago, by wenzelm
clarified signature;
10 months ago, by wenzelm
clarified signature;
10 months ago, by wenzelm
clarified signature and modules: without GUI change yet;
10 months ago, by wenzelm
more operations, to support search within output panel;
10 months ago, by wenzelm
tuned;
10 months ago, by wenzelm
Introduced the function some_elem for grabbing an element from a non-empty set, and simplified the theorem the_elem_image_unique
10 months ago, by paulson
Patch by Stepan Holub, plus tweaks
10 months ago, by paulson
patch to vector_matrix_mult by Alexander Pach
10 months ago, by paulson
try0: cleaned up output;
10 months ago, by Fabian Huch
try0: insert extra facts into state instead of goal, since some methods (e.g. metis) won't work otherwise;
10 months ago, by Fabian Huch
avoid informatik.tu-muenchen.de domain: soon to be discontinued;
10 months ago, by Fabian Huch
renamed Discrete -> Discrete_Functions to avoid name clashes;
10 months ago, by nipkow
Use Var to maintain the difference between function and locale parameters
10 months ago, by nipkow
tuned
10 months ago, by nipkow
tuned proofs;
10 months ago, by wenzelm
tuned proofs;
10 months ago, by wenzelm
minor performance tuning: avoided repeated metric initialization;
10 months ago, by wenzelm
tuned signature: more operations;
10 months ago, by wenzelm
clarified signature;
10 months ago, by wenzelm
more NEWS;
10 months ago, by wenzelm
tuned proofs;
10 months ago, by wenzelm
merged
10 months ago, by wenzelm
enforce rebuild of Isabelle/ML and Isabelle/Scala;
10 months ago, by wenzelm
update to jedit-20241115 (see also ecd62f7b3644 and d92d754b5dd9);
10 months ago, by wenzelm
more patches for the sake of SideKick 1.8 vs. jEdit 5.7.0: provide missing GUIUtilities.isPopupTrigger, avoid StatusBar messages (which often don't fit);
10 months ago, by wenzelm
tuned comments;
10 months ago, by wenzelm
clarified key events: cancel output selection, before input selection;
10 months ago, by wenzelm
proper focus to support subsequent copy-paste via keyboard;
10 months ago, by wenzelm
more accurate initial FontRenderContext, notably on macOS, Windows, or Linux with "env GDK_SCALE=2";
10 months ago, by wenzelm
removed obsolete option: jEdit 5.7.0 can be built with default jdk;
10 months ago, by wenzelm
more rebust mechanics of refresh (see also 82110cbcf9a1 and 2d9b6e32632d): painter.getFontRenderContext might be in undefined state (notably on macOS due to display scaling);
10 months ago, by wenzelm
less ambitious selection;
10 months ago, by wenzelm
mv Discrete to Discrete_Cpo to avoid theory name clashes
10 months ago, by nipkow
disable 2d9b6e32632d for now: unknown problems on macOS;
10 months ago, by wenzelm
clarified mouse selection, avoid conflict of double-click with single-click (follow hyperlink);
10 months ago, by wenzelm
more careful isConsumed() / consume() for key and mouse events;
10 months ago, by wenzelm
merged
10 months ago, by nipkow
added field input_eqns to record the list of equations (the specification)
10 months ago, by nipkow
merged
10 months ago, by wenzelm
more NEWS;
10 months ago, by wenzelm
tuned proofs;
10 months ago, by wenzelm
more ambitious mouse handler: double-click selects highlight_area;
10 months ago, by wenzelm
more accurate mouse handler: only for single clicks, consume accepted event;
10 months ago, by wenzelm
more ambitious scrolling: retain original scroll position if possible;
10 months ago, by wenzelm
more ambitious scrolling: retain bottom position after output;
10 months ago, by wenzelm
performance tuning: cache for Rich_Text.format, notably for incremental tracing;
10 months ago, by wenzelm
clarified persistent values: Command.Results does not suitable for caching, because it contains all other messages;
10 months ago, by wenzelm
omit redundant compact_source (see e1abca2527da): Command_Span.unparsed consists of one token with the original source;
10 months ago, by wenzelm
tuned;
10 months ago, by wenzelm
minor performance tuning: avoid duplication of Symbol.spaces (e.g. from Pretty.formatted);
10 months ago, by wenzelm
clarified signature and modules;
10 months ago, by wenzelm
performance tuning for macOS (after update of "jedit" component): old OpenGL works better for text rendering;
10 months ago, by wenzelm
performance tuning: more incremental update of buffer content;
10 months ago, by wenzelm
obsolete;
10 months ago, by wenzelm
clarified: more uniform results;
10 months ago, by wenzelm
clarified signature: inline org.gjt.sp.jedit.textarea.TextArea.setText();
10 months ago, by wenzelm
minor performance tuning: avoid concatenation of existing string material;
10 months ago, by wenzelm
clarified signature and data storage: incremental lazy values;
10 months ago, by wenzelm
tuned comments;
10 months ago, by wenzelm
clarified signature;
10 months ago, by wenzelm
clarified modules;
10 months ago, by wenzelm
clarified margin operations (again, reverting 4794576828df);
10 months ago, by wenzelm
clarified modules;
10 months ago, by wenzelm
more reactive interrupts (via Future.cancel);
10 months ago, by wenzelm
Document.Snapshot: support for multiple snippet_commands;
10 months ago, by wenzelm
more robust: make double-sure that this is the correct output, not a different version from concurrent GUI_Thread.later;
10 months ago, by wenzelm
clarified signature: include standard margin in object equality;
10 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);
10 months ago, by wenzelm
The ceillog2 function (thanks to Manuel Eberl), replacing two copies of Ceil_Log2
10 months ago, by paulson
merged
10 months ago, by wenzelm
merged
10 months ago, by wenzelm
clarified signature: avoid pointless alias (see also c82a1620b274 and 22aeec526ffd);
10 months ago, by wenzelm
clarified signature;
10 months ago, by wenzelm
tuned GUI: avoid wasting space with proportional fonts;
10 months ago, by wenzelm
clarified signature;
10 months ago, by wenzelm
more accurate pretty_margin for proportional fonts;
10 months ago, by wenzelm
clarified signature: more uniform;
10 months ago, by wenzelm
tuned: fewer warnings in IntelliJ IDEA;
10 months ago, by wenzelm
tuned signature;
10 months ago, by wenzelm
tuned signature;
10 months ago, by wenzelm
clarified signature with subtle change of semantics: output consists of individual messages that are formatted (and separated) internally;
10 months ago, by wenzelm
more accurate message boundaries;
10 months ago, by wenzelm
tuned whitespace;
10 months ago, by wenzelm
clarified signature: more robust type XML.Elem;
10 months ago, by wenzelm
clarified signature;
10 months ago, by wenzelm