tuned

tuned

tuned

tuned file interface

tuned

eliminated some obscure higher-order arguments

trailing newline by default

width is a formal parameter of serialization

whitespace tuning

tuned comment

merged

fiddle with fact filter

adjust Mirabelle

rule out low-level class facts

make Sledgehammer's relevance filter somewhat slacker

move imperative code to where it belongs

fiddle with fact filter based on Mirabelle experiments

allow configuration of fact filter fudge factors

made all fudge factors in relevance filter references, so that Mirabelle can set them (for experiments)

execute actions in same order as specified on command line

show index in fact list of all found facts

allow multiple invocations of "mirabele_sledgehammer_filter", by multiplexing on ID

deal with duplicates

improve new "sledgehammer_filter" action

remove useless var

added evaluation method for relevance filter

remove needless parameter

bring Sledgehammer's combinators in line with Metis's; cf. email from Larry

fiddle with the relevance filter

moved Toplevel.run_command to Pure/PIDE/document.ML; eliminated aliases of exception Toplevel.TERMINATE and Toplevel.EXCURSION_FAIL; tuned signatures;

Command.State: add reported positions to markup tree, according main message position or Markup.binding/entity/report occurrences in body; Position.Id_Range convenience;

tuned;

Node.full_index: allow command spans larger than block_size;

Document_View: repaint overview for any command change of this node (again);

refined proper_line_range (again), to make text_area_extension work with soft wwrap; NB: text_area.offsetToXY returns null for "invisible" positions;

Document state assignment indicates command change;

tuned commands_changed_actor: more precise/efficient handling of visible screen lines;

simplified/clarified Document_View.text_area_extension; tuned Document.Node.block_size, trading some space for better time;

Document.Node: significant speedup of command_range etc. via lazy full_index;

text_edits/recover_spans: reparse at least until line boundary -- increases chance of recovery for bad ML text, for example;

Command.newlines: account for physical newlines;

Toplevel.run_command: more careful treatment of interrupts stemming from nested multi-exceptions etc.; simplified Toplevel.error_msg;

tuned messages: discontinued spurious full-stops (messages are occasionally composed unexpectedly);

more careful treatment of nested multi-exceptions, collapsing cumulatively empty list to Interrupt;

tuned;

Command.results: ordered by serial number;

message serial number indicates physical order;

tuned;

tuned;

merged

what is hidden is hidden

hide all-too-popular constant name eq

merged

formerly unnamed infix equality now named HOL.eq

code checking: compiler invocation happens in same directory as generated file -- avoid problem with different path representations on cygwin

Quotient Package: dont unfold mem_def, use rsp and prs instead

Quotient Package: added respectfulness and preservation lemmas for mem.

quotient package: added a list of pre-simplification rules for Ball, Bex and mem

quotient package: lemmas to be lifted and descended can be pre-simplified

merged

renamed class/constant eq to equal; tuned some instantiations

improved deresolving of implicits

Document_View.text_area_extension: do not insist in crashing if (weak) assertion is violated;

Isabelle/jEdit property for global tooltip dismiss delay;

External_Hyperlink: proper error dialog;

Document_Mode.Line_Context: proper semantic equality/hash code avoids memory leak due to interning in org.gjt.sp.jedit.syntax.TokenMarker;

JEDIT_JAVA_OPTIONS: actors.enableForkJoin=false is supposed to enable ResizableThreadPoolScheduler, to avoid starvation of excessive amounts of future tasks etc.;

session_actor: ignore spurious TIMEOUT (again) -- probably stemming from earlier use of receiveWithin;

session_actor: await state assigment of previous change before signalling current change, and avoid crash in overrun situations;

use Future.get_finished where this is the intended meaning -- prefer immediate crash over deadlock due to promises that are never fulfilled; clarified session signalling;

Swing_Thread.now: volatile result to make double-sure;

Document_Model.token_marker: misc tuning and simplification;

added Document.Snapshot.select_markup, which includes command iteration, range conversion etc.; Markup_Tree.select: plain Iterator; misc tuning and simplification;

XML.Cache: intern property keys once and for all (again);

more careful locking of jEdit buffer;

avoid application crash due to wrong requirement -- result is joined, but change not necessarily finished due to extra map;

include Document.History in Document.State -- just one universal session state maintained by main actor; Session.command_change_buffer: thread actor ensures asynchronous dispatch; misc tuning;

volatile variables (in Scala);

non-critical output primitives -- depending on thread-safe TextIO, while races wrt. flushing should not matter;

modernized specifications;

discontinued separate Pure-ProofGeneral keywords session -- protocol commands are already defined in Pure;

discontinued broken no_warnings_CRITICAL -- global output channels must not be changed after startup initialization;

eliminated broken Output.no_warnings_CRITICAL -- context visibility does the job; modernized attribute setup;

more careful treatment of context visibility flag wrt. spurious warnings; misc tuning;

eliminated obsolete Output.no_warnings, where no warnings were produced anyway;

eliminated broken Output.no_warnings_CRITICAL -- context visibility does the job;

more careful treatment of context visibility flag wrt. spurious warnings;

merged

merged

turn off experimental feature per default + avoid exception on "theory constant"

extended relevance filter with first-order term matching

drop chained facts

rename and simplify

cosmetics

renaming + treat "TFree" better in "pattern_for_type"

fix threshold computation + remove "op =" from relevant constants

avoid needless "that" fact

add nameless chained facts to the pool of things known to Sledgehammer

if the goal contains no constants or frees, fall back on chained facts, then on local facts, etc., instead of generating a trivial ATP problem

improve SPASS hack, when a clause comes from several facts

fix Vampire version numbers

lower penalty for Skolem constants

merged

official support for Scala

updated generated files

tuned whitespace

more xsymbols

re-added accidental omission

proper namespace administration for hierarchical modules

more antiquotations;

eliminated Unsynchronized.ref in favour of configuration option; proper naming of thy: theory vs. ctxt: Proof.context; recovered some Isabelle/ML indendation style;

more appropriate name for configuration option "meson_max_clauses" (cf. output of 'pront_configs');

Sum_Of_Squares: proper configuration options;

tuned printed type names, according to ML;

eliminated unnecessary ref;

clarified iter_deepen_limit vs meson (cf. 7c5896919eb8) -- eliminated global ref;

disposed some old debugging tools;

proper configuration option "show_proofs"; modernized syntax translation;

structure Unsynchronized is never opened and set/reset/toggle have been discontinued; retain Unsynchronized.change alias for Proof General;

expanded some aliases from structure Unsynchronized;