'example_proof' is treated as non-schematic statement with irrelevant proof (NB: even regular proofs can contain unreachable parts wrt. the graph of proof promises);

continue after failed commands;

added Keyword.is_heading (cf. Scala version); tuned;

updated keywords;

mark 'cd' and 'commit' as control command -- not usable in asynchronous document model, likely to cause confusion in Proof General;

somewhat more uniform timing markup in ML vs. Scala;

somewhat more uniform timing in ML vs. Scala;

added Markup.Double, Markup.Double_Property; tuned;

explicit "timing" status for toplevel transactions;

tuned;

tuned comments;

abolished obscure goal variant of [split_format] -- unused (cf. d1c14898fd04), unrelated to '(complete)' variant, and not at all canonical

moved ISABELLE_IDENTIFIER from ISABELLE_OUTPUT further up to ISABELLE_HOME_USER;

updated keywords;

reflect actual content of /home/isabelle/.html-data/cgi-bin/hgwebdir.cgi;

eliminated spurious "firstline" filters for improved display of Isabelle history logs: one item per line, without special headline; more uniform shortlogentry and filelogentry;

reflect actual content of /home/isabelle-repository/hgweb-templates/isabelle by krauss;

obsolete -- python installation on www4 is not modified (despite remaining "firstline" in graph and syndication views);

explicit indication of some remaining violations of the Isabelle/ML interrupt model;

updated generated file, overwriting 55a1693affb6 whose content appears to be in the thy source already;

proper spelling; proper format;

merged

Extend convex analysis by Bogdan Grechuk

merged

fixed handling of theorem references such as "foo bar" (with quotes), "foo bar(2)", and "foo bar(2)"(2)

make Mirabelle work correctly if the prover (e.g. the SMT solver) returns no timing information

pass proper type to SMT_Builtin.is_builtin

remove " s" suffix since seconds are now implicit

ignore facts with only theory constants in them

cosmetics