merged

tuned proofs;

tuned proofs;

provide ISABELLE_JAVA_SYSTEM_OPTIONS via settings;

uniform abbrevs for left/right arrows;

more abbrevs according to Isabelle/HOL ASCII replacement syntax;

added common alternative for == (its ambiguity also avoids conflict with ==>); clarified (= )= [= ]= (like <= >=); removed * (too intrusive);

more accurate description: Swing/L&F has additional handlers;

handle selector formulae with no corecursive calls

merged

tuned proofs;

simplified (see 7c39677f9ea0);

sort items according to persistent history of frequency of use;

more general backup files;

fixed bug in primrec_new (allow indirect recursion through constructor arguments other than the first)

some tests on /home/polyml/polyml-svn, which is approaching polyml-5.5.1;

tuned proofs;

Doc improvements

prove theorem in the right context (that knows about local variables)

fixed docs w.r.t. availability of "primrec_new" and friends

more canonical naming

more set syntax

merged

NEWS;

more explicit indication of unique result (see also 45be26b98ca6, 3d654643cf56);

explicit is always immediate;

single-letter abbrev does not make sense -- too many candidates;

allow short words for explicit completion;

fewer conflicts -- adhoc resolution of == vs. ==> via unicode (!) image;

more symbol abbrevs;

misc tuning -- reduce conflicts;

allow multiple entries;

more symbol abbrevs, based on ProofGeneral-4.2/isar/isar-unicode-tokens.el and traditional Isabelle/HOL ASCII replacement syntax;

allow multiple symbol properties, notably groups and abbrevs;

private copy (!) of etc/symbols for WWW_Find, which has its own interpretation of the file format;

check tar error, e.g. from corrupted download;

less surprising immediate completion;

updated keywords

tuned theory name

moved keywords down the hierarchy

renamed command to clarify connection with BNF

merged two theory files

updated news/contributors with BNF stuff

added example

rationalized files

polished newly included files after moving

moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository

tuned proofs;

merged

qualify internal and external constants in {l,g}fp properly

merged

merged

border as for Pretty_Tooltip;

less aggressive immediate completion, based on input and text;

preserve original word -- relevant for true uniqueness of immediate completion;

tuned;

added action isabelle.complete, using standard jEdit keyboard shortcut;

option to insert unique completion immediately into buffer;

tuned proofs;

renamed BNF fact

renamed BNF axiom

renamed BNF fact

renamed BNF axiom

compile

renamed BNF fact

make SML/NJ happy

merged

tuned proofs;

clarified SideKick parser name, which serves as quasi "mode" here;

explicit indication of outer syntax with no tokens; uniform Isabelle.markers, based on syntax specification -- no tokens for NEWS;

clarified module location;

always use extended styles (despite de26cf3191a3);

more uniform configuration of editor modes and token markers;

syntax for isabelle-news with symbol completion;

tuned signature;

maintain Completion_Popup.Text_Area as client property like Document_View; global Completion_Popup.Text_Area init/exit like SideKickPlugin; eliminated old SideKick completion -- cover all Isabelle modes uniformly; dynamic lookup of Isabelle.mode_syntax -- NB: buffer mode might be undefined in intermediate stages;

some completion options;

more abstract Completion_Popup.Text_Area; more uniform font size;

GTK+ works better due to avoidance of default list view popups;

renamed BNF axiom

merge

handle type class annotations on (co)datatype parameters gracefully

store nesting_bnfs in fp_sugar (required in "nested to mutual" reduction)

cleaner handling of bootstrapping "fake" context, with fewer (no?) obscure bugs

qualify BNF constants properly

qualify generated constants uniformly

rationalized bindings

rationalize message generation + added a warning

removed outdated comments

build relator term for compound type (generalized build_map)

documentation ideas

renamed an ML filed for consistency (low-level => ctor/dtor/xtor in name)

merge

more

tuned proofs;

merged

tuned proofs;

tuned proofs;

complete symbols only in backslash forms -- less intrusive editing, greater chance of finding escape sequence in text; complete words >= 3 characters only; discontinued short word abbrev "Un" (see also fdd6e68e29d9 and e38e80686ce5);

tuned signature -- no need for ooddities;

tuned -- help finding rare NPE on cold start;

tuned proofs;

uniform use of isabelle.jEdit.Popup, based on generic screen location operations;

more elementary Popup via JLayeredPane -- avoid javax.swing.PopupFactory with its many problems and dangers of accidental HeavyWeightPopup (especially on Mac OS X); observe !evt.isConsumed semantically: no initial dismiss here (e.g. due to cursor keys);

tuned;

dismiss popups more uniformly;

more uniform check (see JEdit_Lib.propagate_key);

tuned signature;

more symbols;

tuned proofs;

tuned proofs;

tuned proofs;

enable jEdit KeyEventWorkaround uniformly;

de-register completion first, which is important to make new popup reliably;

register single instance within root, in order to get rid of old popup as user continues typing;

more careful refocus operation: do not reset focus if it was already lost (relevant when activating a different GUI component, for example);

some actual completion via outer syntax; disable old SideKick completion for "isabelle" mode;

tuned signature;

avoid complication and event duplication due to KeyEventInterceptor -- NB: popup has focus within root window, it is closed on loss of focus; uniform JEdit_Lib.propagate_key;

determine completion geometry like tooltip; just one option jedit_popup_bounds for tooltip and completion;

explicit "hidden" operation with focus management; explicit popup_font; just one option jedit_popup_font_scale for tooltip and completion;

some key event handling in the manner of SideKickBindings, SideKickCompletionPopup;

more standard key handling according to jEdit (with workaround); clarified handling of ESCAPE (again): dismiss without second interpretation as select-none;

more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;

got rid of old error -- users who install SPASS manually are responsible for any version mismatches

tuned messages

natural component order

better error message

tuning

tuned

use only one data slot; rename print_quotmaps to print_quot_maps; tuned

merged

added rtrancl_while

renamed inner_dense_linorder to dense_linorder

renamed typeclass dense_linorder to unbounded_dense_linorder

tuned imports; tuned proofs;

another sample found by Stefan Berghofer;

added SHA1 library integrity test, which is invoked at compile time and Isabelle_Process run-time;

allow NUL characters in ML string passed to C library;

simplify code (now that ctr_sugar uses the same type variables as fp_sugar)

merged

prefer build_doc -s to avoid heaps left behind in $ISABELLE_HOME_USER (especially relevant to isatest);

prefer Binding.name_of over Binding.print -- the latter leads to funny quotes and markup within the constructed term;

always transfer thm where attributes are applied -- relevant for internal 'notes' (e.g. via bundle 'includes') in contrast to external 'notes' (cf. Proof_Context.retrieve_thms);

proper context;

tuned

moved derivation of ctor_dtor_unfold to sugar (streamlines fp_result interface)

export one more ML function, needed for primcorec

reverted 6c5e7143e1f6; took a better look at evaluation data this time

tuned unchecked ML;

removed junk;

ignore trailing primes, e.g. rename \<alpha>' to \<alpha>'' instead of \<alpha>'a;

tuned fudge factor in light of evaluation

tuned proofs;

tuned proofs;

discontinued rendering of obsolete \<onesuperior>, \<twosuperior>, \<threesuperior>;

tuned;

maintain goal forks as part of global execution; tuned;

tuned proofs -- fewer warnings;

simplified Goal.forked_proofs: status is determined via group instead of dummy future (see also Pure/PIDE/execution.ML); clarified Task_Queue.group_status; tuned;

discontinued parallel_subproofs_saturation and related internal counters (superseded by parallel_subproofs_threshold and timing information); simplified Goal.future_enabled;

some secondary shortcuts derived from 5.1.0/keymaps/German_Keyboard_keys.props (using CIRCUMFLEX instead of S+1); tuned;

use view root as parent for popup, which provides more space and avoids confusion of mouse wheel handlers on Windows (wrt. text area scrollbar);

tuned proofs;

tuned proofs;

confine popup to parent component, to avoid javax.swing.PopupFactory$HeavyWeightPopup and its problems with Linux window management and Mac OS X key handling;

strict checking of coordinates wrt. inner painter component;

more static values;

support more brackets;

prefer static "control", which is determined when the mouse event happens, not when its action runs;

tuned signature;

more precise painting;

more uniform treatment of Swing_Thread context switch: prefer asynchronous Swing_Thread.later from actor;

clarified border (again, see also 7ce3ebc268a1);

more faithful representation of U+2983 and U+2984 as "white" curly braces -- based on braces and bar from cmsy10.pfb;

prefer plain subscript for notation;

merged

more standard parser combinator expressions and tool setup;

added Theory.setup convenience;

more robust ML_Antiquote.variant via Name.desymbolize (which also allows symbolic names, for example);

clarified type ML_Context.antiq: context parser maintains compilation context, declaration is applied to final context; subtle change of semantics of ML_Context.add_antiq: need to avoid accidental update of context due to concrete syntax parser (cf. Scan.pass);

tuned signature;

discontinued unused antiquotation blocks;

missing ROOT (cf. beb4ee344c22);

more modular setup;

clarified position of Spec_Check for Isabelle/ML -- it is unrelated to Isabelle/HOL; just one src/Tools/ROOT;

removed unused ML antiquotations @{let}, @{note};

obsolete (see 52790e3961fe);

added action isabelle.reset-font-size;

tuned -- some reformatting;

repaired num_extra_feature_facts + tuning

thread information about when a constant became relevant through MePo -- the information is not used yet but could help fight starvation in the (ITP) world

removed obsolete file

minor MaSh fix

eliminated some needless MaSh features

tuned output

better tracing + honor blocking better

learn new facts on query if there aren't too many of them in MaSh

remove OP

increase relevance of unknown proximate facts

fixed pattern matching

fixed subtle bug with "take" + thread overlord through

separate tracing option for code_simp

congruence rules for code_simp to mimic typical non-strict behaviour of conj and disj

delete corresponding compound lhs and rhs when a transfer rule is deleted; tuned

publish a private function

configuration option to control timing output for (co)datatypes

have kill_all also kill MaSh server + be paranoid about reloading after clear_state, to allow for easier experimentation

take chained and proximate facts into consideration when computing MaSh features

pour extra features from proximate facts into goal, in exporter

cleanup old duplicated functionality

store theorem about composition of fold and map in fp_result

tuning

ideas for (co)datatype docs

minor tweaks to MaSh tool

added datatype example

support more brackets; more uniform isabelle modes;

prefer text version of single angle quotation marks: U+2039 and U+203A from DejaVuSansMono;

double check that lhs or rhs really matches a subterm in a goal when creating a hole in a skeleton (Net.net does only rough matching)

improve weight computation for complex terms

improved support for MaSh server

get rid of some silly MaSh features

weight MaSh constants by frequency

transfer stored fp_sugar theorems into the "current" theory when retrieving an fp_sugar (avoids non-trivial merges)