more tight HTML output: avoid extra lines within <pre>;

HTML output for Markdown elements;
clarified HTML operations;

HTML rendering of \<^control> as in Isabelle/jEdit;

tuned signature;

more operations/options;

clarified signature;

clarified defaults;

GUI layout similar to Pure/GUI/wrap_panel.scala;

some HTML GUI elements;

HTML preview based on PIDE markup;

permissive output of XML.Text, e.g. relevant for embedded <style>;

uniform notion of Symbol.is_controllable (see also 265d9300d523);

proper markup for IsabelleText font;

generate CSS for Isabelle fonts;

tuned signature;

tuned signature;

output control symbols like ML version, with optionally hidden source;

tuned signature;

tuned signature;

tuned;

uniform output of HTML as XML;
discontinued special cases of 041dc6d8d344;

modernized generated HTML;

tuned signature;

tuned signature;

tuned signature;

clarified signature;

tuned layout;

support for message underline and tooltips;

clarified signature;

HTML rendering based on Isabelle/jEdit colors;

tuned signature;

more systematic HTML.init_dir with css;

extra space only for some structual elements, but not <a>, <b>, <em> etc. (amending 8a0fe5469ba0);

clarified image size;

make index formally within Isabelle/Scala;

more operations;
tuned;

more readable output: whitespace is insignificant in HTML;

more operations;

tuned;

support for XML as HTML;
tuned;

tuned -- according to ML version;

clarified symbol insertion, depending on buffer encoding;

less ambitious collection of quasi-generic PIDE modules;

encode text with control symbols;

misc tuning, based on warnings by IntelliJ IDEA;

clarified PIDE modules;

tuned imports;

tuned imports;

adjust modules for Admin/build jars_test;

include session description in chapter index;
prefer alphabetical order;

discontinued "isabelle usedir" option -r (reset session path);
simplified internal session identification: chapter / name;
clarified chapter index (of sessions) vs. session index (of theories);
discontinued "up" links, for improved modularity also wrt. partial browser_info (users can use "back" within the browser);
removed obsolete session parent_path;

maintain session index on Scala side, for more determistic results;
removed unused HTML operations;

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

support for wrapped XML elements, which allows to preserve full markup tree information in to_XML/from_XML conversion;

removed obsolete org.w3c.dom operations;

discontinued specific entity markup, which causes confusion with "kind" names with spaces (e.g. "type name");
uniform treatment of "class" entities in input and output;

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

some convenience actions/shortcuts for control symbols;

simplified Symbol based on lazy Symbol.Interpretation -- reduced odd "functorial style";
tuned implicit build/init messages;

simplified Symbol.iterator: produce strings, which are mostly preallocated;
eliminated Symbol.CharSequence complications;

quasi-static Isabelle_System -- reduced tendency towards "functorial style";

type classes: entity markup instead of old-style token markup;

clarified decoded control symbols;

more uniform treatment of recode_set/recode_map;
HTML spans with user fonts;

tuned iteration over short symbols;

tuned;

discontinued special treatment of \<^loc> (which was original meant as workaround for "local" syntax);

some unicode chars for special control symbols;

tuned signatures;

HTML.spans: explicit flag for preservation of original data (which would be turned into org.w3c.dom user data in XML.document_node);

simplified some Markup;

simplified type XML.Tree: embed Markup directly, avoid slightly odd triple;
XML.cache_tree: actually store XML.Text as well;
added Isabelle_Process.Result.properties;

added HTML.encode (in Scala), similar to HTML.output in ML;

recovered StringBuilder functionality after subtle change of + and ++ in Scala 2.8.0 Beta 1;

replaced some deprecated methods;

adapted to Scala 2.8.0 Beta1 -- with notable changes to scala.collection;

refined some Symbol operations/signatures;
added Symbol.Matcher;
flexible Scan.Lexicon.symbols, with one/many/many1 variants;

sealed XML.Tree;
keep original XML.Tree within DOM as user data;

avoid lazy val with side-effects -- spurious null pointers!?

proper markup text for loc;

basic treatment of special control symbols;
misc tuning;

more robust treatment of line breaks -- Java "split" has off semantics;

Basic HTML output.