Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-30000
-10000
-3000
-1000
-480
+480
+1000
tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or
revset expression
.
The revision graph only works with JavaScript-enabled browsers.
added field input_eqns to record the list of equations (the specification)
5 months ago, by nipkow
merged
5 months ago, by wenzelm
more NEWS;
5 months ago, by wenzelm
tuned proofs;
5 months ago, by wenzelm
more ambitious mouse handler: double-click selects highlight_area;
5 months ago, by wenzelm
more accurate mouse handler: only for single clicks, consume accepted event;
5 months ago, by wenzelm
more ambitious scrolling: retain original scroll position if possible;
5 months ago, by wenzelm
more ambitious scrolling: retain bottom position after output;
5 months ago, by wenzelm
performance tuning: cache for Rich_Text.format, notably for incremental tracing;
5 months ago, by wenzelm
clarified persistent values: Command.Results does not suitable for caching, because it contains all other messages;
5 months ago, by wenzelm
omit redundant compact_source (see e1abca2527da): Command_Span.unparsed consists of one token with the original source;
5 months ago, by wenzelm
tuned;
5 months ago, by wenzelm
minor performance tuning: avoid duplication of Symbol.spaces (e.g. from Pretty.formatted);
5 months ago, by wenzelm
clarified signature and modules;
5 months ago, by wenzelm
performance tuning for macOS (after update of "jedit" component): old OpenGL works better for text rendering;
5 months ago, by wenzelm
performance tuning: more incremental update of buffer content;
5 months ago, by wenzelm
obsolete;
5 months ago, by wenzelm
clarified: more uniform results;
5 months ago, by wenzelm
clarified signature: inline org.gjt.sp.jedit.textarea.TextArea.setText();
5 months ago, by wenzelm
minor performance tuning: avoid concatenation of existing string material;
5 months ago, by wenzelm
clarified signature and data storage: incremental lazy values;
5 months ago, by wenzelm
tuned comments;
5 months ago, by wenzelm
clarified signature;
5 months ago, by wenzelm
clarified modules;
5 months ago, by wenzelm
clarified margin operations (again, reverting 4794576828df);
5 months ago, by wenzelm
clarified modules;
5 months ago, by wenzelm
more reactive interrupts (via Future.cancel);
5 months ago, by wenzelm
Document.Snapshot: support for multiple snippet_commands;
5 months ago, by wenzelm
more robust: make double-sure that this is the correct output, not a different version from concurrent GUI_Thread.later;
5 months ago, by wenzelm
clarified signature: include standard margin in object equality;
5 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);
5 months ago, by wenzelm
The ceillog2 function (thanks to Manuel Eberl), replacing two copies of Ceil_Log2
5 months ago, by paulson
merged
5 months ago, by wenzelm
merged
5 months ago, by wenzelm
clarified signature: avoid pointless alias (see also c82a1620b274 and 22aeec526ffd);
5 months ago, by wenzelm
clarified signature;
5 months ago, by wenzelm
tuned GUI: avoid wasting space with proportional fonts;
5 months ago, by wenzelm
clarified signature;
5 months ago, by wenzelm
more accurate pretty_margin for proportional fonts;
5 months ago, by wenzelm
clarified signature: more uniform;
5 months ago, by wenzelm
tuned: fewer warnings in IntelliJ IDEA;
5 months ago, by wenzelm
tuned signature;
5 months ago, by wenzelm
tuned signature;
5 months ago, by wenzelm
clarified signature with subtle change of semantics: output consists of individual messages that are formatted (and separated) internally;
5 months ago, by wenzelm
more accurate message boundaries;
5 months ago, by wenzelm
tuned whitespace;
5 months ago, by wenzelm
clarified signature: more robust type XML.Elem;
5 months ago, by wenzelm
clarified signature;
5 months ago, by wenzelm
clarified signature;
5 months ago, by wenzelm
clarified output representation: postpone Pretty.separate;
5 months ago, by wenzelm
tuned;
5 months ago, by wenzelm
tuned: fewer warnings in IntelliJ IDEA;
5 months ago, by wenzelm
clarified signature: more accurate types;
5 months ago, by wenzelm
tuned signature: more standard names;
5 months ago, by wenzelm
more uniform pretty_text_area.zoom via its zoom_component;
5 months ago, by wenzelm
tuned signature;
5 months ago, by wenzelm
tuned signature: more standard names;
5 months ago, by wenzelm
tuned;
5 months ago, by wenzelm
clarified signature;
5 months ago, by wenzelm
clarified signature;
5 months ago, by wenzelm
tuned;
5 months ago, by wenzelm
revert 1206400b9b48: proper Node.unapply for Node.apply(null);
5 months ago, by wenzelm
tuned signature;
5 months ago, by wenzelm
clarified signature;
5 months ago, by wenzelm
clarified signature, with subtle change of semantics: proper non-null result;
5 months ago, by wenzelm
clarified modules;
5 months ago, by wenzelm
more robust and uniform metric, still with special treatment motivated by jEdit (see also 0cdfce0bf956);
5 months ago, by wenzelm
misc tuning;
5 months ago, by wenzelm
try0: avoid mapping background theory -- should be handled by Context_Position visibility;
5 months ago, by Fabian Huch
try0: stop early if more subgoals are created;
5 months ago, by Fabian Huch
try0: filter out untagged thms;
5 months ago, by Fabian Huch
try0: support literal facts;
6 months ago, by Fabian Huch
try0: add 'use' modifier for thms to insert;
6 months ago, by Fabian Huch
try0: use extra thms via insert;
6 months ago, by Fabian Huch
clarified: proper type for facts;
6 months ago, by Fabian Huch
clarified: proper type;
6 months ago, by Fabian Huch
tuned;
6 months ago, by Fabian Huch
tuned;
6 months ago, by Fabian Huch
try0: pass tagged thms for better control;
6 months ago, by Fabian Huch
clarified: proper return type;
6 months ago, by Fabian Huch
improve try0: solve multiple subgoals at once, if possible;
6 months ago, by Fabian Huch
tuned: unused parameter;
6 months ago, by Fabian Huch
tuned
5 months ago, by nipkow
better termination behaviour
5 months ago, by nipkow
uniform name T_f for closed-form lemmas for function T_f
5 months ago, by nipkow
More time for primitive functions
5 months ago, by nipkow
merged Reverse into Time_Funs
5 months ago, by nipkow
tuned proofs;
5 months ago, by wenzelm
tuned description: plain text documentation is also supported;
5 months ago, by wenzelm
merged
5 months ago, by wenzelm
update to jdk-21.0.5;
5 months ago, by wenzelm
misc tuning and clarification: Doc.Entry supports both plain files and pdf documents;
5 months ago, by wenzelm
tuned proofs
5 months ago, by nipkow
added missing definitions
5 months ago, by nipkow
tuned proofs;
5 months ago, by wenzelm
clarified modules;
5 months ago, by wenzelm
support value-oriented Font_Metric, e.g. for caching Pretty output;
5 months ago, by wenzelm
tuned;
5 months ago, by wenzelm
unused;
5 months ago, by wenzelm
tuned;
5 months ago, by wenzelm
tuned;
5 months ago, by wenzelm
clarified signature;
5 months ago, by wenzelm
more accurate Symbol.Metric, following 6eccae338770;
5 months ago, by wenzelm
tuned rendering, notably for HiDPI on Linux (see also ca7e2c21b104);
5 months ago, by wenzelm
proper parentheses, for the sake of IntelliJ IDEA;
5 months ago, by wenzelm
clarified modules;
5 months ago, by wenzelm
clarified signature;
5 months ago, by wenzelm
tuned proofs;
5 months ago, by wenzelm
tuned GUI (again, see 0521e65af41e);
5 months ago, by wenzelm
tuned proofs;
5 months ago, by wenzelm
tuned;
5 months ago, by wenzelm
tuned comments;
5 months ago, by wenzelm
clarified signature;
5 months ago, by wenzelm
tuned;
5 months ago, by wenzelm
tuned names;
5 months ago, by wenzelm
more robust;
5 months ago, by wenzelm
clarified signature;
5 months ago, by wenzelm
unused;
5 months ago, by wenzelm
clarified signature: more explicit types;
5 months ago, by wenzelm
tuned GUI;
5 months ago, by wenzelm
tuned;
5 months ago, by wenzelm
clarified signature;
5 months ago, by wenzelm
clarified signature;
5 months ago, by wenzelm
tuned imports;
5 months ago, by wenzelm
tuned: remove redundant checks;
5 months ago, by wenzelm
tuned;
5 months ago, by wenzelm
clarified modules;
5 months ago, by wenzelm
clarified signature;
5 months ago, by wenzelm
clarified signature;
5 months ago, by wenzelm
clarified signature;
5 months ago, by wenzelm
tuned: fewer warnings in IntelliJ IDEA;
5 months ago, by wenzelm
clarified signature;
5 months ago, by wenzelm
clarified modules: more re-usable;
5 months ago, by wenzelm
proper protocol messages (amending 7a1f9e571046);
5 months ago, by wenzelm
clarified treatment of caret_range: better support for multiple (unrelated) selections;
5 months ago, by wenzelm
tuned whitespace;
5 months ago, by wenzelm
support incremental isabelle.select-structure --- like select-block, but based on selection instead of caret;
5 months ago, by wenzelm
clarified rendering: entity acts as atomic notation / expression;
5 months ago, by wenzelm
more rendering for Markup.COMMAND_SPAN, following Rendering.structure_elements;
5 months ago, by wenzelm
more NEWS;
5 months ago, by wenzelm
merged
5 months ago, by wenzelm
support Isabelle/jEdit action isabelle.select_structure;
5 months ago, by wenzelm
more operations;
5 months ago, by wenzelm
clarified text;
5 months ago, by wenzelm
update to jedit5.7.0;
5 months ago, by wenzelm
GUI option "editor_auto_hovering" for Output panel;
5 months ago, by wenzelm
update to scala-3.3.4 LTS;
5 months ago, by wenzelm
removed obsolete markup for "open_block" (see also d5ad89fda714): Isabelle/Scala directly supports XML.Elem pretty-printing;
5 months ago, by wenzelm
Library material from Eberl's Parallel_Shear_Sort
5 months ago, by paulson
Trying to clean up these horribly ugly old proofs, but the requirement of constructivity makes it very difficult
5 months ago, by paulson
use automatically generated time function in HOL-Data_Structures.Selection
5 months ago, by Manuel Eberl
merged
5 months ago, by nipkow
better time_functions (let)
5 months ago, by nipkow
less hidden configuration;
5 months ago, by Fabian Huch
proper passwordless smtp check: must be null;
5 months ago, by Fabian Huch
adjusted documentation
5 months ago, by blanchet
more attribute tuning
5 months ago, by nipkow
tuned attributes
5 months ago, by nipkow
merged
5 months ago, by nipkow
added lemmas
5 months ago, by nipkow
tuned proofs;
5 months ago, by wenzelm
tuned NEWS;
5 months ago, by wenzelm
markup for "..." notation;
5 months ago, by wenzelm
more robust: avoid non-authentic translations;
5 months ago, by wenzelm
tuned whitespace of sources;
5 months ago, by wenzelm
update documentation;
5 months ago, by wenzelm
tuned;
5 months ago, by wenzelm
update documentation: print mode "latex" only affects syntax tables, but output of symbols;
5 months ago, by wenzelm
misc tuning and clarification;
5 months ago, by wenzelm
clarified section structure;
5 months ago, by wenzelm
tuned;
5 months ago, by wenzelm
tuned;
5 months ago, by wenzelm
tuned;
5 months ago, by wenzelm
tuned signature;
5 months ago, by wenzelm
clarified symbolic output: avoid redundant "block" element for open_block = true;
5 months ago, by wenzelm
clarified signature;
5 months ago, by wenzelm
clarified (again): Markup.intensify is already part of Variable.markup_fixed for undeclared variable, Markup.fixed is already part of Mariable.markup;
5 months ago, by wenzelm
more accurate Symbol.length;
5 months ago, by wenzelm
tuned;
5 months ago, by wenzelm
merged
5 months ago, by wenzelm
more inner-syntax markup;
5 months ago, by wenzelm
obsolete (see a8502d492dde);
5 months ago, by wenzelm
minor performance tuning;
5 months ago, by wenzelm
tuned proofs;
5 months ago, by wenzelm
more inner-syntax markup;
5 months ago, by wenzelm
merged
5 months ago, by nipkow
time_fun: lambdas and lets work now
5 months ago, by nipkow
variable instantiation in Sledgehammer and Metis
5 months ago, by blanchet
prefer rewrite_term_yoyo for improved performance and occasionally better results (conforming to Ast.normalize);
6 months ago, by wenzelm
revert b35c2aa05fcf: redundant due to 89ea66c2045b, if object-logic judgment lacks delimiters;
6 months ago, by wenzelm
clarified position constraints: omit redundant information, e.g. for implicit object-logic judgment;
6 months ago, by wenzelm
unused (see 0199acc01aa8);
6 months ago, by wenzelm
tuned;
6 months ago, by wenzelm
more robust: avoid ambiguity of contract_abbrevs;
6 months ago, by wenzelm
misc tuning: more concise (or hermetic) pointfree style;
6 months ago, by wenzelm
provide rewrite_term_yoyo, which is analogous to Ast.normalize;
6 months ago, by wenzelm
tuned signature;
6 months ago, by wenzelm
tuned names;
6 months ago, by wenzelm
tuned;
6 months ago, by wenzelm
misc tuning and clarification;
6 months ago, by wenzelm
tuned;
6 months ago, by wenzelm
misc tuning and clarification;
6 months ago, by wenzelm
merged
6 months ago, by wenzelm
adhoc option to disable const constraints, notably for AFP/Isabelle_DOF;
6 months ago, by wenzelm
unused;
6 months ago, by wenzelm
tuned signature;
6 months ago, by wenzelm
proper treatment of position constraints;
6 months ago, by wenzelm
more liberal ast matching, notably for case-translations in HOLCF that operate on logical consts rather than syntax consts;
6 months ago, by wenzelm
more parser markup, based on position constraints for logical mixfix syntax;
6 months ago, by wenzelm
more concise representation of term positions;
6 months ago, by wenzelm
more robust;
6 months ago, by wenzelm
tuned signature;
6 months ago, by wenzelm
tuned comments;
6 months ago, by wenzelm
misc tuning and clarification;
6 months ago, by wenzelm
clarified concrete vs. abstract syntax: avoid translations on logical consts;
6 months ago, by wenzelm
misc tuning and clarification;
6 months ago, by wenzelm
clarified markers for syntax consts: avoid overlap with logical consts;
6 months ago, by wenzelm
update ci mail address;
6 months ago, by Fabian Huch
minor performance tuning;
6 months ago, by wenzelm
notable performance tuning (amending a59d9b81be24 and 8976c5bc9e97): avoid costly could_beta_eta_contract, which traverses the whole term;
6 months ago, by wenzelm
tuned;
6 months ago, by wenzelm
clarified signature;
6 months ago, by wenzelm
tuned whitespace;
6 months ago, by wenzelm
support multiple positions (non-empty list);
6 months ago, by wenzelm
more robust syntax translation;
6 months ago, by wenzelm
clarified concrete vs. abstract syntax;
6 months ago, by wenzelm
more inner-syntax markup;
6 months ago, by wenzelm
clarified concrete vs. abstract syntax;
6 months ago, by wenzelm
clarified concrete vs. abstract syntax;
6 months ago, by wenzelm
more operations;
6 months ago, by wenzelm
tuned;
6 months ago, by wenzelm
tuned signature;
6 months ago, by wenzelm
more operations;
6 months ago, by wenzelm
more accurate treatment of constraints: restrict permissive mode to output;
6 months ago, by wenzelm
tuned;
6 months ago, by wenzelm
tuned proofs;
6 months ago, by wenzelm
clarified order of tooltips: make it less dependent on report order from ML (which differs for input vs. output);
6 months ago, by wenzelm
clarified signature (see also 1de8a8b1ae79);
6 months ago, by wenzelm
clarified signature;
6 months ago, by wenzelm
more type information;
6 months ago, by wenzelm
more type information;
6 months ago, by wenzelm
clarified signature;
6 months ago, by wenzelm
clarified signature;
6 months ago, by wenzelm
tuned signature;
6 months ago, by wenzelm
clarified signature;
6 months ago, by wenzelm
suppress dummyT, e.g. from Type_Annotation.print;
6 months ago, by wenzelm
tuned proofs;
6 months ago, by wenzelm
print type constraints for consts with mixfix syntax;
6 months ago, by wenzelm
tuned comments;
6 months ago, by wenzelm
obsolete (see 137ea3d464be);
6 months ago, by wenzelm
tuned proofs;
6 months ago, by wenzelm
tuned whitespace;
6 months ago, by wenzelm
more inner-syntax markup;
6 months ago, by wenzelm
less instrusive rendering for input buffer (in contrast to 264f043c5da1);
6 months ago, by wenzelm
clarified inner-syntax markup;
6 months ago, by wenzelm
tuned whitespace;
6 months ago, by wenzelm
tuned whitespace;
6 months ago, by wenzelm
clarified syntax declarations: keep things together;
6 months ago, by wenzelm
tuned;
6 months ago, by wenzelm
more inner-syntax markup;
6 months ago, by wenzelm
tuned proofs;
6 months ago, by wenzelm
more ambitious rendering: highlight active area for mouse hovering without modifier;
6 months ago, by wenzelm
tuned proofs;
6 months ago, by wenzelm
show_consts_markup is enabled by default;
6 months ago, by wenzelm
clarified signature (again, reverting ec1023a5c54c);
6 months ago, by wenzelm
clarified signature: more explicit Syntax.print_mode_tabs, depending on print_mode_value ();
6 months ago, by wenzelm
redundant;
6 months ago, by wenzelm
tuned signature;
6 months ago, by wenzelm
performance tuning: cache markup and extern operations;
6 months ago, by wenzelm
minor performance tuning;
6 months ago, by wenzelm
minor performance tuning;
6 months ago, by wenzelm
backout somewhat pointless 5ea48342e0ae: no need to declare syntax consts for translations (e.g. constraints);
6 months ago, by wenzelm
tuned;
6 months ago, by wenzelm
tuned;
6 months ago, by wenzelm
revert redundant guard (T = dummyT) from 0278f6d87bad;
6 months ago, by wenzelm
allow type constraints for const_syntax;
6 months ago, by wenzelm
tuned;
6 months ago, by wenzelm
tuned;
6 months ago, by wenzelm
tuned;
6 months ago, by wenzelm
tuned;
6 months ago, by wenzelm
tuned;
6 months ago, by wenzelm
merged
6 months ago, by wenzelm
misc tuning and clarification;
6 months ago, by wenzelm
tuned;
6 months ago, by wenzelm
tuned: more readable names;
6 months ago, by wenzelm
tuned;
6 months ago, by wenzelm
tuned;
6 months ago, by wenzelm
misc tuning and clarification;
6 months ago, by wenzelm
clarified signature;
6 months ago, by wenzelm
clarified signature;
6 months ago, by wenzelm
misc tuning and clarification;
6 months ago, by wenzelm
eliminate clones: just one Collect_binder_tr';
6 months ago, by wenzelm
clarified signature;
6 months ago, by wenzelm
tuned;
6 months ago, by wenzelm
new HO time functions
6 months ago, by nipkow
tuned NEWS;
6 months ago, by wenzelm
clarified inner-syntax markup;
6 months ago, by wenzelm
more syntax bundles;
6 months ago, by wenzelm
more NEWS;
6 months ago, by wenzelm
more inner-syntax markup;
6 months ago, by wenzelm
back to specific nonterminals (amending 52ed95fa4656): otherwise AFP/CakeML won't terminate;
6 months ago, by wenzelm
uniform \<Sum> and \<Prod> syntax, following d10fafeb93c0;
6 months ago, by wenzelm
more NEWS;
6 months ago, by wenzelm
more accurate datatype_record_syntax;
6 months ago, by wenzelm
more syntax bundles, less clones;
6 months ago, by wenzelm
more syntax bundles;
6 months ago, by wenzelm
more syntax bundles;
6 months ago, by wenzelm
more syntax bundles;
6 months ago, by wenzelm
clarified bundles for list syntax;
6 months ago, by wenzelm
more robust declarations via "no syntax" bundles;
6 months ago, by wenzelm
more accurate no_syntax declarations, following ec121999a9cb;
6 months ago, by wenzelm
more robust syntax;
6 months ago, by wenzelm
avoid syntax clashes;
6 months ago, by wenzelm
tuned whitespace, to simplify hypersearch;
6 months ago, by wenzelm
avoid syntax clashes;
6 months ago, by wenzelm
clarified mixfix annotations;
6 months ago, by wenzelm
more inner-syntax markup;
6 months ago, by wenzelm
more inner-syntax markup, without pretty blocks;
6 months ago, by wenzelm
tuned output;
6 months ago, by wenzelm
tuned comments: all times are < 1ms;
6 months ago, by wenzelm
support for pretty blocks that are "open" and thus have no impact on formatting, only on markup;
6 months ago, by wenzelm
clarified signature;
6 months ago, by wenzelm
tuned;
6 months ago, by wenzelm
more inner-syntax markup;
6 months ago, by wenzelm
ML antiquotation for formally-checked bundle names;
6 months ago, by wenzelm
first-class support for "unbundle no foobar_syntax" -- avoid redundant "bundle no_foobar_syntax" definitions;
6 months ago, by wenzelm
misc tuning;
6 months ago, by wenzelm
documentation for pretty block "notation" markup;
6 months ago, by wenzelm
clarified syntax for opening bundles;
6 months ago, by wenzelm
tuned;
6 months ago, by wenzelm
clarified bundles for syntax modifications;
6 months ago, by wenzelm
bundles for syntax modifications seen in AFP;
6 months ago, by wenzelm
tuned;
6 months ago, by wenzelm
merged
6 months ago, by wenzelm
more standard bundle names;
6 months ago, by wenzelm
provide 'open_bundle' command;
6 months ago, by wenzelm
tuned module structure;
6 months ago, by wenzelm
tuned;
6 months ago, by wenzelm
more inner syntax markup;
6 months ago, by wenzelm
more syntax: avoid duplication in AFP;
6 months ago, by wenzelm
clarified abbreviation;
6 months ago, by wenzelm
tuned whitespace;
6 months ago, by wenzelm
tuned;
6 months ago, by wenzelm
more NEWS;
6 months ago, by wenzelm
more inner syntax markup: HOL-Analysis;
6 months ago, by wenzelm
tuned markup;
6 months ago, by wenzelm
more inner syntax markup: HOLCF;
6 months ago, by wenzelm
more 'no_syntax' bundles;
6 months ago, by wenzelm
more robust 'no_syntax' via bundles;
6 months ago, by wenzelm
tuned markup;
6 months ago, by wenzelm
drop somewhat pointless 'syntax_consts' declarations;
6 months ago, by wenzelm
clarified syntax: use outer block (with indent);
6 months ago, by wenzelm
clarified syntax: prefer nonterminal "args", use outer block (with indent);
6 months ago, by wenzelm
proper command kinds;
6 months ago, by Fabian Huch
updated vscode_extension;
6 months ago, by Fabian Huch
NEWS and CONTRIBUTORS;
6 months ago, by Fabian Huch
clarified: add operation;
6 months ago, by Fabian Huch
minor tuning;
6 months ago, by Fabian Huch
lsp: added additional commit characters to immediate completions;
9 months ago, by Thomas Lindae
vscode: further adjusted default settings and wordPattern for consistent completion popups;
9 months ago, by Thomas Lindae
lsp: added more triggerCharacters to make completion popups more consistent;
9 months ago, by Thomas Lindae
vscode: added default setting to make completions pop up by themselves;
9 months ago, by Thomas Lindae
lsp: improved completions;
9 months ago, by Thomas Lindae
vscode: removed unused code;
9 months ago, by Thomas Lindae
vscode: removed README because its content is outdated;
9 months ago, by Thomas Lindae
vscode: disabled whitespace rendering by default because the whitespace symbol is not monospace;
9 months ago, by Thomas Lindae
lsp: added symbol conversion request;
9 months ago, by Thomas Lindae
vscode: changed how options are inserted into package.json so that one can still call `npm install` without errors;
9 months ago, by Thomas Lindae
vscode: removed unused import;
9 months ago, by Thomas Lindae
vscode: changed vscode_unicode_symbols_edits option default to true;
9 months ago, by Thomas Lindae
vscode: made uri equality check on actual strings, not on the functions;
9 months ago, by Thomas Lindae
vscode: switched document_decoration map to use strings as keys instead of Uris, because Uri equality check is inconsistent;
9 months ago, by Thomas Lindae
lsp: added rudimentary indenting to code actions;
9 months ago, by Thomas Lindae
vscode: adjusted setting description;
9 months ago, by Thomas Lindae
lsp: added support for code actions to apply active sendback markups;
9 months ago, by Thomas Lindae
lsp: clarified WorkspaceEdit;
9 months ago, by Thomas Lindae
lsp: made TextDocumentEdit accept optional versions;
9 months ago, by Thomas Lindae
lsp: tuned;
9 months ago, by Thomas Lindae
lsp: removed code that is never run;
9 months ago, by Thomas Lindae
lsp: created distinction for unicode symbols setting between output and edits and clarified output text functions;
9 months ago, by Thomas Lindae
clarified PIDE/line range conversions;
9 months ago, by Thomas Lindae
lsp: refactored conversion from Decoration_List to JSON;
9 months ago, by Thomas Lindae
lsp: tuned pretty_text_panel;
9 months ago, by Thomas Lindae
lsp: removed output_pretty_panel function as its logic is now in pretty_text_panel;
9 months ago, by Thomas Lindae
vscode: added more relevant options;
9 months ago, by Thomas Lindae
lsp: converted state panel to use a pretty text panel;
10 months ago, by Thomas Lindae
lsp: converted dynamic output to use a pretty text panel;
10 months ago, by Thomas Lindae
lsp: added Pretty_Text_Panel module;
10 months ago, by Thomas Lindae
vscode: added relevant isabelle options to vscode settings;
10 months ago, by Thomas Lindae
vscode: indent;
10 months ago, by Thomas Lindae
lsp: extracted panel content generation logic;
10 months ago, by Thomas Lindae
vscode: added all fonts to extension;
10 months ago, by Thomas Lindae
added vscode options tag;
10 months ago, by Thomas Lindae
vscode: tuned;
10 months ago, by Thomas Lindae
lsp: refactored non-html dynamic/state output;
10 months ago, by Thomas Lindae
vscode: reduced how often symbol width gets measured;
11 months ago, by Thomas Lindae
vscode: IsabelleDejaVuSansMono for state and output panel;
11 months ago, by Thomas Lindae
vscode: added decoration request on file switch;
11 months ago, by Thomas Lindae
lsp: added decoration_request notification;
11 months ago, by Thomas Lindae
lsp: added decorations to state updates;
11 months ago, by Thomas Lindae
lsp: added delay to dynamic_output updates after a set_margin;
11 months ago, by Thomas Lindae
lsp: added conversion of symbols for dynamic output so that decoration ranges consider vscode_unicode_symbols setting;
11 months ago, by Thomas Lindae
lsp: unified PIDE/decorations and dynamic output decorations format;
11 months ago, by Thomas Lindae
vscode: changed test_string to "mix" to be consistent with jEdit;
11 months ago, by Thomas Lindae
lsp: added decorations to dynamic output;
11 months ago, by Thomas Lindae
lsp: force update after state_set_margin;
11 months ago, by Thomas Lindae
vscode: added dynamic and state output set margin messages to vscode extension;
10 months ago, by Thomas Lindae
lsp: made margins synchronized;
9 months ago, by Thomas Lindae
lsp: added separation for non-html output and state;
11 months ago, by Thomas Lindae
lsp: tuned;
11 months ago, by Thomas Lindae
lsp: clarified preview_request;
11 months ago, by Thomas Lindae
lsp: added Symbols_Request;
11 months ago, by Thomas Lindae
lsp: added Output_Set_Margin and State_Set_Margin Notifications;
11 months ago, by Thomas Lindae
lsp: changed State_Init notification into a request and removed State_Init_Response;
9 months ago, by Thomas Lindae
lsp: tuned;
11 months ago, by Thomas Lindae
lsp: updated ErrorCodes;
10 months ago, by Thomas Lindae
lsp: added State and Dynamic Output html_output and margin handling;
11 months ago, by Thomas Lindae
lsp: added vscode_html_output option;
11 months ago, by Thomas Lindae
tuned formatting;
11 months ago, by Thomas Lindae
lsp: partially revert c0388fbd8096 to get decorations for all keywords;
12 months ago, by Thomas Lindae
lsp: added State_Init_Response message;
12 months ago, by Thomas Lindae
lsp: removed change_document normalization because it causes desyncs;
10 months ago, by Thomas Lindae
clarified inner-syntax markup, notably for enumerations: prefer "notation=mixfix" over "entity" via 'syntax_consts' (see also 70076ba563d2);
6 months ago, by wenzelm
less markup: prefer "notatation" over "entity";
6 months ago, by wenzelm
clarify comparison of output: ignore token positions, which are somewhat accidental;
6 months ago, by wenzelm
clarified order of markup: more uniform input vs. output;
6 months ago, by wenzelm
misc tuning;
6 months ago, by wenzelm
clarified parse tree: always provide root node;
6 months ago, by wenzelm
tuned signature;
6 months ago, by wenzelm
tuned markup;
6 months ago, by wenzelm
clarified markup: avoid conflict of "notation" with "entity", e.g. in "[x,y,z]" without spaces;
6 months ago, by wenzelm
more flexible command syntax;
6 months ago, by wenzelm
less markup (amending 07ad0b407d38): const = "" is mainly for parentheses syntax -- avoid entity_markup here;
6 months ago, by wenzelm
more markup reports: notably "notation=..." within pretty blocks;
6 months ago, by wenzelm
more parse tree positions;
6 months ago, by wenzelm
more operations;
6 months ago, by wenzelm
clarified order for 'print_syntax' command;
6 months ago, by wenzelm
more accurate parse tree: retain all tokens (and thus positions);
6 months ago, by wenzelm
more thorough markup reports (amending 0c6a600c8939 and 7f9e8516ca05): descend into vacuous nodes;
6 months ago, by wenzelm
clarified comparison: prefer authentic nonterminal context, instead of somewhat accidental "const";
6 months ago, by wenzelm
more detailed parse tree: retain nonterminal context as well;
6 months ago, by wenzelm
clarified persistent data;
6 months ago, by wenzelm
clarified input and output: support markup blocks via Bg/En;
6 months ago, by wenzelm
tuned;
6 months ago, by wenzelm
tuned;
6 months ago, by wenzelm
more operations;
6 months ago, by wenzelm
clarified output: count Tip entries;
6 months ago, by wenzelm
tuned signature;
6 months ago, by wenzelm
tuned whitespace;
6 months ago, by wenzelm
clarified signature: more explicit type "output";
6 months ago, by wenzelm
clarified signature;
6 months ago, by wenzelm
tuned: more uniform;
6 months ago, by wenzelm
tuned: more uniform;
6 months ago, by wenzelm
tuned;
6 months ago, by wenzelm
minor performance tuning;
6 months ago, by wenzelm
tuned;
6 months ago, by wenzelm
tuned;
6 months ago, by wenzelm
minor performance tuning;
6 months ago, by wenzelm
partial revert of d97fdabd9e2b, to build old documentation more reliably;
6 months ago, by wenzelm
tuned signature;
6 months ago, by wenzelm
tuned signature;
6 months ago, by wenzelm
tuned signature;
6 months ago, by wenzelm
clarified signature;
6 months ago, by wenzelm
minor performance tuning: proper table for parsetree list;
6 months ago, by wenzelm
unused (see 954e9d6782ea);
6 months ago, by wenzelm
tuned;
6 months ago, by wenzelm
unused (see 7c1e73540990);
6 months ago, by wenzelm
minor performance tuning (NB: order of prods / states does not matter);
6 months ago, by wenzelm
tuned;
6 months ago, by wenzelm
tuned;
6 months ago, by wenzelm
tuned comments;
6 months ago, by wenzelm
tuned;
6 months ago, by wenzelm
pro-forma support for markup blocks, without any change of result yet;
6 months ago, by wenzelm
tuned;
6 months ago, by wenzelm
merged
6 months ago, by wenzelm
proper 'no_syntax' declarations (amending 8e72f55295fd);
6 months ago, by wenzelm
tuned, following make_symbs in src/Pure/Syntax/printer.ML;
6 months ago, by wenzelm
clarified use of Lexicon.dummy;
6 months ago, by wenzelm
unused (see 584828fa7a97);
6 months ago, by wenzelm
tuned;
6 months ago, by wenzelm
less
more
|
(0)
-30000
-10000
-3000
-1000
-480
+480
+1000
tip