centralized upper/lowercase name mangling

optional case enforcement

obsolete: no symbol identifiers remaining in Pure

prevent subscription in nested contexts explicitly -- at foundational and user level

cleanup

NEWS

use qualified name (was interpreted as a catch-all variable name)

add additional check to avoid selector formula right-hand side consisting of a nullary constructor getting interpreted as a discriminator formula

updated keywords;

clarified signature: load_file is still required internally;

merged

some support for session-qualified theories: allow to refer to resources via qualified name instead of odd file-system path;

support for long names in Scala;

tuned;

Discontinued old spark_open; spark_open_siv is now spark_open

suppress slightly odd completions of "real";

tuned proofs;

tuned proofs;

clarified exit sequence: prover is reset afterwards, no more output messages;

more synchronized treatment of prover process, which might emit more messages before shutdown and requires manager to accept them;

tuned;

some sanity checks for Isabelle sources;

prefer plain ASCII / latex over not-so-universal Unicode;

tuned whitespace;

proper Unix line termination;

require explicit 'document_files';

updated mkroot;

basic support for Mercurial command line tools;

clarified;

ignore malformed file names outright, e.g. .class files with dollar;

more systematic Isabelle output, like in classic Isabelle/ML (without markup);

systematic replacement of 'files' by 'document_files';

tuned signature -- accomodate operations of ROOT files;

tuned -- prefer Isabelle/Scala operations;

tuned proofs;

tuned;

tuned proofs;

improved syslog performance -- avoid denial-of-service e.g. with threads_trace = 5 and active Syslog dockable;

tuned -- fewer aliases of critical operations;

removed dead code; tuned comments;

tuned comments;

more systematic delay_first discipline for change_buffer and prune_history;

mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;

tuned;

added Scala version of module Event_Timer;

restored naming trick

more reliable 'name_of_bnf'

cleaner 'rel_inject' theorems

modernized Isabelle classpath for graphview;

tuned;

merged

NEWS;

tuned message;

proper handling of shared zoom component: update layout dynamically;

PIDE support for find_consts;

some rearrangements to support multiple find operations;

tuned;

clarified GUI focus;

actually observe search limit;

misc tuning;

uniform focus traversal via TAB / Shift-TAB for all fields, in contrast to Java defaults, but in accordance to occasional jEdit practice;

tuned GUI events;

tuned;

tuned spelling;

clarified PIDE modules;

clarified;

tuned signature;

tuned imports;

tuned headers;

tuned signature;

more complete classical rules for Inf and Sup, modelled after theiry counterparts on Inter and Union (and INF and SUP)

subsumed by existing default simp rules for functions and booleans

tuned

avoid non-standard simp default rule

retired wwwfind

use right set of variables for recursive check

merged

tuned -- potentially more robust;

suppress potential dangerous option (see 1baa5d19ac44);

manager is direct receiver of prover output -- discontinued old performance tuning (329320fc88df, 1baa5d19ac44);

modernized theory setup;

just one default thread pool (which is hardwired to Runtime.availableProcessors);

tuned signature -- separate pool for JFuture tasks, which can be canceled;

prefer Isabelle/Scala operations;

unused;

use Z3 4.3.2 to fix most FIXMEs

added Z3 4.3.2 (unstable) component

updated Z3 version number

use Z3 4.3.2 syntax

subscription as target-specific implementation device

make SML/NJ happier;

merged

updated properties for scala.concurrent.ExecutionContext.Implicits.global (future task farm), similar to Isabelle/ML; removed obsolete properties for old actors;

simplified change_buffer (again, see 937826d702d5): no thread, just timer, rely on asynchronous commands_changed.post;

replaced manager Actor by Consumer_Thread, which is lazy to defer its start to actual Handler init time;

tuned whitespace;