equal
deleted
inserted
replaced
71 |
71 |
72 class Style { |
72 class Style { |
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)) |
|
77 def enclose_bold(str: String): String = enclose(make_bold(str)) |
76 } |
78 } |
77 |
79 |
78 class Style_HTML extends Style { |
80 class Style_HTML extends Style { |
79 override def enclose(body: String): String = "<html>" + body + "</html>" |
81 override def enclose(body: String): String = "<html>" + body + "</html>" |
80 override def make_text(str: String): String = HTML.output(str) |
82 override def make_text(str: String): String = HTML.output(str) |
317 |
319 |
318 /* tooltip with multi-line support */ |
320 /* tooltip with multi-line support */ |
319 |
321 |
320 def tooltip_lines(text: String): String = |
322 def tooltip_lines(text: String): String = |
321 if (text == null || text == "") null |
323 if (text == null || text == "") null |
322 else "<html>" + HTML.output(text) + "</html>" |
324 else Style_HTML.enclose_text(text) |
323 |
325 |
324 |
326 |
325 /* icon */ |
327 /* icon */ |
326 |
328 |
327 def isabelle_icon(): ImageIcon = |
329 def isabelle_icon(): ImageIcon = |