--- a/src/Tools/jEdit/src/completion_popup.scala Fri Dec 23 22:33:14 2022 +0100
+++ b/src/Tools/jEdit/src/completion_popup.scala Fri Dec 23 22:41:47 2022 +0100
@@ -281,7 +281,7 @@
if (buffer.isEditable) {
val caret = text_area.getCaretPosition
- val opt_rendering = Document_View.get(text_area).map(_.get_rendering())
+ val opt_rendering = Document_View.get_rendering(text_area)
val result0 = syntax_completion(history, explicit, opt_rendering)
val (no_completion, semantic_completion) = {
opt_rendering match {