merged

explicit document_output directory, without implicit purge of default in ISABELLE_BROWSER_INFO;

more direct interpretation of document_variants for build (unchanged for usedir);

tone down "z3_tptp", now that Z3 (starting with 4.1) no longer supports TPTP TFF0

fixed then-else confusion

tweak Vampire setup in the light of new evaluation

improved set of reconstructor methods

warn users about unused "using" facts

be less aggressive at kicking out chained facts

recognize bus errors as crash

consider removing chained facts last, so that they're more likely to be kept

clarified format of etc/options: only declarations, not re-definitions;

check_errors for cumulative session content;

even more defensive path expansion (see also 8d381fdef898);

support for 'typ' with explicit sort constraint;

added jedit option -d;

always retain doc-src (as regular component);

merged

Calling isabelle with proper (relative) path, no longer relying on $PATH.

fewer workarounds for MacOS to increase chances that COMMAND ("META") key works with Java 1.7 from Oracle;

updated to jedit-4.5.2 (still unchanged);

restored ISABELLE_OUTPUT etc -- still relevant at least for mira.py itself

tuned;

fixed mira.py (cf. fd50596bf78b)

more direct embedding of abstract thm values into the ML environment -- avoidance of repeated ML_Thms.the_thm(s) considerably reduces compilation time for Poly/ML 5.4.x;

more static antiquotations;

always show some timing information, to reduce the need for explicit -v;

some information for central Isabelle repository configuration;

reduced settings patching

removed obsolete configuration AFP_images

faster compilation of ML with antiquotations: static ML_context is bound once in auxiliary structure Isabelle;

simplified symbol matching;

further clarification of malformed symbols;

more liberal scanning of potentially malformed symbols;

vacuous execution after first malformed command;

clarified Command.range vs. Command.proper_range according to Scala version, which is potentially relevant for command status markup;

tuned markup;

tuned message;

clarified "bad" markup: proper body text, invent missing serial on Scala side (counting backwards);

reports with body text, not just markup;

fixed "double rev" bug that arose in situations where a % comment arose on the last line of a file without \n at the end

special code with lists no longer necessary, use sets

proper error prefixes;

more precise recover_quoted, recover_verbatim, recover_comment (cf. ML version) -- NB: context parsers expect explicit termination;

tuned message;

clarified Linear_Set.next/prev: check definedness;

merged

Improved complete lattice formalisation - no more index set.

merged

tuned proofs;

sneak message into "bad" markup as property -- to be displayed after YXML parsing;

apply all text edits to each node, before determining the resulting doc_edits -- allow several iterations to consolidate spans etc.; expand Clear edit before sending to prover; at most one full reparse of each node;

clarified undefined, unparsed, unfinished command spans; common reparse_spans, diff_commands; some support for consolidate_spans after change of perspective;

tuned;

discontinued mostly unused markup for command spans;

more visible markup of malformed input as "bad";

tuned proofs

some attempts to keep malformed syntax errors focussed, without too much red spilled onto the document view;

refined recover_spans: take visible range into account, reparse and trim results -- to improve editing experience wrt. unbalanced quotations etc.; tuned signature;

tuned signature;

more direct Linear_Set.reverse, swapping orientation of the graph; tuned;

tuned signature;

tuned;

refined recovery of scan errors: longest prefix of delimited token after failure, otherwise just one symbol;

explicit FIXME;

tuned signature;

corrected header

refined isabelle mkroot; allow empty 'theories' to facilitate generated templates;

simplified session specifications: names are taken verbatim and current directory is default;

added build option -D: include session directory and select its sessions;

discontinued obsolete "isabelle makeall";

even more permissive approximation of master_dir, which is only required to access external resources ('uses' etc.);

back to implicit commit via isabelle-process -- save image only once (cf. 181b91e1d1c1);

proper axiomatization of "mem" -- do not leave it formally unspecified;

simplified Pure bootstrap -- separate pure_setup.ML was required for Alice/ML at some point;

more casual exit back to ML toplevel, to accomodate commit in SML/NJ which continues at the saved point;

obsolete;

eliminated obsolete ISABELLE_USEDIR_OPTIONS;

updated ML settings;

add legacy target for HOL-Probability, needed by AFP/Markov_Models

proper isabelle update_keywords tool;

configure Admin as component, with its own lib/Tools;

SOMEthing went utterly wrong in 5b51ccdc8623;

more legacy targets;

discontinued obsolete IsaMakefile and ROOT.ML files from the Isabelle distribution;

tuned;

proper quoting

merged

more structural parsing for minor modes; tuned signatures;

clarified Sidekick configuration, including minor modes;

stop distinguishing between complete and incomplete slices, since this is very fragile and has hardly any useful semantics to users

specify full path to clausifier

documentation

more token markers, based on actual outer syntax; prefer official Outer_Syntax.init with its completions;

simplified process startup phases: INIT suffices for is_ready;

need to expand path in order to resolve imports like "~~/src/Tools/Code_Generator";

prefer static Build.session_content for loaded theories -- discontinued incremental protocol;

prefer static Build.outer_syntax in Isabelle/Scala session -- discontinued incremental protocol; just one cumulative Keyword.status at end of batch session;

permissive outer syntax wrt. symbol recoding;

simplified Document.Node.Header -- internalized errors;

tuned signature;

tuned signature -- slightly more abstract text representation of prover process;

tuned signature -- make Pretty less dependent on Symbol;

extended Mirabelle to support user-provided setup files which contain the configuration for a Mirabelle run (avoids some layers of scripts and reduces the complexity of the overall Mirabelle setup)

increase defensive timeout that should typically not kick in thanks to solid time limits in Sledgehammer (otherwise, Mirabelle-based evaluations might be distorted)

documentation

added iProver(-Eq) local

optimized saving

pass Isabelle/Scala system options into ML process of Isar tty or build jobs;

merged

switching from Emacs.app to Aquamacs.app

switching from Emacs.app to Aquamacs.app