src/Tools/jEdit/src/completion_popup.scala

       }
 
 
     /* rendering */
 
-    def rendering(rendering: Rendering, line_range: Text.Range): Option[Text.Info[Color]] =
+    def rendering(rendering: JEdit_Rendering, line_range: Text.Range): Option[Text.Info[Color]] =
     {
       active_range match {
         case Some(range) => range.try_restrict(line_range)
         case None =>
           if (line_range.contains(text_area.getCaretPosition)) {

     /* syntax completion */
 
     def syntax_completion(
       history: Completion.History,
       explicit: Boolean,
-      opt_rendering: Option[Rendering]): Option[Completion.Result] =
+      opt_rendering: Option[JEdit_Rendering]): Option[Completion.Result] =
     {
       val buffer = text_area.getBuffer
       val decode = Isabelle_Encoding.is_active(buffer)
 
       Isabelle.buffer_syntax(buffer) match {

     }
 
 
     /* path completion */
 
-    def path_completion(rendering: Rendering): Option[Completion.Result] =
+    def path_completion(rendering: JEdit_Rendering): Option[Completion.Result] =
     {
       def complete(text: String): List[(String, List[String])] =
       {
         try {
           val path = Path.explode(text)

   {
     val screen = JEdit_Lib.screen_location(layered, location)
     val size =
     {
       val geometry = JEdit_Lib.window_geometry(completion, completion)
-      val bounds = Rendering.popup_bounds
+      val bounds = JEdit_Rendering.popup_bounds
       val w = geometry.width min (screen.bounds.width * bounds).toInt min layered.getWidth
       val h = geometry.height min (screen.bounds.height * bounds).toInt min layered.getHeight
       new Dimension(w, h)
     }
     new Popup(layered, completion, screen.relative(layered, size), size)