proper install_fonts;

proper jvmpath for Windows;

basic integration of graphview into document model; added Graph_Dockable; updated Isabelle/jEdit authors and dependencies etc.;

ML support for generic graph display, with browser and graphview backends (via print modes); reverse graph layout (again), according to the graph orientation provided by ML; simplified scala types -- eliminated unused type parameters; more explicit Model.Info, Model.Graph; renamed isabelle.graphview.Graphview_Frame to isabelle.graphview.Frame in accordance to file name; removed obsolete Graph_XML and Tooltips; tuned graphview command line; more generous JVM resources via GRAPHVIEW_JAVA_OPTIONS;

tuned;

more complete build; added option -c to imitate old browser;

proper error message;

separate module Graph_Display; tuned signature;

added graph encode/decode operations; tuned signature;

tuned;

minimal component and build setup for graphview;

added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;

made smlnj even happier

tuned proofs;

more explicit keyword1/keyword2 markup -- avoid potential conflict with input token markup produced by Token_Marker;

updated checksum, which appears to have changed accidentally;

updated to exec_process-1.0.2;

search bash via PATH as usual (this is no longer restricted to Cygwin with its known file-system layout);

discontinued futile attempt to hardwire build options into the image, sequential mode is enabled more robustly at runtime (cf. 3b0a60eee56e);

Mirabelle appears to work better in single-threaded mode;

generalized types

tuned termination proof

adapted examples to new names

renamed coinduction principles to have "dtor" in the name

renamed "set_incl" etc. to have "ctor" or "dtor" in the name

renamed low-level "map_unique" to have "ctor" or "dtor" in the name

renamed low-level "set_simps" and "set_induct" to have "ctor" or "dtor" in the name

renamed "map_simps" to "{c,d}tor_maps"

took out accidentally submitted "tracing" calls

fixed bug in "fold" tactic with nested products (beyond the sum of product corresponding to constructors)

simplified fact policies

generate "rel_as_srel" and "rel_flip" properties

started work on generation of "rel" theorems

make smlnj happy

more strict typscheme_equiv check: must fix variables of more specific type; dropped dead code; tuned order

cache should not contain material from descendant theory

some PIDE NEWS from this summer;

tuned whitespace;

tuned;

tuned proofs;

report proper binding positions only -- avoid swamping document model with unspecific information;

accumulate under exec_id as well;

more restrictive pattern, to avoid malformed positions intruding the command range (cf. d7a1973b063c);

misc tuning;

Thy_Syntax.consolidate_spans is subject to editor_reparse_limit, for improved experience of unbalanced comments etc.;

tuned signature;

tuned proofs;

misc tuning;

tighten margin for TextArea instead of Lobo;

misc tuning;

renamed LFP low-level rel property to have ctor not dtor in its name

changed base session for "HOL-BNF" for faster building in the typical case

renamed "rel_simp" to "dtor_rel" and similarly for "srel"

fixed a few names that escaped the renaming

tuned whitespace

merged

clean up lemmas used for composition

created separate session "HOL-BNF-LFP" as a step towards eventual integration in "HOL" in the middle term

renamed "Codatatype" directory "BNF" (and corresponding session) -- this opens the door to no-nonsense session names like "HOL-BNF-LFP"

renamed top-level theory from "Codatatype" to "BNF"