NEWS: some notes on interrupts;

refined Runtime.toplevel_error/Document.run_command: let interrupts pass unhindered;

removed dead code;

avoid handling interrupts in user code;

Meson.make_clauses_unsorted: removed spurious debug code stemming from 5146d640aa4a -- must not handle arbitrary exceptions in user space;

main command loops are supposed to be uninterruptible -- no special treatment here;

Exn.is_interrupt: include interrupts that have passed through the IO layer;

more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;

avoid mixing of static and runtime errors in compiler output, to accomodate Proof General; refrain from absorbing Exn.Interrupt, to accomodate asynchronous interaction; actually observe Isabelle/ML naming conventions in exception STATIC_ERRORS;

ML_Compiler.eval: discontinued extra "Static Errors" of raw Poly/ML;

isabelle-jedit.css: suppress "location" markup, which indicates extra positional information intended for plain-old TTY mode;

ML_Compiler.eval: more careful printing of messages and regular output, trying to accomodate Poly/ML, Proof General, Isabelle/Scala/jEdit at the same time;

clarified -- inlined ML_Env.local_context;

merged

restricting invocation only if PROLOG_HOME is set

tuned proofs (based on fancy gutter icons in Isabelle/jEdit);

merge

remove "safe" (as suggested by Tobias) and added "arith" to "try"

remove "minipick" (the toy version of Nitpick) and some tests; a small step towards making the Nitpick tests take less time

use Future.fork rather than Thread.fork, so that the thread is part of the global thread management

fix editor

merged

merged

tidied using inductive_simps

NEWS

removed ancient constdefs command

put expand_(fun/set)_eq back in as synonyms, for compatibility

set up Nil and Cons to work as fixrec patterns

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;