equal
deleted
inserted
replaced
69 |
69 |
70 /* named items */ |
70 /* named items */ |
71 |
71 |
72 enum Style { case plain, html, symbol_encoded, symbol_decoded } |
72 enum Style { case plain, html, symbol_encoded, symbol_decoded } |
73 |
73 |
|
74 def make_text(str: String, style: Style = Style.plain): String = |
|
75 if (style == Style.html) HTML.output(str) else str |
|
76 |
74 def make_bold(str: String, style: Style = Style.plain): String = |
77 def make_bold(str: String, style: Style = Style.plain): String = |
75 style match { |
78 style match { |
76 case Style.plain => str |
79 case Style.plain => str |
77 case Style.html => "<b>" + HTML.output(str) + "</b>" |
80 case Style.html => "<b>" + HTML.output(str) + "</b>" |
78 case _ => |
81 case _ => |
89 style: Style = Style.plain |
92 style: Style = Style.plain |
90 ) { |
93 ) { |
91 override def toString: String = { |
94 override def toString: String = { |
92 val a = kind.nonEmpty |
95 val a = kind.nonEmpty |
93 val b = name.nonEmpty |
96 val b = name.nonEmpty |
94 val k = if_proper(kind, make_bold(kind, style = style)) |
97 make_text(prefix, style = style) + |
95 prefix + if_proper(a || b, |
98 if_proper(a || b, |
96 if_proper(prefix, ": ") + k + if_proper(a && b, " ") + if_proper(b, quote(name))) |
99 if_proper(prefix, ": ") + if_proper(kind, make_bold(kind, style = style)) + |
|
100 if_proper(a && b, " ") + if_proper(b, make_text(quote(name), style = style))) |
97 } |
101 } |
98 } |
102 } |
99 |
103 |
100 |
104 |
101 /* simple dialogs */ |
105 /* simple dialogs */ |