merged

updated generated document

only write ghc pragma when writing to a file

added flat_program; tuned signature

dropped ancient deresolve_base; plain_const_syntax also needs modification of instance statement

moved flat_program to code_namespace

dropped outdated substitution

Haskell uses generic flat_program combinator

factored out build_module_namespace

added generic flat_program procedure

using the proposed modes for starting the fixpoint iteration in the mode analysis

merged

renamed expand_*_eq in HOLCF as well

expand_fun_eq -> ext_iff expand_set_eq -> set_ext_iff Naming in line now with multisets

merged

lower expectation in Reg exp example

renewing specification in example file; adding invocation in example file

handling collection of simprules as sets rather than as lists

stating errors in error messages more verbose in predicate compiler

raising an exception instead of guessing some reasonable behaviour for this function

using linear find_least instead of sorting in the mode analysis of the predicate compiler

adding code attribute to definition of equality of finite sets for executability of equality of finite sets

adapting example files

adding the Reg_Exp example

towards time limiting the prolog execution

adding IMP quickcheck examples

adding the CFG example to the build process

adding a List example (challenge from Tobias) for counterexample search

adding dependencies to IsaMakefile; increasing negative search limit for predicate_compile_quickcheck; adding tracing of introduction rules in code_prolog

disposed some old TODO/FIXME;

Document_View: select gutter message icons from markup over line range, not full range results; tuned;

tuned properties;

moved token markup tables to isabelle_markup.scala;

concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;

simplified Markup_Tree.select: Stream instead of Iterator (again), explicit Option instead of default; tuned Snapshot.convert/revert;

Document_View: more precise painting of gutter icons, only if line selection area is sufficiently large;

basic support for warning/error gutter icons;

Document_View: some markup for main inner syntax categories;

Command.State.accumulate: check actual source range;

Isar_Document.reported_positions: slightly more robust treatment of positions outside the command range, notably parsing beyond EOF;

highlight bad range of nested error (here from inner parsing);

Isar_Document.reported_positions: exclude proof state output;

Document_View: less aggressive background coloring, departing from classic PG highlighting; tuned colors;

report token range after inner parse error -- often provides important clues about misunderstanding concerning lexical phase; tuned color;

slightly more robust Plugin.stop -- components might refer to Isabelle.system even after shutdown;

turned show_hyps and show_tags into proper configuration option;

discontinued obsolete ProofContext.prems_limit; simplified command setup for 'pr' etc.;

ML_Context.thm and ML_Context.thms no longer pervasive;

more explicit indication of Config.raw options, which are only needed for bootstrapping Pure;

merged

When comparing Floats use integers instead of reals (represented as rationals), generates less code when Floats are used.

isatest: back to polyml-5.3.0 due to unresolved stability issues of polyml-5.4.0 and HOL/Decision_Procs/Approximation_Ex.thy;

more antiquotations;

ML_Context.thm;

more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical);

modernized session ROOT setup;

some results of concurrency code inspection;

merged;

mention ~/.isabelle/etc/settings file

make remote ATP invocation work for those people who need to go through a proxy; thanks go to Mathieu G. for that fix