| 2022-09-08 |
wenzelm |
support Pretty.unformatted, similar to ML version;
|
file |
diff |
annotate
|
| 2022-08-22 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| 2022-04-01 |
wenzelm |
clarified formatting, for the sake of scala3;
|
file |
diff |
annotate
|
| 2021-03-04 |
wenzelm |
tuned --- fewer warnings;
|
file |
diff |
annotate
|
| 2020-04-22 |
wenzelm |
tuned signature -- avoid warnings;
|
file |
diff |
annotate
|
| 2020-03-27 |
wenzelm |
misc tuning based on hints by IntelliJ IDEA;
|
file |
diff |
annotate
|
| 2019-03-05 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 2018-03-17 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| 2018-01-30 |
wenzelm |
clarified breakgain: keeping it constant avoids margin fluctuation in Pretty_Tooltip vs. Pretty_Text_Area;
|
file |
diff |
annotate
|
| 2017-03-06 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 2016-04-02 |
wenzelm |
proper type;
|
file |
diff |
annotate
|
| 2016-04-01 |
wenzelm |
more robust pretty printing: permissive treatment of bad values;
|
file |
diff |
annotate
|
| 2015-12-21 |
wenzelm |
clarified length of block with pre-existant forced breaks;
|
file |
diff |
annotate
|
| 2015-12-20 |
wenzelm |
unused;
|
file |
diff |
annotate
|
| 2015-12-20 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 2015-12-19 |
wenzelm |
more explicit Pretty.Tree, like in ML;
|
file |
diff |
annotate
|
| 2015-12-19 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 2015-12-19 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| 2015-12-19 |
wenzelm |
support for blocks with consistent breaks;
|
file |
diff |
annotate
|
| 2015-12-17 |
wenzelm |
support pretty break indent, like underlying ML systems;
|
file |
diff |
annotate
|
| 2014-02-18 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| 2013-04-04 |
wenzelm |
tuned imports;
|
file |
diff |
annotate
|
| 2013-03-28 |
wenzelm |
ghost bullet via markup, which is painted as bar under text (normally space);
|
file |
diff |
annotate
|
| 2013-03-28 |
wenzelm |
basic support for Pretty.item, which is considered as logical markup and interpreted in Isabelle/Scala, but ignored elsewhere (TTY, latex etc.);
|
file |
diff |
annotate
|
| 2013-03-28 |
wenzelm |
maintain integer indentation during formatting -- it needs to be implemented by repeated spaces eventually;
|
file |
diff |
annotate
|
| 2013-03-28 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 2013-03-25 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| 2013-03-23 |
wenzelm |
allow fractional pretty margin -- avoid premature rounding;
|
file |
diff |
annotate
|
| 2013-03-23 |
wenzelm |
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);
|
file |
diff |
annotate
|
| 2013-03-21 |
wenzelm |
proper metric for blanks -- NB: 70f7483df9cb discontinues coincidence of char_width with space width;
|
file |
diff |
annotate
|
| 2013-03-21 |
wenzelm |
eliminated char_width_int to avoid unclear rounding;
|
file |
diff |
annotate
|
| 2013-01-12 |
wenzelm |
more uniform Pretty.char_width;
|
file |
diff |
annotate
|
| 2012-11-25 |
wenzelm |
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
|
file |
diff |
annotate
|
| 2012-10-12 |
wenzelm |
further refinement of jEdit line range, avoiding lack of final \n;
|
file |
diff |
annotate
|
| 2012-10-11 |
wenzelm |
refined separator: FBreak needs to be free for proper breaking, extra space at end helps to work around last-line oddity in jEdit;
|
file |
diff |
annotate
|
| 2012-09-29 |
wenzelm |
turn constraints into Isabelle_Markup.typing, depending on show_markup options;
|
file |
diff |
annotate
|
| 2012-09-28 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 2012-09-28 |
wenzelm |
support for wrapped XML elements, which allows to preserve full markup tree information in to_XML/from_XML conversion;
|
file |
diff |
annotate
|
| 2012-09-20 |
wenzelm |
tuned rendering;
|
file |
diff |
annotate
|
| 2012-09-20 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| 2012-09-18 |
wenzelm |
some actual rich text markup via XML.content_markup;
|
file |
diff |
annotate
|
| 2012-09-18 |
wenzelm |
some support for inital command markup;
|
file |
diff |
annotate
|
| 2012-08-29 |
wenzelm |
clarified separated_chunks vs. space_explode;
|
file |
diff |
annotate
|
| 2012-08-07 |
wenzelm |
tuned signature -- make Pretty less dependent on Symbol;
|
file |
diff |
annotate
|
| 2011-11-28 |
wenzelm |
separate module for concrete Isabelle markup;
|
file |
diff |
annotate
|
| 2011-10-22 |
wenzelm |
more private stuff;
|
file |
diff |
annotate
|
| 2011-07-09 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| 2010-08-25 |
wenzelm |
Pretty: tuned markup objects;
|
file |
diff |
annotate
|
| 2010-08-22 |
wenzelm |
tuned signatures;
|
file |
diff |
annotate
|
| 2010-08-14 |
wenzelm |
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
|
file |
diff |
annotate
|
| 2010-08-07 |
wenzelm |
simplified type XML.Tree: embed Markup directly, avoid slightly odd triple;
|
file |
diff |
annotate
|
| 2010-06-13 |
wenzelm |
Pretty.string_of (in Scala): actually observe margin/metric;
|
file |
diff |
annotate
|
| 2010-05-12 |
wenzelm |
clarified Pretty.font_metrics;
|
file |
diff |
annotate
|
| 2010-05-12 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 2010-05-11 |
wenzelm |
more precise pretty printing based on actual font metrics;
|
file |
diff |
annotate
|
| 2010-05-09 |
wenzelm |
static Symbol.spaces;
|
file |
diff |
annotate
|
| 2010-05-08 |
wenzelm |
unified/simplified Pretty.margin_default;
|
file |
diff |
annotate
|
| 2010-05-07 |
wenzelm |
unformatted output;
|
file |
diff |
annotate
|
| 2010-05-07 |
wenzelm |
Pretty.formatted operates directly on XML trees, treating XML.Elem like a pro-forma block of indentation 0, like the ML version;
|
file |
diff |
annotate
|
| 2010-05-06 |
wenzelm |
replaced slightly odd fbreak markup by plain "\n", which also coincides with regular linebreaks produced outside the ML pretty engine;
|
file |
diff |
annotate
|