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
clarified signature;
10 months ago, by wenzelm
clarified output representation: postpone Pretty.separate;
10 months ago, by wenzelm
tuned;
10 months ago, by wenzelm
tuned: fewer warnings in IntelliJ IDEA;
10 months ago, by wenzelm
clarified signature: more accurate types;
10 months ago, by wenzelm
tuned signature: more standard names;
10 months ago, by wenzelm
more uniform pretty_text_area.zoom via its zoom_component;
10 months ago, by wenzelm
tuned signature;
10 months ago, by wenzelm
tuned signature: more standard names;
10 months ago, by wenzelm
tuned;
10 months ago, by wenzelm
clarified signature;
10 months ago, by wenzelm
clarified signature;
10 months ago, by wenzelm
tuned;
10 months ago, by wenzelm
revert 1206400b9b48: proper Node.unapply for Node.apply(null);
10 months ago, by wenzelm
tuned signature;
10 months ago, by wenzelm
clarified signature;
10 months ago, by wenzelm
clarified signature, with subtle change of semantics: proper non-null result;
10 months ago, by wenzelm
clarified modules;
10 months ago, by wenzelm
more robust and uniform metric, still with special treatment motivated by jEdit (see also 0cdfce0bf956);
10 months ago, by wenzelm
misc tuning;
10 months ago, by wenzelm
try0: avoid mapping background theory -- should be handled by Context_Position visibility;
10 months ago, by Fabian Huch
try0: stop early if more subgoals are created;
11 months ago, by Fabian Huch
try0: filter out untagged thms;
11 months ago, by Fabian Huch
try0: support literal facts;
11 months ago, by Fabian Huch
try0: add 'use' modifier for thms to insert;
11 months ago, by Fabian Huch
try0: use extra thms via insert;
11 months ago, by Fabian Huch
clarified: proper type for facts;
11 months ago, by Fabian Huch
clarified: proper type;
11 months ago, by Fabian Huch
tuned;
11 months ago, by Fabian Huch
tuned;
11 months ago, by Fabian Huch
try0: pass tagged thms for better control;
11 months ago, by Fabian Huch
clarified: proper return type;
11 months ago, by Fabian Huch
improve try0: solve multiple subgoals at once, if possible;
11 months ago, by Fabian Huch
tuned: unused parameter;
11 months ago, by Fabian Huch
tuned
10 months ago, by nipkow
better termination behaviour
10 months ago, by nipkow
uniform name T_f for closed-form lemmas for function T_f
10 months ago, by nipkow
More time for primitive functions
10 months ago, by nipkow
merged Reverse into Time_Funs
10 months ago, by nipkow
tuned proofs;
10 months ago, by wenzelm
tuned description: plain text documentation is also supported;
10 months ago, by wenzelm
merged
10 months ago, by wenzelm
update to jdk-21.0.5;
10 months ago, by wenzelm
misc tuning and clarification: Doc.Entry supports both plain files and pdf documents;
10 months ago, by wenzelm
tuned proofs
10 months ago, by nipkow
added missing definitions
10 months ago, by nipkow
tuned proofs;
11 months ago, by wenzelm
clarified modules;
11 months ago, by wenzelm
support value-oriented Font_Metric, e.g. for caching Pretty output;
11 months ago, by wenzelm
tuned;
11 months ago, by wenzelm
unused;
11 months ago, by wenzelm
tuned;
11 months ago, by wenzelm
tuned;
11 months ago, by wenzelm
clarified signature;
11 months ago, by wenzelm
more accurate Symbol.Metric, following 6eccae338770;
11 months ago, by wenzelm
tuned rendering, notably for HiDPI on Linux (see also ca7e2c21b104);
11 months ago, by wenzelm
proper parentheses, for the sake of IntelliJ IDEA;
11 months ago, by wenzelm
clarified modules;
11 months ago, by wenzelm
clarified signature;
11 months ago, by wenzelm
tuned proofs;
11 months ago, by wenzelm
tuned GUI (again, see 0521e65af41e);
11 months ago, by wenzelm
tuned proofs;
11 months ago, by wenzelm
tuned;
11 months ago, by wenzelm
tuned comments;
11 months ago, by wenzelm
clarified signature;
11 months ago, by wenzelm
tuned;
11 months ago, by wenzelm
tuned names;
11 months ago, by wenzelm
more robust;
11 months ago, by wenzelm
clarified signature;
11 months ago, by wenzelm
unused;
11 months ago, by wenzelm
clarified signature: more explicit types;
11 months ago, by wenzelm
tuned GUI;
11 months ago, by wenzelm
tuned;
11 months ago, by wenzelm
clarified signature;
11 months ago, by wenzelm
clarified signature;
11 months ago, by wenzelm
tuned imports;
11 months ago, by wenzelm
tuned: remove redundant checks;
11 months ago, by wenzelm
tuned;
11 months ago, by wenzelm
clarified modules;
11 months ago, by wenzelm
clarified signature;
11 months ago, by wenzelm
clarified signature;
11 months ago, by wenzelm
clarified signature;
11 months ago, by wenzelm
tuned: fewer warnings in IntelliJ IDEA;
11 months ago, by wenzelm
clarified signature;
11 months ago, by wenzelm
clarified modules: more re-usable;
11 months ago, by wenzelm
proper protocol messages (amending 7a1f9e571046);
11 months ago, by wenzelm
clarified treatment of caret_range: better support for multiple (unrelated) selections;
11 months ago, by wenzelm
tuned whitespace;
11 months ago, by wenzelm
support incremental isabelle.select-structure --- like select-block, but based on selection instead of caret;
11 months ago, by wenzelm
clarified rendering: entity acts as atomic notation / expression;
11 months ago, by wenzelm
more rendering for Markup.COMMAND_SPAN, following Rendering.structure_elements;
11 months ago, by wenzelm
more NEWS;
11 months ago, by wenzelm
merged
11 months ago, by wenzelm
support Isabelle/jEdit action isabelle.select_structure;
11 months ago, by wenzelm
more operations;
11 months ago, by wenzelm
clarified text;
11 months ago, by wenzelm
update to jedit5.7.0;
11 months ago, by wenzelm
GUI option "editor_auto_hovering" for Output panel;
11 months ago, by wenzelm
update to scala-3.3.4 LTS;
11 months ago, by wenzelm
removed obsolete markup for "open_block" (see also d5ad89fda714): Isabelle/Scala directly supports XML.Elem pretty-printing;
11 months ago, by wenzelm
Library material from Eberl's Parallel_Shear_Sort
11 months ago, by paulson
Trying to clean up these horribly ugly old proofs, but the requirement of constructivity makes it very difficult
11 months ago, by paulson
use automatically generated time function in HOL-Data_Structures.Selection
11 months ago, by Manuel Eberl
merged
11 months ago, by nipkow
better time_functions (let)
11 months ago, by nipkow
less hidden configuration;
11 months ago, by Fabian Huch
proper passwordless smtp check: must be null;
11 months ago, by Fabian Huch
adjusted documentation
11 months ago, by blanchet
more attribute tuning
11 months ago, by nipkow
tuned attributes
11 months ago, by nipkow
merged
11 months ago, by nipkow
added lemmas
11 months ago, by nipkow
tuned proofs;
11 months ago, by wenzelm
tuned NEWS;
11 months ago, by wenzelm
markup for "..." notation;
11 months ago, by wenzelm
more robust: avoid non-authentic translations;
11 months ago, by wenzelm
tuned whitespace of sources;
11 months ago, by wenzelm
update documentation;
11 months ago, by wenzelm
tuned;
11 months ago, by wenzelm
update documentation: print mode "latex" only affects syntax tables, but output of symbols;
11 months ago, by wenzelm