added Future.promise/fulfill -- promised futures that are fulfilled by external means; Future.value: official result assignment -- produces immutable ref; Future.shutdown: raw_wait keeps raw task attributes, e.g. asynchronous interrupts of toplevel; Task_Queue: passive tasks track dependencies, but lack any evaluation process; tuned;

Basic edits on plain text.

recovered legacy settings for Proof General 3.x;

merged

merged

avoid exporting Type.build_tsig

repaired legacy setting variable

merged

more correct handling of empty functions

separate module Thy_Syntax for command span parsing;

more accurate scanning of bad input;

added filter_proper parameter; added eof; added command_span;

more token discriminators;

tuned message;

tuned;

added Promise.fulfill_result;

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