1/* Title: Tools/jEdit/src/completion_popup.scala 2 Author: Makarius 3 4Completion popup. 5*/ 6 7package isabelle.jedit 8 9 10import isabelle._ 11 12import java.awt.{Color, Font, Point, BorderLayout, Dimension} 13import java.awt.event.{KeyEvent, MouseEvent, MouseAdapter, FocusAdapter, FocusEvent} 14import java.io.{File => JFile} 15import javax.swing.{JPanel, JComponent, JLayeredPane, SwingUtilities} 16import javax.swing.border.LineBorder 17import javax.swing.text.DefaultCaret 18 19import scala.swing.{ListView, ScrollPane} 20import scala.swing.event.MouseClicked 21 22import org.gjt.sp.jedit.View 23import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea, Selection} 24import org.gjt.sp.jedit.gui.{HistoryTextField, KeyEventWorkaround} 25import org.gjt.sp.util.StandardUtilities 26 27 28object Completion_Popup 29{ 30 /** items with HTML rendering **/ 31 32 private class Item(val item: Completion.Item) 33 { 34 private val html = 35 item.description match { 36 case a :: bs => 37 "<html><b>" + HTML.output(Symbol.print_newlines(a)) + "</b>" + 38 HTML.output(bs.map(b => " " + Symbol.print_newlines(b)).mkString) + "</html>" 39 case Nil => "" 40 } 41 override def toString: String = html 42 } 43 44 45 46 /** jEdit text area **/ 47 48 object Text_Area 49 { 50 private val key = new Object 51 52 def apply(text_area: TextArea): Option[Completion_Popup.Text_Area] = 53 { 54 GUI_Thread.require {} 55 text_area.getClientProperty(key) match { 56 case text_area_completion: Completion_Popup.Text_Area => Some(text_area_completion) 57 case _ => None 58 } 59 } 60 61 def active_range(text_area: TextArea): Option[Text.Range] = 62 apply(text_area) match { 63 case Some(text_area_completion) => text_area_completion.active_range 64 case None => None 65 } 66 67 def action(text_area: TextArea, word_only: Boolean): Boolean = 68 apply(text_area) match { 69 case Some(text_area_completion) => 70 if (text_area_completion.active_range.isDefined) 71 text_area_completion.action(word_only = word_only) 72 else 73 text_area_completion.action(immediate = true, explicit = true, word_only = word_only) 74 true 75 case None => false 76 } 77 78 def exit(text_area: JEditTextArea) 79 { 80 GUI_Thread.require {} 81 apply(text_area) match { 82 case None => 83 case Some(text_area_completion) => 84 text_area_completion.deactivate() 85 text_area.putClientProperty(key, null) 86 } 87 } 88 89 def init(text_area: JEditTextArea): Completion_Popup.Text_Area = 90 { 91 exit(text_area) 92 val text_area_completion = new Text_Area(text_area) 93 text_area.putClientProperty(key, text_area_completion) 94 text_area_completion.activate() 95 text_area_completion 96 } 97 98 def dismissed(text_area: TextArea): Boolean = 99 { 100 GUI_Thread.require {} 101 apply(text_area) match { 102 case Some(text_area_completion) => text_area_completion.dismissed() 103 case None => false 104 } 105 } 106 } 107 108 class Text_Area private(text_area: JEditTextArea) 109 { 110 // owned by GUI thread 111 private var completion_popup: Option[Completion_Popup] = None 112 113 def active_range: Option[Text.Range] = 114 completion_popup match { 115 case Some(completion) => completion.active_range 116 case None => None 117 } 118 119 120 /* rendering */ 121 122 def rendering(rendering: JEdit_Rendering, line_range: Text.Range): Option[Text.Info[Color]] = 123 { 124 active_range match { 125 case Some(range) => range.try_restrict(line_range) 126 case None => 127 val caret = text_area.getCaretPosition 128 if (line_range.contains(caret)) { 129 rendering.before_caret_range(caret).try_restrict(line_range) match { 130 case Some(range) if !range.is_singularity => 131 val range0 = 132 Completion.Result.merge(Completion.History.empty, 133 syntax_completion(Completion.History.empty, true, Some(rendering)), 134 rendering.path_completion(caret), 135 Document_Model.bibtex_completion(Completion.History.empty, rendering, caret)) 136 .map(_.range) 137 rendering.semantic_completion(range0, range) match { 138 case None => range0 139 case Some(Text.Info(_, Completion.No_Completion)) => None 140 case Some(Text.Info(range1, _: Completion.Names)) => Some(range1) 141 } 142 case _ => None 143 } 144 } 145 else None 146 } 147 }.map(range => Text.Info(range, rendering.completion_color)) 148 149 150 /* syntax completion */ 151 152 def syntax_completion( 153 history: Completion.History, 154 explicit: Boolean, 155 opt_rendering: Option[JEdit_Rendering]): Option[Completion.Result] = 156 { 157 val buffer = text_area.getBuffer 158 val unicode = Isabelle_Encoding.is_active(buffer) 159 160 Isabelle.buffer_syntax(buffer) match { 161 case Some(syntax) => 162 val context = 163 (for { 164 rendering <- opt_rendering 165 if PIDE.options.bool("jedit_completion_context") 166 caret_range = rendering.before_caret_range(text_area.getCaretPosition) 167 context <- rendering.language_context(caret_range) 168 } yield context) getOrElse syntax.language_context 169 170 val caret = text_area.getCaretPosition 171 val line_range = JEdit_Lib.line_range(buffer, text_area.getCaretLine) 172 val line_start = line_range.start 173 for { 174 line_text <- JEdit_Lib.get_text(buffer, line_range) 175 result <- 176 syntax.complete( 177 history, unicode, explicit, line_start, line_text, caret - line_start, context) 178 } yield result 179 180 case None => None 181 } 182 } 183 184 185 /* completion action: text area */ 186 187 private def insert(item: Completion.Item) 188 { 189 GUI_Thread.require {} 190 191 val buffer = text_area.getBuffer 192 val range = item.range 193 if (buffer.isEditable) { 194 JEdit_Lib.buffer_edit(buffer) { 195 JEdit_Lib.get_text(buffer, range) match { 196 case Some(text) if text == item.original => 197 text_area.getSelectionAtOffset(text_area.getCaretPosition) match { 198 199 /*rectangular selection as "tall caret"*/ 200 case selection : Selection.Rect 201 if selection.getStart(buffer, text_area.getCaretLine) == range.stop => 202 text_area.moveCaretPosition(range.stop) 203 (0 until Character.codePointCount(item.original, 0, item.original.length)) 204 .foreach(_ => text_area.backspace()) 205 text_area.setSelectedText(selection, item.replacement) 206 text_area.moveCaretPosition(text_area.getCaretPosition + item.move) 207 208 /*other selections: rectangular, multiple range, ...*/ 209 case selection 210 if selection != null && 211 selection.getStart(buffer, text_area.getCaretLine) == range.start && 212 selection.getEnd(buffer, text_area.getCaretLine) == range.stop => 213 text_area.moveCaretPosition(range.stop + item.move) 214 text_area.getSelection.foreach(text_area.setSelectedText(_, item.replacement)) 215 216 /*no selection*/ 217 case _ => 218 buffer.remove(range.start, range.length) 219 buffer.insert(range.start, item.replacement) 220 text_area.moveCaretPosition(range.start + item.replacement.length + item.move) 221 Isabelle.indent_input(text_area) 222 } 223 case _ => 224 } 225 } 226 } 227 } 228 229 def action( 230 immediate: Boolean = false, 231 explicit: Boolean = false, 232 delayed: Boolean = false, 233 word_only: Boolean = false): Boolean = 234 { 235 val view = text_area.getView 236 val layered = view.getLayeredPane 237 val buffer = text_area.getBuffer 238 val painter = text_area.getPainter 239 240 val history = PIDE.plugin.completion_history.value 241 val unicode = Isabelle_Encoding.is_active(buffer) 242 243 def open_popup(result: Completion.Result) 244 { 245 val font = 246 painter.getFont.deriveFont( 247 Font_Info.main_size(PIDE.options.real("jedit_popup_font_scale"))) 248 249 val range = result.range 250 251 val loc1 = text_area.offsetToXY(range.start) 252 if (loc1 != null) { 253 val loc2 = 254 SwingUtilities.convertPoint(painter, 255 loc1.x, loc1.y + painter.getLineHeight, layered) 256 257 val items = result.items.map(new Item(_)) 258 val completion = 259 new Completion_Popup(Some(range), layered, loc2, font, items) 260 { 261 override def complete(item: Completion.Item) { 262 PIDE.plugin.completion_history.update(item) 263 insert(item) 264 } 265 override def propagate(evt: KeyEvent) { 266 if (view.getKeyEventInterceptor == null) 267 JEdit_Lib.propagate_key(view, evt) 268 else if (view.getKeyEventInterceptor == inner_key_listener) { 269 try { 270 view.setKeyEventInterceptor(null) 271 JEdit_Lib.propagate_key(view, evt) 272 } 273 finally { 274 if (isDisplayable) view.setKeyEventInterceptor(inner_key_listener) 275 } 276 } 277 if (evt.getID == KeyEvent.KEY_TYPED) input(evt) 278 } 279 override def shutdown(focus: Boolean) { 280 if (view.getKeyEventInterceptor == inner_key_listener) 281 view.setKeyEventInterceptor(null) 282 if (focus) text_area.requestFocus 283 JEdit_Lib.invalidate_range(text_area, range) 284 } 285 } 286 dismissed() 287 completion_popup = Some(completion) 288 view.setKeyEventInterceptor(completion.inner_key_listener) 289 JEdit_Lib.invalidate_range(text_area, range) 290 Pretty_Tooltip.dismissed_all() 291 completion.show_popup(false) 292 } 293 } 294 295 if (buffer.isEditable) { 296 val caret = text_area.getCaretPosition 297 val opt_rendering = Document_View.get(text_area).map(_.get_rendering()) 298 val result0 = syntax_completion(history, explicit, opt_rendering) 299 val (no_completion, semantic_completion) = 300 { 301 opt_rendering match { 302 case Some(rendering) => 303 rendering.semantic_completion_result(history, unicode, result0.map(_.range), 304 rendering.before_caret_range(caret)) 305 case None => (false, None) 306 } 307 } 308 if (no_completion) false 309 else { 310 val result = 311 { 312 val result1 = 313 if (word_only) None 314 else Completion.Result.merge(history, semantic_completion, result0) 315 opt_rendering match { 316 case None => result1 317 case Some(rendering) => 318 Completion.Result.merge(history, 319 result1, 320 JEdit_Spell_Checker.completion(rendering, explicit, caret), 321 rendering.path_completion(caret), 322 Document_Model.bibtex_completion(history, rendering, caret)) 323 } 324 } 325 result match { 326 case Some(result) => 327 result.items match { 328 case List(item) if result.unique && item.immediate && immediate => 329 insert(item) 330 true 331 case _ :: _ if !delayed => 332 open_popup(result) 333 false 334 case _ => false 335 } 336 case None => false 337 } 338 } 339 } 340 else false 341 } 342 343 344 /* input key events */ 345 346 def input(evt: KeyEvent) 347 { 348 GUI_Thread.require {} 349 350 if (!evt.isConsumed) { 351 val special = JEdit_Lib.special_key(evt) 352 353 if (PIDE.options.bool("jedit_completion")) { 354 dismissed() 355 if (evt.getKeyChar != '\b') { 356 val immediate = PIDE.options.bool("jedit_completion_immediate") 357 if (PIDE.options.seconds("jedit_completion_delay").is_zero && !special) { 358 input_delay.revoke() 359 action(immediate = immediate) 360 } 361 else { 362 if (!special && action(immediate = immediate, delayed = true)) 363 input_delay.revoke() 364 else 365 input_delay.invoke() 366 } 367 } 368 } 369 370 val selection = text_area.getSelection() 371 if (!special && (selection == null || selection.length == 0)) 372 Isabelle.indent_input(text_area) 373 } 374 } 375 376 private val input_delay = 377 GUI_Thread.delay_last(PIDE.options.seconds("jedit_completion_delay")) { 378 action() 379 } 380 381 382 /* dismiss popup */ 383 384 def dismissed(): Boolean = 385 { 386 GUI_Thread.require {} 387 388 completion_popup match { 389 case Some(completion) => 390 completion.hide_popup() 391 completion_popup = None 392 true 393 case None => 394 false 395 } 396 } 397 398 399 /* activation */ 400 401 private val outer_key_listener = 402 JEdit_Lib.key_listener(key_typed = input _) 403 404 private def activate() 405 { 406 text_area.addKeyListener(outer_key_listener) 407 } 408 409 private def deactivate() 410 { 411 dismissed() 412 text_area.removeKeyListener(outer_key_listener) 413 } 414 } 415 416 417 418 /** history text field **/ 419 420 class History_Text_Field( 421 name: String = null, 422 instant_popups: Boolean = false, 423 enter_adds_to_history: Boolean = true, 424 syntax: Outer_Syntax = Outer_Syntax.empty) extends 425 HistoryTextField(name, instant_popups, enter_adds_to_history) 426 { 427 text_field => 428 429 // see https://forums.oracle.com/thread/1361677 430 if (GUI.is_macos_laf) text_field.setCaret(new DefaultCaret) 431 432 // owned by GUI thread 433 private var completion_popup: Option[Completion_Popup] = None 434 435 436 /* dismiss */ 437 438 private def dismissed(): Boolean = 439 { 440 completion_popup match { 441 case Some(completion) => 442 completion.hide_popup() 443 completion_popup = None 444 true 445 case None => 446 false 447 } 448 } 449 450 451 /* insert */ 452 453 private def insert(item: Completion.Item) 454 { 455 GUI_Thread.require {} 456 457 val range = item.range 458 if (text_field.isEditable) { 459 val content = text_field.getText 460 range.try_substring(content) match { 461 case Some(text) if text == item.original => 462 text_field.setText( 463 content.substring(0, range.start) + 464 item.replacement + 465 content.substring(range.stop)) 466 text_field.getCaret.setDot(range.start + item.replacement.length + item.move) 467 case _ => 468 } 469 } 470 } 471 472 473 /* completion action: text field */ 474 475 def action() 476 { 477 GUI.layered_pane(text_field) match { 478 case Some(layered) if text_field.isEditable => 479 val history = PIDE.plugin.completion_history.value 480 481 val caret = text_field.getCaret.getDot 482 val text = text_field.getText 483 484 val context = syntax.language_context 485 486 syntax.complete(history, true, false, 0, text, caret, context) match { 487 case Some(result) => 488 val fm = text_field.getFontMetrics(text_field.getFont) 489 val loc = 490 SwingUtilities.convertPoint(text_field, fm.stringWidth(text), fm.getHeight, layered) 491 492 val items = result.items.map(new Item(_)) 493 val completion = 494 new Completion_Popup(None, layered, loc, text_field.getFont, items) 495 { 496 override def complete(item: Completion.Item) { 497 PIDE.plugin.completion_history.update(item) 498 insert(item) 499 } 500 override def propagate(evt: KeyEvent) { 501 if (!evt.isConsumed) text_field.processKeyEvent(evt) 502 } 503 override def shutdown(focus: Boolean) { if (focus) text_field.requestFocus } 504 } 505 dismissed() 506 completion_popup = Some(completion) 507 completion.show_popup(true) 508 509 case None => 510 } 511 case _ => 512 } 513 } 514 515 516 /* process key event */ 517 518 private def process(evt: KeyEvent) 519 { 520 if (PIDE.options.bool("jedit_completion")) { 521 dismissed() 522 if (evt.getKeyChar != '\b') { 523 val special = JEdit_Lib.special_key(evt) 524 if (PIDE.options.seconds("jedit_completion_delay").is_zero && !special) { 525 process_delay.revoke() 526 action() 527 } 528 else process_delay.invoke() 529 } 530 } 531 } 532 533 private val process_delay = 534 GUI_Thread.delay_last(PIDE.options.seconds("jedit_completion_delay")) { 535 action() 536 } 537 538 override def processKeyEvent(evt0: KeyEvent) 539 { 540 val evt = KeyEventWorkaround.processKeyEvent(evt0) 541 if (evt != null) { 542 evt.getID match { 543 case KeyEvent.KEY_PRESSED => 544 val key_code = evt.getKeyCode 545 if (key_code == KeyEvent.VK_ESCAPE) { 546 if (dismissed()) evt.consume 547 } 548 case KeyEvent.KEY_TYPED => 549 super.processKeyEvent(evt) 550 process(evt) 551 evt.consume 552 case _ => 553 } 554 if (!evt.isConsumed) super.processKeyEvent(evt) 555 } 556 } 557 } 558} 559 560 561class Completion_Popup private( 562 opt_range: Option[Text.Range], 563 layered: JLayeredPane, 564 location: Point, 565 font: Font, 566 items: List[Completion_Popup.Item]) extends JPanel(new BorderLayout) 567{ 568 completion => 569 570 GUI_Thread.require {} 571 572 require(items.nonEmpty) 573 val multi = items.length > 1 574 575 576 /* actions */ 577 578 def complete(item: Completion.Item) { } 579 def propagate(evt: KeyEvent) { } 580 def shutdown(focus: Boolean) { } 581 582 583 /* list view */ 584 585 private val list_view = new ListView(items) 586 list_view.font = font 587 list_view.selection.intervalMode = ListView.IntervalMode.Single 588 list_view.peer.setFocusTraversalKeysEnabled(false) 589 list_view.peer.setVisibleRowCount(items.length min 8) 590 list_view.peer.setSelectedIndex(0) 591 592 for (cond <- 593 List(JComponent.WHEN_FOCUSED, 594 JComponent.WHEN_ANCESTOR_OF_FOCUSED_COMPONENT, 595 JComponent.WHEN_IN_FOCUSED_WINDOW)) list_view.peer.setInputMap(cond, null) 596 597 private def complete_selected(): Boolean = 598 { 599 list_view.selection.items.toList match { 600 case item :: _ => complete(item.item); true 601 case _ => false 602 } 603 } 604 605 private def move_items(n: Int) 606 { 607 val i = list_view.peer.getSelectedIndex 608 val j = ((i + n) min (items.length - 1)) max 0 609 if (i != j) { 610 list_view.peer.setSelectedIndex(j) 611 list_view.peer.ensureIndexIsVisible(j) 612 } 613 } 614 615 private def move_pages(n: Int) 616 { 617 val page_size = list_view.peer.getVisibleRowCount - 1 618 move_items(page_size * n) 619 } 620 621 622 /* event handling */ 623 624 val inner_key_listener = 625 JEdit_Lib.key_listener( 626 key_pressed = (e: KeyEvent) => 627 { 628 if (!e.isConsumed) { 629 e.getKeyCode match { 630 case KeyEvent.VK_ENTER if PIDE.options.bool("jedit_completion_select_enter") => 631 if (complete_selected()) e.consume 632 hide_popup() 633 case KeyEvent.VK_TAB if PIDE.options.bool("jedit_completion_select_tab") => 634 if (complete_selected()) e.consume 635 hide_popup() 636 case KeyEvent.VK_ESCAPE => 637 hide_popup() 638 e.consume 639 case KeyEvent.VK_UP | KeyEvent.VK_KP_UP if multi => 640 move_items(-1) 641 e.consume 642 case KeyEvent.VK_DOWN | KeyEvent.VK_KP_DOWN if multi => 643 move_items(1) 644 e.consume 645 case KeyEvent.VK_PAGE_UP if multi => 646 move_pages(-1) 647 e.consume 648 case KeyEvent.VK_PAGE_DOWN if multi => 649 move_pages(1) 650 e.consume 651 case _ => 652 if (e.isActionKey || e.isAltDown || e.isMetaDown || e.isControlDown) 653 hide_popup() 654 } 655 } 656 propagate(e) 657 }, 658 key_typed = propagate _ 659 ) 660 661 list_view.peer.addKeyListener(inner_key_listener) 662 663 list_view.peer.addMouseListener(new MouseAdapter { 664 override def mouseClicked(e: MouseEvent) { 665 if (complete_selected()) e.consume 666 hide_popup() 667 } 668 }) 669 670 list_view.peer.addFocusListener(new FocusAdapter { 671 override def focusLost(e: FocusEvent) { hide_popup() } 672 }) 673 674 675 /* main content */ 676 677 override def getFocusTraversalKeysEnabled = false 678 completion.setBorder(new LineBorder(Color.BLACK)) 679 completion.add((new ScrollPane(list_view)).peer.asInstanceOf[JComponent]) 680 681 682 /* popup */ 683 684 def active_range: Option[Text.Range] = 685 if (isDisplayable) opt_range else None 686 687 private val popup = 688 { 689 val screen = JEdit_Lib.screen_location(layered, location) 690 val size = 691 { 692 val geometry = JEdit_Lib.window_geometry(completion, completion) 693 val bounds = JEdit_Rendering.popup_bounds 694 val w = geometry.width min (screen.bounds.width * bounds).toInt min layered.getWidth 695 val h = geometry.height min (screen.bounds.height * bounds).toInt min layered.getHeight 696 new Dimension(w, h) 697 } 698 new Popup(layered, completion, screen.relative(layered, size), size) 699 } 700 701 private def show_popup(focus: Boolean) 702 { 703 popup.show 704 if (focus) list_view.requestFocus 705 } 706 707 private def hide_popup() 708 { 709 shutdown(list_view.peer.isFocusOwner) 710 popup.hide 711 } 712} 713