--- 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"
--- 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()
}
--- 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")
--- 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)
}
}