author | wenzelm |
Sat, 19 Dec 2015 19:07:14 +0100 | |
changeset 61868 | 8c0037ebab1a |
parent 61865 | 6dcc9e4f1aa6 |
child 61871 | 2cb4a2970941 |
permissions | -rw-r--r-- |
36683 | 1 |
/* Title: Pure/General/pretty.scala |
2 |
Author: Makarius |
|
3 |
||
36687 | 4 |
Generic pretty printing module. |
36683 | 5 |
*/ |
6 |
||
7 |
package isabelle |
|
8 |
||
9 |
||
10 |
object Pretty |
|
11 |
{ |
|
48704
85a3de10567d
tuned signature -- make Pretty less dependent on Symbol;
wenzelm
parents:
45666
diff
changeset
|
12 |
/* spaces */ |
85a3de10567d
tuned signature -- make Pretty less dependent on Symbol;
wenzelm
parents:
45666
diff
changeset
|
13 |
|
61865 | 14 |
def spaces(n: Int): XML.Body = |
15 |
if (n == 0) Nil |
|
16 |
else List(XML.Text(Symbol.spaces(n))) |
|
48704
85a3de10567d
tuned signature -- make Pretty less dependent on Symbol;
wenzelm
parents:
45666
diff
changeset
|
17 |
|
61865 | 18 |
val space: XML.Body = spaces(1) |
61864 | 19 |
|
48704
85a3de10567d
tuned signature -- make Pretty less dependent on Symbol;
wenzelm
parents:
45666
diff
changeset
|
20 |
|
51492
eaa1c4cc1106
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);
wenzelm
parents:
51470
diff
changeset
|
21 |
/* text metric -- standardized to width of space */ |
eaa1c4cc1106
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);
wenzelm
parents:
51470
diff
changeset
|
22 |
|
eaa1c4cc1106
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);
wenzelm
parents:
51470
diff
changeset
|
23 |
abstract class Metric |
eaa1c4cc1106
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);
wenzelm
parents:
51470
diff
changeset
|
24 |
{ |
eaa1c4cc1106
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);
wenzelm
parents:
51470
diff
changeset
|
25 |
val unit: Double |
eaa1c4cc1106
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);
wenzelm
parents:
51470
diff
changeset
|
26 |
def apply(s: String): Double |
61868 | 27 |
def content_length(body: XML.Body): Double = |
28 |
XML.traverse_text(body)(0.0)(_ + apply(_)) |
|
51492
eaa1c4cc1106
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);
wenzelm
parents:
51470
diff
changeset
|
29 |
} |
eaa1c4cc1106
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);
wenzelm
parents:
51470
diff
changeset
|
30 |
|
eaa1c4cc1106
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);
wenzelm
parents:
51470
diff
changeset
|
31 |
object Metric_Default extends Metric |
eaa1c4cc1106
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);
wenzelm
parents:
51470
diff
changeset
|
32 |
{ |
eaa1c4cc1106
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);
wenzelm
parents:
51470
diff
changeset
|
33 |
val unit = 1.0 |
eaa1c4cc1106
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);
wenzelm
parents:
51470
diff
changeset
|
34 |
def apply(s: String): Double = s.length.toDouble |
eaa1c4cc1106
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);
wenzelm
parents:
51470
diff
changeset
|
35 |
} |
eaa1c4cc1106
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);
wenzelm
parents:
51470
diff
changeset
|
36 |
|
eaa1c4cc1106
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);
wenzelm
parents:
51470
diff
changeset
|
37 |
|
36687 | 38 |
/* markup trees with physical blocks and breaks */ |
39 |
||
61864 | 40 |
def block(body: XML.Body): XML.Tree = Block(false, 2, body) |
38573 | 41 |
|
36683 | 42 |
object Block |
43 |
{ |
|
61864 | 44 |
def apply(consistent: Boolean, indent: Int, body: XML.Body): XML.Tree = |
45 |
XML.Elem(Markup.Block(consistent, indent), body) |
|
36683 | 46 |
|
61864 | 47 |
def unapply(tree: XML.Tree): Option[(Boolean, Int, XML.Body)] = |
36683 | 48 |
tree match { |
61864 | 49 |
case XML.Elem(Markup.Block(consistent, indent), body) => Some((consistent, indent, body)) |
36683 | 50 |
case _ => None |
51 |
} |
|
52 |
} |
|
53 |
||
54 |
object Break |
|
55 |
{ |
|
61862
e2a9e46ac0fb
support pretty break indent, like underlying ML systems;
wenzelm
parents:
55551
diff
changeset
|
56 |
def apply(w: Int, i: Int = 0): XML.Tree = |
61865 | 57 |
XML.Elem(Markup.Break(w, i), spaces(w)) |
36683 | 58 |
|
61862
e2a9e46ac0fb
support pretty break indent, like underlying ML systems;
wenzelm
parents:
55551
diff
changeset
|
59 |
def unapply(tree: XML.Tree): Option[(Int, Int)] = |
36683 | 60 |
tree match { |
61862
e2a9e46ac0fb
support pretty break indent, like underlying ML systems;
wenzelm
parents:
55551
diff
changeset
|
61 |
case XML.Elem(Markup.Break(w, i), _) => Some((w, i)) |
36683 | 62 |
case _ => None |
63 |
} |
|
64 |
} |
|
65 |
||
36689
379f5b1e7f91
replaced slightly odd fbreak markup by plain "\n", which also coincides with regular linebreaks produced outside the ML pretty engine;
wenzelm
parents:
36687
diff
changeset
|
66 |
val FBreak = XML.Text("\n") |
36687 | 67 |
|
51570
3633828d80fc
basic support for Pretty.item, which is considered as logical markup and interpreted in Isabelle/Scala, but ignored elsewhere (TTY, latex etc.);
wenzelm
parents:
51569
diff
changeset
|
68 |
def item(body: XML.Body): XML.Tree = |
61865 | 69 |
Block(false, 2, XML.elem(Markup.BULLET, space) :: space ::: body) |
51570
3633828d80fc
basic support for Pretty.item, which is considered as logical markup and interpreted in Isabelle/Scala, but ignored elsewhere (TTY, latex etc.);
wenzelm
parents:
51569
diff
changeset
|
70 |
|
61865 | 71 |
val Separator = List(XML.elem(Markup.SEPARATOR, space), FBreak) |
49843
afddf4e26fac
further refinement of jEdit line range, avoiding lack of final \n;
wenzelm
parents:
49827
diff
changeset
|
72 |
def separate(ts: List[XML.Tree]): XML.Body = Library.separate(Separator, ts.map(List(_))).flatten |
49473 | 73 |
|
36687 | 74 |
|
51570
3633828d80fc
basic support for Pretty.item, which is considered as logical markup and interpreted in Isabelle/Scala, but ignored elsewhere (TTY, latex etc.);
wenzelm
parents:
51569
diff
changeset
|
75 |
/* standard form */ |
36687 | 76 |
|
51570
3633828d80fc
basic support for Pretty.item, which is considered as logical markup and interpreted in Isabelle/Scala, but ignored elsewhere (TTY, latex etc.);
wenzelm
parents:
51569
diff
changeset
|
77 |
def standard_form(body: XML.Body): XML.Body = |
49468 | 78 |
body flatMap { |
49650
9fad6480300d
support for wrapped XML elements, which allows to preserve full markup tree information in to_XML/from_XML conversion;
wenzelm
parents:
49473
diff
changeset
|
79 |
case XML.Wrapped_Elem(markup, body1, body2) => |
51570
3633828d80fc
basic support for Pretty.item, which is considered as logical markup and interpreted in Isabelle/Scala, but ignored elsewhere (TTY, latex etc.);
wenzelm
parents:
51569
diff
changeset
|
80 |
List(XML.Wrapped_Elem(markup, body1, standard_form(body2))) |
3633828d80fc
basic support for Pretty.item, which is considered as logical markup and interpreted in Isabelle/Scala, but ignored elsewhere (TTY, latex etc.);
wenzelm
parents:
51569
diff
changeset
|
81 |
case XML.Elem(markup, body) => |
3633828d80fc
basic support for Pretty.item, which is considered as logical markup and interpreted in Isabelle/Scala, but ignored elsewhere (TTY, latex etc.);
wenzelm
parents:
51569
diff
changeset
|
82 |
if (markup.name == Markup.ITEM) List(item(standard_form(body))) |
3633828d80fc
basic support for Pretty.item, which is considered as logical markup and interpreted in Isabelle/Scala, but ignored elsewhere (TTY, latex etc.);
wenzelm
parents:
51569
diff
changeset
|
83 |
else List(XML.Elem(markup, standard_form(body))) |
48996 | 84 |
case XML.Text(text) => Library.separate(FBreak, split_lines(text).map(XML.Text)) |
36689
379f5b1e7f91
replaced slightly odd fbreak markup by plain "\n", which also coincides with regular linebreaks produced outside the ML pretty engine;
wenzelm
parents:
36687
diff
changeset
|
85 |
} |
379f5b1e7f91
replaced slightly odd fbreak markup by plain "\n", which also coincides with regular linebreaks produced outside the ML pretty engine;
wenzelm
parents:
36687
diff
changeset
|
86 |
|
51570
3633828d80fc
basic support for Pretty.item, which is considered as logical markup and interpreted in Isabelle/Scala, but ignored elsewhere (TTY, latex etc.);
wenzelm
parents:
51569
diff
changeset
|
87 |
|
3633828d80fc
basic support for Pretty.item, which is considered as logical markup and interpreted in Isabelle/Scala, but ignored elsewhere (TTY, latex etc.);
wenzelm
parents:
51569
diff
changeset
|
88 |
/* formatted output */ |
3633828d80fc
basic support for Pretty.item, which is considered as logical markup and interpreted in Isabelle/Scala, but ignored elsewhere (TTY, latex etc.);
wenzelm
parents:
51569
diff
changeset
|
89 |
|
51493
59d8a1031c00
allow fractional pretty margin -- avoid premature rounding;
wenzelm
parents:
51492
diff
changeset
|
90 |
private val margin_default = 76.0 |
36820 | 91 |
|
51493
59d8a1031c00
allow fractional pretty margin -- avoid premature rounding;
wenzelm
parents:
51492
diff
changeset
|
92 |
def formatted(input: XML.Body, margin: Double = margin_default, |
51492
eaa1c4cc1106
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);
wenzelm
parents:
51470
diff
changeset
|
93 |
metric: Metric = Metric_Default): XML.Body = |
36687 | 94 |
{ |
51568 | 95 |
sealed case class Text(tx: XML.Body = Nil, pos: Double = 0.0, nl: Int = 0) |
51470
a981a5c8a505
proper metric for blanks -- NB: 70f7483df9cb discontinues coincidence of char_width with space width;
wenzelm
parents:
51469
diff
changeset
|
96 |
{ |
a981a5c8a505
proper metric for blanks -- NB: 70f7483df9cb discontinues coincidence of char_width with space width;
wenzelm
parents:
51469
diff
changeset
|
97 |
def newline: Text = copy(tx = FBreak :: tx, pos = 0.0, nl = nl + 1) |
61864 | 98 |
def string(s: String): Text = |
99 |
if (s == "") this |
|
100 |
else copy(tx = XML.Text(s) :: tx, pos = pos + metric(s)) |
|
61865 | 101 |
def blanks(wd: Int): Text = string(Symbol.spaces(wd)) |
51470
a981a5c8a505
proper metric for blanks -- NB: 70f7483df9cb discontinues coincidence of char_width with space width;
wenzelm
parents:
51469
diff
changeset
|
102 |
def content: XML.Body = tx.reverse |
a981a5c8a505
proper metric for blanks -- NB: 70f7483df9cb discontinues coincidence of char_width with space width;
wenzelm
parents:
51469
diff
changeset
|
103 |
} |
a981a5c8a505
proper metric for blanks -- NB: 70f7483df9cb discontinues coincidence of char_width with space width;
wenzelm
parents:
51469
diff
changeset
|
104 |
|
36687 | 105 |
val breakgain = margin / 20 |
51569
4e084727faae
maintain integer indentation during formatting -- it needs to be implemented by repeated spaces eventually;
wenzelm
parents:
51568
diff
changeset
|
106 |
val emergencypos = (margin / 2).round.toInt |
36687 | 107 |
|
61864 | 108 |
def break_dist(trees: XML.Body, after: Double): Double = |
36817
ed97e877ff2d
more precise pretty printing based on actual font metrics;
wenzelm
parents:
36763
diff
changeset
|
109 |
trees match { |
61862
e2a9e46ac0fb
support pretty break indent, like underlying ML systems;
wenzelm
parents:
55551
diff
changeset
|
110 |
case Break(_, _) :: _ => 0.0 |
36817
ed97e877ff2d
more precise pretty printing based on actual font metrics;
wenzelm
parents:
36763
diff
changeset
|
111 |
case FBreak :: _ => 0.0 |
61868 | 112 |
case t :: ts => metric.content_length(List(t)) + break_dist(ts, after) |
36817
ed97e877ff2d
more precise pretty printing based on actual font metrics;
wenzelm
parents:
36763
diff
changeset
|
113 |
case Nil => after |
ed97e877ff2d
more precise pretty printing based on actual font metrics;
wenzelm
parents:
36763
diff
changeset
|
114 |
} |
ed97e877ff2d
more precise pretty printing based on actual font metrics;
wenzelm
parents:
36763
diff
changeset
|
115 |
|
61864 | 116 |
def force_all(trees: XML.Body): XML.Body = |
117 |
trees flatMap { |
|
61865 | 118 |
case Break(_, ind) => FBreak :: spaces(ind) |
61864 | 119 |
case tree => List(tree) |
120 |
} |
|
121 |
||
122 |
def force_next(trees: XML.Body): XML.Body = |
|
36817
ed97e877ff2d
more precise pretty printing based on actual font metrics;
wenzelm
parents:
36763
diff
changeset
|
123 |
trees match { |
ed97e877ff2d
more precise pretty printing based on actual font metrics;
wenzelm
parents:
36763
diff
changeset
|
124 |
case Nil => Nil |
ed97e877ff2d
more precise pretty printing based on actual font metrics;
wenzelm
parents:
36763
diff
changeset
|
125 |
case FBreak :: _ => trees |
61865 | 126 |
case Break(_, ind) :: ts => FBreak :: spaces(ind) ::: ts |
61864 | 127 |
case t :: ts => t :: force_next(ts) |
36817
ed97e877ff2d
more precise pretty printing based on actual font metrics;
wenzelm
parents:
36763
diff
changeset
|
128 |
} |
ed97e877ff2d
more precise pretty printing based on actual font metrics;
wenzelm
parents:
36763
diff
changeset
|
129 |
|
51569
4e084727faae
maintain integer indentation during formatting -- it needs to be implemented by repeated spaces eventually;
wenzelm
parents:
51568
diff
changeset
|
130 |
def format(trees: XML.Body, blockin: Int, after: Double, text: Text): Text = |
36687 | 131 |
trees match { |
132 |
case Nil => text |
|
133 |
||
61864 | 134 |
case Block(consistent, indent, body) :: ts => |
51569
4e084727faae
maintain integer indentation during formatting -- it needs to be implemented by repeated spaces eventually;
wenzelm
parents:
51568
diff
changeset
|
135 |
val pos1 = (text.pos + indent).ceil.toInt |
36687 | 136 |
val pos2 = pos1 % emergencypos |
61868 | 137 |
val blockin1 = if (pos1 < emergencypos) pos1 else pos2 |
138 |
val blen = metric.content_length(body) |
|
61864 | 139 |
val d = break_dist(ts, after) |
140 |
val body1 = if (consistent && text.pos + blen > margin - d) force_all(body) else body |
|
141 |
val btext = format(body1, blockin1, d, text) |
|
142 |
val ts1 = if (text.nl < btext.nl) force_next(ts) else ts |
|
36687 | 143 |
format(ts1, blockin, after, btext) |
144 |
||
61862
e2a9e46ac0fb
support pretty break indent, like underlying ML systems;
wenzelm
parents:
55551
diff
changeset
|
145 |
case Break(wd, ind) :: ts => |
61864 | 146 |
if (text.pos + wd <= ((margin - break_dist(ts, after)) max (blockin + breakgain))) |
36687 | 147 |
format(ts, blockin, after, text.blanks(wd)) |
61862
e2a9e46ac0fb
support pretty break indent, like underlying ML systems;
wenzelm
parents:
55551
diff
changeset
|
148 |
else format(ts, blockin, after, text.newline.blanks(blockin + ind)) |
51569
4e084727faae
maintain integer indentation during formatting -- it needs to be implemented by repeated spaces eventually;
wenzelm
parents:
51568
diff
changeset
|
149 |
case FBreak :: ts => format(ts, blockin, after, text.newline.blanks(blockin)) |
36687 | 150 |
|
49650
9fad6480300d
support for wrapped XML elements, which allows to preserve full markup tree information in to_XML/from_XML conversion;
wenzelm
parents:
49473
diff
changeset
|
151 |
case XML.Wrapped_Elem(markup, body1, body2) :: ts => |
61864 | 152 |
val btext = format(body2, blockin, break_dist(ts, after), text.copy(tx = Nil)) |
153 |
val ts1 = if (text.nl < btext.nl) force_next(ts) else ts |
|
49650
9fad6480300d
support for wrapped XML elements, which allows to preserve full markup tree information in to_XML/from_XML conversion;
wenzelm
parents:
49473
diff
changeset
|
154 |
val btext1 = btext.copy(tx = XML.Wrapped_Elem(markup, body1, btext.content) :: text.tx) |
9fad6480300d
support for wrapped XML elements, which allows to preserve full markup tree information in to_XML/from_XML conversion;
wenzelm
parents:
49473
diff
changeset
|
155 |
format(ts1, blockin, after, btext1) |
9fad6480300d
support for wrapped XML elements, which allows to preserve full markup tree information in to_XML/from_XML conversion;
wenzelm
parents:
49473
diff
changeset
|
156 |
|
38230
ed147003de4b
simplified type XML.Tree: embed Markup directly, avoid slightly odd triple;
wenzelm
parents:
37374
diff
changeset
|
157 |
case XML.Elem(markup, body) :: ts => |
61864 | 158 |
val btext = format(body, blockin, break_dist(ts, after), text.copy(tx = Nil)) |
159 |
val ts1 = if (text.nl < btext.nl) force_next(ts) else ts |
|
38230
ed147003de4b
simplified type XML.Tree: embed Markup directly, avoid slightly odd triple;
wenzelm
parents:
37374
diff
changeset
|
160 |
val btext1 = btext.copy(tx = XML.Elem(markup, btext.content) :: text.tx) |
36734
d9b10c173330
Pretty.formatted operates directly on XML trees, treating XML.Elem like a pro-forma block of indentation 0, like the ML version;
wenzelm
parents:
36689
diff
changeset
|
161 |
format(ts1, blockin, after, btext1) |
49650
9fad6480300d
support for wrapped XML elements, which allows to preserve full markup tree information in to_XML/from_XML conversion;
wenzelm
parents:
49473
diff
changeset
|
162 |
|
51492
eaa1c4cc1106
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);
wenzelm
parents:
51470
diff
changeset
|
163 |
case XML.Text(s) :: ts => format(ts, blockin, after, text.string(s)) |
36687 | 164 |
} |
49650
9fad6480300d
support for wrapped XML elements, which allows to preserve full markup tree information in to_XML/from_XML conversion;
wenzelm
parents:
49473
diff
changeset
|
165 |
|
51570
3633828d80fc
basic support for Pretty.item, which is considered as logical markup and interpreted in Isabelle/Scala, but ignored elsewhere (TTY, latex etc.);
wenzelm
parents:
51569
diff
changeset
|
166 |
format(standard_form(input), 0, 0.0, Text()).content |
36687 | 167 |
} |
36734
d9b10c173330
Pretty.formatted operates directly on XML trees, treating XML.Elem like a pro-forma block of indentation 0, like the ML version;
wenzelm
parents:
36689
diff
changeset
|
168 |
|
51493
59d8a1031c00
allow fractional pretty margin -- avoid premature rounding;
wenzelm
parents:
51492
diff
changeset
|
169 |
def string_of(input: XML.Body, margin: Double = margin_default, |
51492
eaa1c4cc1106
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);
wenzelm
parents:
51470
diff
changeset
|
170 |
metric: Metric = Metric_Default): String = |
49416
1053a564dd25
some actual rich text markup via XML.content_markup;
wenzelm
parents:
49414
diff
changeset
|
171 |
XML.content(formatted(input, margin, metric)) |
36736 | 172 |
|
173 |
||
174 |
/* unformatted output */ |
|
175 |
||
38573 | 176 |
def unformatted(input: XML.Body): XML.Body = |
36736 | 177 |
{ |
38573 | 178 |
def fmt(tree: XML.Tree): XML.Body = |
36736 | 179 |
tree match { |
61864 | 180 |
case Block(_, _, body) => body.flatMap(fmt) |
61865 | 181 |
case Break(wd, _) => spaces(wd) |
182 |
case FBreak => space |
|
49650
9fad6480300d
support for wrapped XML elements, which allows to preserve full markup tree information in to_XML/from_XML conversion;
wenzelm
parents:
49473
diff
changeset
|
183 |
case XML.Wrapped_Elem(markup, body1, body2) => |
9fad6480300d
support for wrapped XML elements, which allows to preserve full markup tree information in to_XML/from_XML conversion;
wenzelm
parents:
49473
diff
changeset
|
184 |
List(XML.Wrapped_Elem(markup, body1, body2.flatMap(fmt))) |
38230
ed147003de4b
simplified type XML.Tree: embed Markup directly, avoid slightly odd triple;
wenzelm
parents:
37374
diff
changeset
|
185 |
case XML.Elem(markup, body) => List(XML.Elem(markup, body.flatMap(fmt))) |
36736 | 186 |
case XML.Text(_) => List(tree) |
187 |
} |
|
51570
3633828d80fc
basic support for Pretty.item, which is considered as logical markup and interpreted in Isabelle/Scala, but ignored elsewhere (TTY, latex etc.);
wenzelm
parents:
51569
diff
changeset
|
188 |
standard_form(input).flatMap(fmt) |
36736 | 189 |
} |
190 |
||
49416
1053a564dd25
some actual rich text markup via XML.content_markup;
wenzelm
parents:
49414
diff
changeset
|
191 |
def str_of(input: XML.Body): String = XML.content(unformatted(input)) |
36683 | 192 |
} |