type Path.binding may be empty: check later via proper_binding;
clarified 'export_prefix' default;

tuned signature;

tuned signature;

clarified signature: more explicit type Path.binding;
tuned;

tuned signature -- more operations;

clarified signature: Path.T as in Generated_Files;

updated tagging for 9 theories: Cross3, Determinants, Tagged_Division, Change_of_Vars, Extended_Real_Limits, Fashoda, Finite_Cartesian_Product, Function_Topology, Finite_Product_Measure

clarified signature;

clarified Path.check_elem;

reject further illegal chars according to https://docs.microsoft.com/en-us/windows/desktop/fileio/naming-a-file

tuned;

more strict check: avoid confusion of Path.basic with Path.current / Path.parent;

tuned;

update LTS Haskell version

--HG--
extra : amend_source : 77f438b7e2076ee3c2fe3ac2fd48943c470fc174

more general command 'generate_file' for registered file types, notably Haskell;
discontinued 'generate_haskell_file', 'export_haskell_file';
eliminated generated sources: compile files in tmp dir;

clarified signature;

smart_implode "$AFP" as well;

clarified take/drop/chop prefix/suffix;

tuned signature;

careful export of type-dependent functions, without losing their special status;

clarified modules;
tuned signature;

renamed Pretty.str_of to Pretty.unformatted_string_of to emphasize its meaning;

added Path.decode in ML, in correspondence to Path.encode in Scala;

explicit 'document_files' in session ROOT specifications;
clarified Isabelle_System.copy_file(_base): preserve file-attributes and local directory hierarchy;

even smarter Path.smart_implode;

clarified Path.smart_implode;
more informative report and rendering;

check_tool wrt. official ISABELLE_TOOLS;
added Path.split (cf. Scala version);

tuned messages;

Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;

tuned comment;

reject path variable nesting explicitly;

disallow quotes in path specifications -- extra paranoia;

USER_HOME settings variable points to cross-platform user home directory;

separate module for concrete Isabelle markup;

--HG--
rename : src/Pure/General/markup.ML => src/Pure/General/isabelle_markup.ML
rename : src/Pure/General/markup.scala => src/Pure/General/isabelle_markup.scala

more symbolic file positions via smart replacement of ISABELLE_HOME -- allows Isabelle distribution to be moved later on;

allow "$" within basic path elements (NB: initial "$" refers to path variable);

getenv_strict in ML;
tuned;

tuned comments;

proper Path.print;

print Path.T with some markup;

Path.print is the official way to show file-system paths to users -- note that Path.implode often indicates violation of the abstract datatype;

renamed raw "explode" function to "raw_explode" to emphasize its meaning;

support named_root, which approximates UNC server prefix (for Cygwin);
tuned representation: reversed elements;
misc simplification and cleanup;

normalized uncurry take/drop

--HG--
extra : rebase_source : 647c8b5a6641f0eef6d4d81646474d16388f9fb9

curried take/drop

--HG--
extra : rebase_source : 6e6b508d936640bef00f0ad0c4fb089ad5253ef0

curried inter as canonical list operation (beware of argument order)

dropped redundant gen_ prefix

replaced old_style infixes eq_set, subset, union, inter and variants by generic versions

removed Ids;

renamed Position.path to Path.position;

tuned signature;

moved Path.position to Position.path;

avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;

tuned basic list operators (flat, maps, map_filter);

avoid polymorphic equality;

expand: error on undefined/empty env variable;
tuned;

Move towards standard functions.

Deleted Library.option type.

Merged in license change from Isabelle2004

added split_ext; removed drop_ext;

GPLed;

added drop_ext;
tuned;

added position;

added is_current;

added make, dir;

val appends: T list -> T;

check_elem: allow ~, except for '~' and '~~';

enabled sig;

more abstract implementation;

fixed titles;

moved Thy/path.ML to General/path.ML;