src/Pure/Thy/export.ML
13 months ago wenzelm 2018-05-13 clarified implicit compression;
13 months ago wenzelm 2018-05-11 more scalable API;
13 months ago wenzelm 2018-05-08 tuned signature;
13 months ago wenzelm 2018-05-07 more checks;
13 months ago wenzelm 2018-05-07 clarified signature; avoid pointless compression;
13 months ago wenzelm 2018-05-07 store exports within PIDE command state; Markup.Export.unapply: proper NAME;
13 months ago wenzelm 2018-05-06 tuned signature; clarified modules;