merged

adding an example with integers and String.literals

adding an example to show how code_pred must be invoked with locales

removing report from the arguments of the quickcheck functions and refering to it by picking it from the context

changing the container for the quickcheck options to a generic data

Tidied up proofs using sledgehammer, also deleting unnecessary semicolons

changing String.literal to a type instead of a datatype

increasing the number of iterations to ensure to find a counterexample by random generation

only conceal primitive definition theorems, not predicate names

merged

modernized primrec

Markup_Tree is already scalable;

Isabelle_Markup.tooltip: explicit indication of ML;

Future.promise: more robust treatment of concurrent abort vs. fulfill (amending 047c96f41455);

primitive use_text: let interrupts pass unhindered;

Isabelle.load_icon with some sanity checks;

ML_Compiler.eval: reported positions need to contain offset, to avoid displaced reports due to synthesized line numbers;

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;