pass build error code;

tuned isatest ML_OPTIONS;

merged

a primitive scala serializer

fixed type error;

remove overloaded star operator, use specific vector / matrix operators

finite annotation on cartesian product is now implicit.

added syntax translation to automatically add finite typeclass to index type of cartesian product type

Made finite cartesian products finite

reduced arity of Nitpick selectors associated with sets by 1, by using "Formula" instead of "Atom 2"

make Nitpick's tests not leave files in the temp directory

more text edit operations;

always report updates -- required has "handshake";

tuned Isabelle/Scala build;

simplified build/bootstrap of graph browser -- avoid make;

simplified build/bootstrap of Isabelle/Scala components -- avoid make;

more robust cancelation, notably of passive futures without scheduler running;

eliminated cache, which complicates the code without making a real difference (NB: deque_towards often disrupts caching, and daisy-chaining of workers already reduces queue overhead);

tasks of canceled groups are considered "ready" -- enables to purge the queue from tasks depending on unfinished promises (also improves general reactivity); shutdown: back to synchronous wait, which means no asynchronous interrupts within the loop;

do not memoize interrupts; actually memoize results in sequential version; tuned;

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;