2013-07-12 ago wenzelm tuned;
2013-07-12 ago wenzelm clarified execution: maintain running execs only, check "stable" separately via memo (again);
2013-07-12 ago wenzelm tuned signature;
2013-07-12 ago wenzelm clarified module name;
2013-07-11 ago wenzelm more explicit type Exec.context;
2013-07-11 ago wenzelm tuned signature;
2013-07-11 ago wenzelm strictly monotonic Document.update: avoid disruptive cancel_execution, merely discontinue_execution and cancel/terminate old execs individually;
2013-07-11 ago wenzelm tuned -- cleanup before publishing assignment;
2013-07-11 ago wenzelm more abstract types;
2013-07-11 ago wenzelm tuned;
2013-07-11 ago wenzelm disallow concurrent execution attempt explicitly -- it should never happen due to management of singleton execution;
2013-07-11 ago wenzelm more precise fact declarations -- fewer warnings;
2013-07-11 ago wenzelm global management of command execution fragments;
2013-07-11 ago wenzelm fully synchronized guard of running execution;
2013-07-11 ago nipkow merged
2013-07-11 ago nipkow added exercises
2013-07-11 ago smolkas optimize isar-proofs by trying different proof methods
2013-07-11 ago smolkas made SML/NJ happy
2013-07-11 ago smolkas tuned
2013-07-11 ago wenzelm tuned;
2013-07-11 ago wenzelm re-assign prints of unchanged eval only -- avoid crash of new_exec;
2013-07-11 ago wenzelm tuned -- refrain from odd optimization;
2013-07-11 ago wenzelm tuned;
2013-07-10 ago wenzelm added "echo" command for demonstration purposes;
2013-07-10 ago wenzelm more abstract message channel;
2013-07-10 ago wenzelm explicit shutdown of message output thread;
2013-07-10 ago wenzelm tuned signature;
2013-07-10 ago wenzelm no need for raw stdin;
2013-07-10 ago wenzelm fall back on synchronous message output for single-threaded SML/NJ;
2013-07-10 ago wenzelm make SML/NJ happy;
2013-07-10 ago wenzelm retain main thread for protocol loop -- no access to raw ML toplevel;
2013-07-10 ago wenzelm removed historic dimacs2hol (see also read_dimacs_cnf_file in src/HOL/Tools/sat_solver.ML);
2013-07-10 ago wenzelm less intrusive token_range rendering, which is relevant for inner parse errors;
2013-07-10 ago smolkas made SML/NJ happy
2013-07-10 ago wenzelm merged
2013-07-10 ago wenzelm tuned start_execution: avoid sleep on worker thread;
2013-07-10 ago wenzelm print "persistent" flag allows to adjust tradeoff of ML run-time vs. JVM heap-space;
2013-07-10 ago wenzelm allow to remove print functions;
2013-07-10 ago wenzelm clarified Command.print: update old prints here;
2013-07-09 ago wenzelm produce print_execs assignment earlier during last_common phase (referring to current command_id, not prev);
2013-07-09 ago wenzelm tuned;
2013-07-09 ago wenzelm tuned proofs;
2013-07-09 ago wenzelm more formal type assign_update: avoid duplicate results and redundant update of global State.execs;
2013-07-09 ago wenzelm tuned message;
2013-07-09 ago wenzelm tuned signature -- NB: Command.read is actually part of Command.eval;
2013-07-09 ago wenzelm tuned protocol terminology;
2013-07-09 ago wenzelm tuned;
2013-07-08 ago wenzelm allow whitespace in file names;
2013-07-08 ago wenzelm tuned;
2013-07-08 ago wenzelm more direct interleaving of eval/print and update/execution -- refrain from crude manipulation of max_threads;
2013-07-08 ago wenzelm allow worker guest threads, which participate actively in future joins, but are outside thread accounting;
2013-07-10 ago smolkas made SML/NJ happy
2013-07-09 ago smolkas completely rewrote SH compress; added two parameters for experimentation/fine grained control
2013-07-09 ago smolkas moved code -> easier debugging
2013-07-08 ago nipkow tuned proofs
2013-07-07 ago wenzelm some support for Cygwin;
2013-07-07 ago wenzelm reduced number of old manuals: chapter HOL is back again to the Logics manual by Larry;
2013-07-07 ago wenzelm tuned signature;
2013-07-07 ago wenzelm discontinued obsolete "isabelle print";
2013-07-07 ago wenzelm discontinued command 'print_drafts';