clarified signature;

clarified breakgain: keeping it constant avoids margin fluctuation in Pretty_Tooltip vs. Pretty_Text_Area;

tuned;

proper type;
tuned;

more robust pretty printing: permissive treatment of bad values;

clarified length of block with pre-existant forced breaks;

unused;

tuned;

more explicit Pretty.Tree, like in ML;
tuned;

tuned;

tuned signature;

support for blocks with consistent breaks;
tuned;

support pretty break indent, like underlying ML systems;

tuned signature;

tuned imports;

ghost bullet via markup, which is painted as bar under text (normally space);

basic support for Pretty.item, which is considered as logical markup and interpreted in Isabelle/Scala, but ignored elsewhere (TTY, latex etc.);

maintain integer indentation during formatting -- it needs to be implemented by repeated spaces eventually;
always round block indentation upwards, to ensure that text moves visually to the right of the "hanging" part;

tuned;

tuned signature;

allow fractional pretty margin -- avoid premature rounding;

more explicit Pretty.Metric, with clear distinction of unit (space width) vs. average char width (for visual adjustments) -- NB: Pretty formatting works via full space characters (despite a981a5c8a505 and 70f7483df9cb);
separate JEdit_Lib.pretty_metric, with slightly closer imitation of jEdit;

proper metric for blanks -- NB: 70f7483df9cb discontinues coincidence of char_width with space width;

eliminated char_width_int to avoid unclear rounding;
clarified integer conversion for margin;

more uniform Pretty.char_width;

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

further refinement of jEdit line range, avoiding lack of final \n;

refined separator: FBreak needs to be free for proper breaking, extra space at end helps to work around last-line oddity in jEdit;

turn constraints into Isabelle_Markup.typing, depending on show_markup options;
proper recursion in standard_format;

tuned;

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

tuned rendering;

tuned signature;

some actual rich text markup via XML.content_markup;
tuned signature;

some support for inital command markup;
tuned signature;

clarified separated_chunks vs. space_explode;

tuned signature -- make Pretty less dependent on Symbol;

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 private stuff;

tuned signature;

Pretty: tuned markup objects;

tuned signatures;

more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
added convenient Markup.Int/Long objects (Scala);
simplified "assign" message format -- explicit version id;
misc tuning and simplification;

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;

Pretty.string_of (in Scala): actually observe margin/metric;

clarified Pretty.font_metrics;

tuned;

more precise pretty printing based on actual font metrics;
removed obsolete relative margin;

static Symbol.spaces;

unified/simplified Pretty.margin_default;
discontinued special Pretty.setmargin etc;
explicit margin argument for Pretty.string_of_margin etc.;

unformatted output;

Pretty.formatted operates directly on XML trees, treating XML.Elem like a pro-forma block of indentation 0, like the ML version;
tuned;

replaced slightly odd fbreak markup by plain "\n", which also coincides with regular linebreaks produced outside the ML pretty engine;

basic formatting of pretty trees;
line-up ML vs. Scala sources;

basic support for symbolic pretty printing;
tuned;