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)

reference to datatype refinment paper

tuned theory imports

avoid constructor name clash

renamed theory files to be closer to (new) command names

only generate feature weights for queries -- they're not used elsewhere

generate max suggestions in MaSh export driver

new version of MaSh tool, with more server bugfixes

take out dangerous feature, now that all updates are permanent

use new MaSh command-line arguments

shutdown MaSh server

new version of MaSh tool, with less broken server

merged

more careful parsing of nested argument tokens -- avoid Parse.RESET_VALUE on still uninterpreted material;

proper exhaustive match (cf. e9beabf045ab);

proper context;

merged

renamed theory Mrec to Legacy_Mrec, no longer included by default

replaced use of obsolete MREC by partial_function (heap)