async_state: report within proper transaction context;

merged

simplified representation of monad type

attempt to reconstruct missing HOL/Codegenerator_Test/ROOT.ML;

merged

updated document

dropped passed irregular names

adapt Nitpick to "prod_case" and "*" -> "sum" renaming; the code in "Nitpick_Preproc", which sorted the types using "typ_ord", was wrong and evil; it seems to have worked only because "*" was called "*"

remove needless signature entry

references to ghc and ocaml

explicit code_datatype declaration prevents multiple instantiations later on

refrain from using datatype declaration -- opens chance for quickcheck later on

tuned proof

reverted to verion from fc27be4c6b1c

traceback for error messages

accomodate for different behvaiour of nitpick (c.f. also 180e80b4eac1)

introduced distinct session HOL-Codegenerator_Test

tuned bootstrap files

remove codegeneration-related theories from big library theory

drop unconvenient code declarations

build image for session HOL-Library; introduced distinct session HOL-Codegenerator_Test

general Future.report -- also for Toplevel.async_state;

simplified Isabelle_Process.Result: use markup directly;

run_command: actually observe "print" flag;

Toplevel.run_command: asynchronous state output, as an attempt to address potentially slow pretty printing (e.g. in HOL/Bali);

more precise timing;

more efficient document model/view -- avoid repeated iteration over commands from start, prefer bulk operations; misc tuning;

standard argument order; tuned;

do not open auxiliary ML structures; misc tuning;

tuned white space;