equal
deleted
inserted
replaced
100 s ++= body |
100 s ++= body |
101 s ++= "</span></html>" |
101 s ++= "</span></html>" |
102 } |
102 } |
103 } |
103 } |
104 |
104 |
105 def bullet: String = "\u2218" |
105 def regular_bullet: String = "\u2022" |
106 def bullet_triangle: String = "\u25b9" |
106 def triangular_bullet: String = "\u2023" |
107 } |
107 } |
108 |
108 |
109 abstract class Style_Symbol extends Style { |
109 abstract class Style_Symbol extends Style { |
110 def bold: String |
110 def bold: String |
111 override def make_bold(str: String): String = |
111 override def make_bold(str: String): String = |