82 case Text.Info(_, XML.Elem(Markup(Markup.WRITELN, _), _)) => regular_color |
82 case Text.Info(_, XML.Elem(Markup(Markup.WRITELN, _), _)) => regular_color |
83 case Text.Info(_, XML.Elem(Markup(Markup.WARNING, _), _)) => warning_color |
83 case Text.Info(_, XML.Elem(Markup(Markup.WARNING, _), _)) => warning_color |
84 case Text.Info(_, XML.Elem(Markup(Markup.ERROR, _), _)) => error_color |
84 case Text.Info(_, XML.Elem(Markup(Markup.ERROR, _), _)) => error_color |
85 } |
85 } |
86 |
86 |
87 val popup: Markup_Tree.Select[XML.Tree] = |
87 val popup: Markup_Tree.Select[String] = |
88 { |
88 { |
89 case Text.Info(_, msg @ XML.Elem(Markup(markup, _), _)) |
89 case Text.Info(_, msg @ XML.Elem(Markup(markup, _), _)) |
90 if markup == Markup.WRITELN || markup == Markup.WARNING || markup == Markup.ERROR => msg |
90 if markup == Markup.WRITELN || markup == Markup.WARNING || markup == Markup.ERROR => |
|
91 Pretty.string_of(List(msg), margin = 40) |
91 } |
92 } |
92 |
93 |
93 val gutter_message: Markup_Tree.Select[Icon] = |
94 val gutter_message: Markup_Tree.Select[Icon] = |
94 { |
95 { |
95 case Text.Info(_, XML.Elem(Markup(Markup.WARNING, _), _)) => warning_icon |
96 case Text.Info(_, XML.Elem(Markup(Markup.WARNING, _), _)) => warning_icon |