# HG changeset patch # User wenzelm # Date 1393355747 -3600 # Node ID bef19c929ba52a5191834968e5f31e306e3ca208 # Parent 97f390fa0f3afadfc80f26b8efeac44933b00665 more completion rendering: active, semantic, syntactic; tuned; diff -r 97f390fa0f3a -r bef19c929ba5 src/Tools/jEdit/etc/options --- a/src/Tools/jEdit/etc/options Tue Feb 25 18:07:35 2014 +0100 +++ b/src/Tools/jEdit/etc/options Tue Feb 25 20:15:47 2014 +0100 @@ -86,6 +86,7 @@ option keyword2_color : string = "009966FF" option keyword3_color : string = "0099FFFF" option caret_invisible_color : string = "50000080" +option completion_color : string = "0000FFFF" option tfree_color : string = "A020F0FF" option tvar_color : string = "A020F0FF" diff -r 97f390fa0f3a -r bef19c929ba5 src/Tools/jEdit/src/completion_popup.scala --- a/src/Tools/jEdit/src/completion_popup.scala Tue Feb 25 18:07:35 2014 +0100 +++ b/src/Tools/jEdit/src/completion_popup.scala Tue Feb 25 20:15:47 2014 +0100 @@ -92,6 +92,65 @@ } + /* rendering */ + + def rendering(rendering: Rendering, line_range: Text.Range): Option[Text.Info[Color]] = + { + active_range match { + case Some(range) => range.try_restrict(line_range) + case None => + val buffer = text_area.getBuffer + val caret = text_area.getCaretPosition + + if (line_range.contains(caret)) { + JEdit_Lib.stretch_point_range(buffer, caret).try_restrict(line_range) match { + case Some(range) if !range.is_singularity => + rendering.completion_names(range) match { + case Some(names) => Some(names.range) + case None => + syntax_completion(Some(rendering), false) match { + case Some(result) => Some(result.range) + case None => None + } + } + case _ => None + } + } + else None + } + }.map(range => Text.Info(range, rendering.completion_color)) + + + /* syntax completion */ + + def syntax_completion( + opt_rendering: Option[Rendering], explicit: Boolean): Option[Completion.Result] = + { + val buffer = text_area.getBuffer + val history = PIDE.completion_history.value + val decode = Isabelle_Encoding.is_active(buffer) + + Isabelle.mode_syntax(JEdit_Lib.buffer_mode(buffer)) match { + case Some(syntax) => + val caret = text_area.getCaretPosition + val line = buffer.getLineOfOffset(caret) + val start = buffer.getLineStartOffset(line) + val text = buffer.getSegment(start, caret - start) + + val context = + (opt_rendering orElse PIDE.document_view(text_area).map(_.get_rendering()) match { + case Some(rendering) => + rendering.completion_context(JEdit_Lib.stretch_point_range(buffer, caret)) + case None => None + }) getOrElse syntax.completion_context + + syntax.completion.complete(history, decode, explicit, start, text, context) + + case None => None + } + } + + /* completion action */ private def insert(item: Completion.Item) @@ -179,41 +238,20 @@ } } - def syntax_completion(): Boolean = - { - Isabelle.mode_syntax(JEdit_Lib.buffer_mode(buffer)) match { - case Some(syntax) => - val line = buffer.getLineOfOffset(caret) - val start = buffer.getLineStartOffset(line) - val text = buffer.getSegment(start, caret - start) - - val context = - (PIDE.document_view(text_area) match { - case None => None - case Some(doc_view) => - val rendering = doc_view.get_rendering() - rendering.completion_context(JEdit_Lib.stretch_point_range(buffer, caret)) - }) getOrElse syntax.completion_context - - syntax.completion.complete(history, decode, explicit, start, text, context) match { - case Some(result) => - result.items match { - case List(item) if result.unique && item.immediate && immediate => - insert(item) - true - case _ :: _ => - open_popup(result) - true - case _ => false - } - case None => false + def syntactic_completion(): Boolean = + syntax_completion(None, explicit) match { + case Some(result) => + result.items match { + case List(item) if result.unique && item.immediate && immediate => + insert(item); true + case _ :: _ => open_popup(result); true + case _ => false } case None => false } - } if (buffer.isEditable) - semantic_completion() || syntax_completion() + semantic_completion() || syntactic_completion() } diff -r 97f390fa0f3a -r bef19c929ba5 src/Tools/jEdit/src/rendering.scala --- a/src/Tools/jEdit/src/rendering.scala Tue Feb 25 18:07:35 2014 +0100 +++ b/src/Tools/jEdit/src/rendering.scala Tue Feb 25 20:15:47 2014 +0100 @@ -261,6 +261,7 @@ val keyword2_color = color_value("keyword2_color") val keyword3_color = color_value("keyword3_color") val caret_invisible_color = color_value("caret_invisible_color") + val completion_color = color_value("completion_color") val tfree_color = color_value("tfree_color") val tvar_color = color_value("tvar_color") diff -r 97f390fa0f3a -r bef19c929ba5 src/Tools/jEdit/src/rich_text_area.scala --- a/src/Tools/jEdit/src/rich_text_area.scala Tue Feb 25 18:07:35 2014 +0100 +++ b/src/Tools/jEdit/src/rich_text_area.scala Tue Feb 25 20:15:47 2014 +0100 @@ -222,23 +222,6 @@ } - /* caret */ - - private def get_caret_range(stretch: Boolean): Text.Range = - if (caret_visible) { - val caret = text_area.getCaretPosition - if (stretch) JEdit_Lib.stretch_point_range(buffer, caret) - else JEdit_Lib.point_range(buffer, caret) - } - else Text.Range(-1) - - private def get_caret_color(rendering: Rendering): Color = - { - if (text_area.isCaretVisible) text_area.getPainter.getCaretColor - else rendering.caret_invisible_color - } - - /* text background */ private val background_painter = new TextAreaExtension @@ -312,13 +295,23 @@ /* text */ + private def caret_color(rendering: Rendering): Color = + { + if (text_area.isCaretVisible) + text_area.getPainter.getCaretColor + else rendering.caret_invisible_color + } + private def paint_chunk_list(rendering: Rendering, gfx: Graphics2D, line_start: Text.Offset, head: Chunk, x: Float, y: Float): Float = { val clip_rect = gfx.getClipBounds val painter = text_area.getPainter val font_context = painter.getFontRenderContext - val caret_range = get_caret_range(false) + + val caret_range = + if (caret_visible) JEdit_Lib.point_range(buffer, text_area.getCaretPosition) + else Text.Range(-1) var w = 0.0f var chunk = head @@ -369,7 +362,7 @@ val astr = new AttributedString(s2) astr.addAttribute(TextAttribute.FONT, chunk_font) - astr.addAttribute(TextAttribute.FOREGROUND, get_caret_color(rendering)) + astr.addAttribute(TextAttribute.FOREGROUND, caret_color(rendering)) astr.addAttribute(TextAttribute.SWAP_COLORS, TextAttribute.SWAP_COLORS_ON) gfx.drawString(astr.getIterator, x1 + string_width(s1), y) @@ -455,9 +448,6 @@ start: Array[Int], end: Array[Int], y: Int, line_height: Int) { robust_rendering { rendering => - val caret_range = get_caret_range(true) - val caret_color = text_area.getPainter.getCaretColor - for (i <- 0 until physical_lines.length) { if (physical_lines(i) != -1) { val line_range = Text.Range(start(i), end(i)) @@ -492,21 +482,14 @@ } // completion range - if (!hyperlink_area.is_active) { - def paint_completion(range: Text.Range) { - for (r <- JEdit_Lib.gfx_range(text_area, range)) { - gfx.setColor(caret_color) - gfx.drawRect(r.x, y + i * line_height, r.length - 1, line_height - 1) - } - } - Completion_Popup.Text_Area.active_range(text_area) match { - case Some(range) if range.try_restrict(line_range).isDefined => - paint_completion(range.try_restrict(line_range).get) - case _ => - for { - caret <- caret_range.try_restrict(line_range) - names <- rendering.completion_names(caret) - } paint_completion(names.range) + if (!hyperlink_area.is_active && caret_visible) { + for { + completion <- Completion_Popup.Text_Area(text_area) + Text.Info(range, color) <- completion.rendering(rendering, line_range) + r <- JEdit_Lib.gfx_range(text_area, range) + } { + gfx.setColor(color) + gfx.drawRect(r.x, y + i * line_height, r.length - 1, line_height - 1) } } } @@ -550,7 +533,7 @@ val offset = caret - text_area.getLineStartOffset(physical_line) val x = text_area.offsetToXY(physical_line, offset).x - gfx.setColor(get_caret_color(rendering)) + gfx.setColor(caret_color(rendering)) gfx.drawRect(x, y, (metric.unit * metric.average).round.toInt - 1, fm.getHeight - 1) } }