slightly shorter tail (again) -- theory loader produces less warning spam (cf. 2524c1bbd087);

kill failed theories in reverse order -- avoids cascaded warnings;

discontinued old TheoryDataFun, but retain Theory_Data_PP with is Pretty.pp argument to merge (still required in exotic situations -- hard to get rid of);

Standard_System.raw_exec; more robust root.mkdirs;

removed function "isabelle-process", keeping "isabelle" only -- functions within the process environment might get passed through a genuine /bin/sh, which does not allow non-identifiers here;

added Cygwin "make" package;

discontinued old ISABELLE and ISATOOL environment settings;

shell functions "isabelle-process" and "isabelle" refer to the proper executables statically -- for interactive use or sloppy bash scripts;

removed further remains of mutable theory data (cf. 25bd3ed2ac9f);

merged

code cache only persists on equal theories

moved name duplicates to end of theory; reduced warning noise

merged

modernized

added applify combinator

dropped redundant name declarations

dropped copy operation for legacy TheoryDataFun

code cache without copy; tuned

report keywords as singleton messages, control message kind via print mode;

explicit markup of document assigment message (simplified variant of earlier "edits" 8c3e1f73953d);

omit useless (?) scaladoc;

added Future.promise -- essentially a single-assignment variable with signalling, using the Future interface;

after_qed: refrain from Position.setmp_thread_data, which causes duplication of results with several independent proof attempts;

discontinued special HOL_USEDIR_OPTIONS;

updated stats;

made SML/NJ happy;

merged

removed legacy asm_lr_simp_tac

removed more asm_rl's - unfortunately slowdown of 1 min.

new year's resolution: reindented code in function package

provide simp and induct rules in Function.info

more official data record Function.info

simplified

absorb structures Decompose and Descent into Termination, to simplify further restructuring

another legacy "asm_lr"

merged

removed legacy asm_lr

merged

added lemmas

added lemma

removed FIXME

tuned error handling;

Standard_System.raw_execute: optional cwd; basic Cygwin.setup with download and unattended installation;

Download URLs -- with progress monitor.

Future values -- Scala version.

added simple dialogs;

added is_ready;

simplified init message -- removed redundant session property;

removed obsolete version check -- sanity delegated to Isabelle_System; tuned;

eliminated Markup.edits/EDITS: Isar.edit_document reports Markup.edit/EDIT while running under new document id; eliminated ML interface of Isar_Document: the protocol only works with certain transaction positions, i.e. via Isar commands;

tuned signature;

less ambitious isatest for SML/NJ;

killed a few warnings

more regular axiom of infinity, with no (indirect) reference to overloaded constants

back to Unsynchronized.ref, with some attempts to make the main operations actually thread-safe;

removed slightly odd Isar_Document.init; simplified begin_document: associate empty command/state with no_id, which is implicit start; replaced make_id by create_id (cf. Scala version); eliminated CRITICAL/Unsynchronized.ref in favour of Synchronized.var; tuned;

explicit session HOL-Proofs -- avoid statefulness of main HOL image wrt. HOL_proofs etc.;

tuned;

crude Cygwin.setup;

ignore undefined environment;

separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);

tuned;

system shutdown hook: strict kill;

moved Library.decode_permissive_utf8 to Isabelle_System; moved Library.with_tmp_file to Isabelle_System; added Isabelle_System.read_file/write_file; added Isabelle_System.system_out, with propagation of thread interrupts and process shutdown (global CTRL-C);