equal
deleted
inserted
replaced
73 def enclose(body: String): String = body |
73 def enclose(body: String): String = body |
74 def make_text(str: String): String = str |
74 def make_text(str: String): String = str |
75 def make_bold(str: String): String = str |
75 def make_bold(str: String): String = str |
76 def enclose_text(str: String): String = enclose(make_text(str)) |
76 def enclose_text(str: String): String = enclose(make_text(str)) |
77 def enclose_bold(str: String): String = enclose(make_bold(str)) |
77 def enclose_bold(str: String): String = enclose(make_bold(str)) |
|
78 def spaces(n: Int): String = Symbol.spaces(n) |
78 } |
79 } |
79 |
80 |
80 class Style_HTML extends Style { |
81 class Style_HTML extends Style { |
81 override def enclose(body: String): String = "<html>" + body + "</html>" |
82 override def enclose(body: String): String = "<html>" + body + "</html>" |
82 override def make_text(str: String): String = HTML.output(str) |
83 override def make_text(str: String): String = HTML.output(str) |
83 override def make_bold(str: String): String = "<b>" + make_text(str) + "</b>" |
84 override def make_bold(str: String): String = "<b>" + make_text(str) + "</b>" |
|
85 override def spaces(n: Int): String = HTML.spaces(n) |
84 } |
86 } |
85 |
87 |
86 abstract class Style_Symbol extends Style { |
88 abstract class Style_Symbol extends Style { |
87 def bold: String |
89 def bold: String |
88 override def make_bold(str: String): String = |
90 override def make_bold(str: String): String = |