--- a/src/Pure/GUI/popup.scala Tue Sep 24 20:24:14 2013 +0200 +++ b/src/Pure/GUI/popup.scala Tue Sep 24 20:41:28 2013 +0200 @@ -1,4 +1,5 @@ /* Title: Pure/GUI/popup.scala + Module: PIDE-GUI Author: Makarius Popup within layered pane.