#
34f28eb1 |
|
17-Mar-2018 |
wenzelm <none@none> |
clarified signature;
|
#
4aa14774 |
|
30-Jan-2018 |
wenzelm <none@none> |
clarified breakgain: keeping it constant avoids margin fluctuation in Pretty_Tooltip vs. Pretty_Text_Area;
|
#
a5c4ec5b |
|
06-Mar-2017 |
wenzelm <none@none> |
tuned;
|
#
f505acad |
|
02-Apr-2016 |
wenzelm <none@none> |
proper type; tuned;
|
#
75340e33 |
|
01-Apr-2016 |
wenzelm <none@none> |
more robust pretty printing: permissive treatment of bad values;
|
#
a90d9901 |
|
21-Dec-2015 |
wenzelm <none@none> |
clarified length of block with pre-existant forced breaks;
|
#
39cf4f1a |
|
19-Dec-2015 |
wenzelm <none@none> |
unused;
|
#
5eba3ab3 |
|
19-Dec-2015 |
wenzelm <none@none> |
tuned;
|
#
5f0352a5 |
|
19-Dec-2015 |
wenzelm <none@none> |
more explicit Pretty.Tree, like in ML; tuned;
|
#
f2177179 |
|
19-Dec-2015 |
wenzelm <none@none> |
tuned;
|
#
1ee5cc81 |
|
19-Dec-2015 |
wenzelm <none@none> |
tuned signature;
|
#
444e410d |
|
19-Dec-2015 |
wenzelm <none@none> |
support for blocks with consistent breaks; tuned;
|
#
a88302d7 |
|
17-Dec-2015 |
wenzelm <none@none> |
support pretty break indent, like underlying ML systems;
|
#
c97520e9 |
|
18-Feb-2014 |
wenzelm <none@none> |
tuned signature;
|
#
0a17500d |
|
04-Apr-2013 |
wenzelm <none@none> |
tuned imports;
|
#
18135dc4 |
|
28-Mar-2013 |
wenzelm <none@none> |
ghost bullet via markup, which is painted as bar under text (normally space);
|
#
96158914 |
|
28-Mar-2013 |
wenzelm <none@none> |
basic support for Pretty.item, which is considered as logical markup and interpreted in Isabelle/Scala, but ignored elsewhere (TTY, latex etc.);
|
#
cbec6210 |
|
28-Mar-2013 |
wenzelm <none@none> |
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;
|
#
8e101ca4 |
|
28-Mar-2013 |
wenzelm <none@none> |
tuned;
|
#
6a8629fc |
|
25-Mar-2013 |
wenzelm <none@none> |
tuned signature;
|
#
cf2b9111 |
|
23-Mar-2013 |
wenzelm <none@none> |
allow fractional pretty margin -- avoid premature rounding;
|
#
9d81aab6 |
|
23-Mar-2013 |
wenzelm <none@none> |
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;
|
#
e2412726 |
|
21-Mar-2013 |
wenzelm <none@none> |
proper metric for blanks -- NB: 70f7483df9cb discontinues coincidence of char_width with space width;
|
#
c14ff302 |
|
21-Mar-2013 |
wenzelm <none@none> |
eliminated char_width_int to avoid unclear rounding; clarified integer conversion for margin;
|
#
71c18c31 |
|
12-Jan-2013 |
wenzelm <none@none> |
more uniform Pretty.char_width;
|
#
95d64a2f |
|
25-Nov-2012 |
wenzelm <none@none> |
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
|
#
bb302c09 |
|
12-Oct-2012 |
wenzelm <none@none> |
further refinement of jEdit line range, avoiding lack of final \n;
|
#
b977866d |
|
11-Oct-2012 |
wenzelm <none@none> |
refined separator: FBreak needs to be free for proper breaking, extra space at end helps to work around last-line oddity in jEdit;
|
#
0707cca3 |
|
29-Sep-2012 |
wenzelm <none@none> |
turn constraints into Isabelle_Markup.typing, depending on show_markup options; proper recursion in standard_format;
|
#
bab54651 |
|
28-Sep-2012 |
wenzelm <none@none> |
tuned;
|
#
70369ac4 |
|
28-Sep-2012 |
wenzelm <none@none> |
support for wrapped XML elements, which allows to preserve full markup tree information in to_XML/from_XML conversion;
|
#
30236237 |
|
20-Sep-2012 |
wenzelm <none@none> |
tuned rendering;
|
#
27431ee4 |
|
20-Sep-2012 |
wenzelm <none@none> |
tuned signature;
|
#
603e40fa |
|
18-Sep-2012 |
wenzelm <none@none> |
some actual rich text markup via XML.content_markup; tuned signature;
|
#
81c0cb97 |
|
18-Sep-2012 |
wenzelm <none@none> |
some support for inital command markup; tuned signature;
|
#
3135256d |
|
28-Aug-2012 |
wenzelm <none@none> |
clarified separated_chunks vs. space_explode;
|
#
c9b64eed |
|
06-Aug-2012 |
wenzelm <none@none> |
tuned signature -- make Pretty less dependent on Symbol;
|
#
99fd6f8e |
|
28-Nov-2011 |
wenzelm <none@none> |
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
|
#
b8663317 |
|
22-Oct-2011 |
wenzelm <none@none> |
more private stuff;
|
#
16933a60 |
|
08-Jul-2011 |
wenzelm <none@none> |
tuned signature;
|
#
f9b0ab5e |
|
25-Aug-2010 |
wenzelm <none@none> |
Pretty: tuned markup objects;
|
#
0e6f763c |
|
22-Aug-2010 |
wenzelm <none@none> |
tuned signatures;
|
#
30347bc0 |
|
14-Aug-2010 |
wenzelm <none@none> |
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;
|
#
16b11fcc |
|
07-Aug-2010 |
wenzelm <none@none> |
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;
|
#
dddbeb22 |
|
13-Jun-2010 |
wenzelm <none@none> |
Pretty.string_of (in Scala): actually observe margin/metric;
|
#
456e6e1d |
|
11-May-2010 |
wenzelm <none@none> |
clarified Pretty.font_metrics;
|
#
163f95a4 |
|
12-May-2010 |
wenzelm <none@none> |
tuned;
|
#
f3a6f2ca |
|
11-May-2010 |
wenzelm <none@none> |
more precise pretty printing based on actual font metrics; removed obsolete relative margin;
|
#
631d20c8 |
|
09-May-2010 |
wenzelm <none@none> |
static Symbol.spaces;
|
#
e8b34bd4 |
|
08-May-2010 |
wenzelm <none@none> |
unified/simplified Pretty.margin_default; discontinued special Pretty.setmargin etc; explicit margin argument for Pretty.string_of_margin etc.;
|
#
f4b0b5a2 |
|
07-May-2010 |
wenzelm <none@none> |
unformatted output;
|
#
c9fead59 |
|
07-May-2010 |
wenzelm <none@none> |
Pretty.formatted operates directly on XML trees, treating XML.Elem like a pro-forma block of indentation 0, like the ML version; tuned;
|
#
c9721cff |
|
06-May-2010 |
wenzelm <none@none> |
replaced slightly odd fbreak markup by plain "\n", which also coincides with regular linebreaks produced outside the ML pretty engine;
|
#
853cb7db |
|
06-May-2010 |
wenzelm <none@none> |
basic formatting of pretty trees; line-up ML vs. Scala sources;
|
#
85780ec8 |
|
06-May-2010 |
wenzelm <none@none> |
basic support for symbolic pretty printing; tuned;
|