163 Markup.ML_SOURCE -> "ML source", |
163 Markup.ML_SOURCE -> "ML source", |
164 Markup.DOC_SOURCE -> "document source") |
164 Markup.DOC_SOURCE -> "document source") |
165 |
165 |
166 val tooltip: Markup_Tree.Select[String] = |
166 val tooltip: Markup_Tree.Select[String] = |
167 { |
167 { |
168 case Text.Info(_, XML.Elem(Markup.Entity(kind, name), _)) => kind + " \"" + name + "\"" |
168 case Text.Info(_, XML.Elem(Markup.Entity(kind, name), _)) => kind + " " + quote(name) |
169 case Text.Info(_, XML.Elem(Markup(Markup.ML_TYPING, _), body)) => |
169 case Text.Info(_, XML.Elem(Markup(Markup.ML_TYPING, _), body)) => |
170 Pretty.string_of(List(Pretty.block(XML.Text("ML:") :: Pretty.Break(1) :: body)), |
170 Pretty.string_of(List(Pretty.block(XML.Text("ML:") :: Pretty.Break(1) :: body)), |
171 margin = Isabelle.Int_Property("tooltip-margin")) |
171 margin = Isabelle.Int_Property("tooltip-margin")) |
172 case Text.Info(_, XML.Elem(Markup(name, _), _)) |
172 case Text.Info(_, XML.Elem(Markup(name, _), _)) |
173 if tooltips.isDefinedAt(name) => tooltips(name) |
173 if tooltips.isDefinedAt(name) => tooltips(name) |