equal
deleted
inserted
replaced
48 |
48 |
49 stack match { |
49 stack match { |
50 case top :: _ if top.results == results && top.info == info => top |
50 case top :: _ if top.results == results && top.info == info => top |
51 case _ => |
51 case _ => |
52 val (old, rest) = |
52 val (old, rest) = |
53 JEdit_Lib.ancestors(parent).collectFirst({ case x: Pretty_Tooltip => x }) match { |
53 GUI.ancestors(parent).collectFirst({ case x: Pretty_Tooltip => x }) match { |
54 case Some(tip) => hierarchy(tip).getOrElse((stack, Nil)) |
54 case Some(tip) => hierarchy(tip).getOrElse((stack, Nil)) |
55 case None => (stack, Nil) |
55 case None => (stack, Nil) |
56 } |
56 } |
57 old.foreach(_.hide_popup) |
57 old.foreach(_.hide_popup) |
58 |
58 |