--- a/NEWS Mon Feb 24 10:16:10 2014 +0100
+++ b/NEWS Mon Feb 24 13:52:48 2014 +0100
@@ -35,9 +35,10 @@
auxiliary ML files.
* Improved completion based on context information about embedded
-languages: keywords are only completed for outer syntax, symbols for
-languages that support them. E.g. no symbol completion for ML source,
-but within ML strings, comments, antiquotations.
+languages: keywords are only completed for outer syntax, symbols or
+antiquotations for languages that support them. E.g. no symbol
+completion for ML source, but within ML strings, comments,
+antiquotations.
* Document panel: simplied interaction where every single mouse click
(re)opens document via desktop environment or as jEdit buffer.
--- a/src/Pure/General/completion.scala Mon Feb 24 10:16:10 2014 +0100
+++ b/src/Pure/General/completion.scala Mon Feb 24 13:52:48 2014 +0100
@@ -170,8 +170,8 @@
{
val outer = Context("", true, false)
val inner = Context(Markup.Language.UNKNOWN, true, false)
- val ML_outer = Context(Markup.Language.ML, false, false)
- val ML_inner = Context(Markup.Language.ML, true, true)
+ val ML_outer = Context(Markup.Language.ML, false, true)
+ val ML_inner = Context(Markup.Language.ML, true, false)
}
sealed case class Context(language: String, symbols: Boolean, antiquotes: Boolean)
--- a/src/Pure/General/symbol_pos.ML Mon Feb 24 10:16:10 2014 +0100
+++ b/src/Pure/General/symbol_pos.ML Mon Feb 24 13:52:48 2014 +0100
@@ -178,8 +178,8 @@
fun cartouche_content syms =
let
fun err () =
- error ("Malformed text cartouche: " ^ quote (content syms) ^
- Position.here (Position.set_range (range syms)));
+ error ("Malformed text cartouche: "
+ ^ quote (content syms) ^ Position.here (#1 (range syms)));
in
(case syms of
("\\<open>", _) :: rest =>
--- a/src/Pure/Isar/args.ML Mon Feb 24 10:16:10 2014 +0100
+++ b/src/Pure/Isar/args.ML Mon Feb 24 13:52:48 2014 +0100
@@ -191,7 +191,7 @@
fun named_attribute att =
internal_attribute ||
- named >> evaluate Token.Attribute (fn tok => att (Token.content_of tok, Token.position_of tok));
+ named >> evaluate Token.Attribute (fn tok => att (Token.content_of tok, Token.pos_of tok));
(* terms and types *)
--- a/src/Pure/Isar/method.ML Mon Feb 24 10:16:10 2014 +0100
+++ b/src/Pure/Isar/method.ML Mon Feb 24 13:52:48 2014 +0100
@@ -408,7 +408,7 @@
(Parse.position (Parse.xname >> rpair []) >> (Source o Args.src) ||
(* FIXME implicit "cartouche" method (experimental, undocumented) *)
Scan.ahead Parse.cartouche |-- Parse.not_eof >> (fn tok =>
- Source (Args.src (("cartouche", [tok]), Token.position_of tok))) ||
+ Source (Args.src (("cartouche", [tok]), Token.pos_of tok))) ||
Parse.$$$ "(" |-- Parse.!!! (meth0 --| Parse.$$$ ")")) x
and meth3 x =
(meth4 --| Parse.$$$ "?" >> Try ||
@@ -425,7 +425,7 @@
in
val parse =
- Scan.trace meth3 >> (fn (m, toks) => (m, Token.position_range_of toks));
+ Scan.trace meth3 >> (fn (m, toks) => (m, Token.range_of toks));
end;
@@ -438,7 +438,7 @@
| text (SOME (txt, _)) = SOME txt;
fun position NONE = Position.none
- | position (SOME (_, range)) = Position.set_range range;
+ | position (SOME (_, (pos, _))) = pos;
(* theory setup *)
--- a/src/Pure/Isar/outer_syntax.ML Mon Feb 24 10:16:10 2014 +0100
+++ b/src/Pure/Isar/outer_syntax.ML Mon Feb 24 13:52:48 2014 +0100
@@ -310,7 +310,7 @@
let val name = Token.content_of tok in
(case lookup_commands outer_syntax name of
NONE => []
- | SOME cmd => [((Token.position_of tok, command_markup false (name, cmd)), "")])
+ | SOME cmd => [((Token.pos_of tok, command_markup false (name, cmd)), "")])
end
else [];
--- a/src/Pure/Isar/parse.ML Mon Feb 24 10:16:10 2014 +0100
+++ b/src/Pure/Isar/parse.ML Mon Feb 24 13:52:48 2014 +0100
@@ -122,9 +122,11 @@
(fn () =>
(case Token.text_of tok of
(txt, "") =>
- s () ^ " expected,\nbut " ^ txt ^ Token.pos_of tok ^ " was found"
+ s () ^ " expected,\nbut " ^ txt ^ Position.here (Token.pos_of tok) ^
+ " was found"
| (txt1, txt2) =>
- s () ^ " expected,\nbut " ^ txt1 ^ Token.pos_of tok ^ " was found:\n" ^ txt2)));
+ s () ^ " expected,\nbut " ^ txt1 ^ Position.here (Token.pos_of tok) ^
+ " was found:\n" ^ txt2)));
(* cut *)
@@ -132,7 +134,7 @@
fun cut kind scan =
let
fun get_pos [] = " (end-of-input)"
- | get_pos (tok :: _) = Token.pos_of tok;
+ | get_pos (tok :: _) = Position.here (Token.pos_of tok);
fun err (toks, NONE) = (fn () => kind ^ get_pos toks)
| err (toks, SOME msg) =
@@ -165,7 +167,7 @@
val not_eof = RESET_VALUE (Scan.one Token.not_eof);
-fun position scan = (Scan.ahead not_eof >> Token.position_of) -- scan >> Library.swap;
+fun position scan = (Scan.ahead not_eof >> Token.pos_of) -- scan >> Library.swap;
fun source_position atom = Scan.ahead atom |-- not_eof >> Token.source_position_of;
fun inner_syntax atom = Scan.ahead atom |-- not_eof >> Token.inner_syntax_of;
--- a/src/Pure/Isar/proof.ML Mon Feb 24 10:16:10 2014 +0100
+++ b/src/Pure/Isar/proof.ML Mon Feb 24 13:52:48 2014 +0100
@@ -825,8 +825,7 @@
val (finish_text, terminal_pos, finished_pos) =
(case opt_text of
NONE => (Method.finish_text (NONE, immed), Position.none, prev_pos)
- | SOME (text, (pos, end_pos)) =>
- (Method.finish_text (SOME text, immed), Position.set_range (pos, end_pos), end_pos));
+ | SOME (text, (pos, end_pos)) => (Method.finish_text (SOME text, immed), pos, end_pos));
in
Seq.APPEND (fn state =>
state
@@ -861,11 +860,11 @@
fun apply_end text = assert_forward #> refine_end text;
-fun apply_results (text, range) =
- Seq.APPEND (apply text #> Seq.make_results, method_error "" (Position.set_range range));
+fun apply_results (text, (pos, _)) =
+ Seq.APPEND (apply text #> Seq.make_results, method_error "" pos);
-fun apply_end_results (text, range) =
- Seq.APPEND (apply_end text #> Seq.make_results, method_error "" (Position.set_range range));
+fun apply_end_results (text, (pos, _)) =
+ Seq.APPEND (apply_end text #> Seq.make_results, method_error "" pos);
--- a/src/Pure/Isar/token.ML Mon Feb 24 10:16:10 2014 +0100
+++ b/src/Pure/Isar/token.ML Mon Feb 24 13:52:48 2014 +0100
@@ -16,10 +16,8 @@
Attribute of morphism -> attribute | Files of file Exn.result list
type T
val str_of_kind: kind -> string
- val position_of: T -> Position.T
- val end_position_of: T -> Position.T
- val position_range_of: T list -> Position.range
- val pos_of: T -> string
+ val pos_of: T -> Position.T
+ val range_of: T list -> Position.range
val eof: T
val is_eof: T -> bool
val not_eof: T -> bool
@@ -130,13 +128,13 @@
(* position *)
-fun position_of (Token ((_, (pos, _)), _, _)) = pos;
-fun end_position_of (Token ((_, (_, pos)), _, _)) = pos;
+fun pos_of (Token ((_, (pos, _)), _, _)) = pos;
+fun end_pos_of (Token ((_, (_, pos)), _, _)) = pos;
-fun position_range_of [] = Position.no_range
- | position_range_of toks = (position_of (hd toks), end_position_of (List.last toks));
-
-val pos_of = Position.here o position_of;
+fun range_of (toks as tok :: _) =
+ let val pos' = end_pos_of (List.last toks)
+ in Position.range (pos_of tok) pos' end
+ | range_of [] = Position.no_range;
(* control tokens *)
@@ -153,7 +151,7 @@
| not_sync _ = true;
val stopper =
- Scan.stopper (fn [] => eof | toks => mk_eof (end_position_of (List.last toks))) is_eof;
+ Scan.stopper (fn [] => eof | toks => mk_eof (end_pos_of (List.last toks))) is_eof;
(* kind of token *)
@@ -251,8 +249,7 @@
fun put_files [] tok = tok
| put_files files (Token (x, y, Slot)) = Token (x, y, Value (SOME (Files files)))
- | put_files _ tok =
- raise Fail ("Cannot put inlined files here" ^ Position.here (position_of tok));
+ | put_files _ tok = raise Fail ("Cannot put inlined files here" ^ Position.here (pos_of tok));
(* access values *)
--- a/src/Pure/PIDE/command.ML Mon Feb 24 10:16:10 2014 +0100
+++ b/src/Pure/PIDE/command.ML Mon Feb 24 13:52:48 2014 +0100
@@ -128,12 +128,11 @@
val outer_syntax = #2 (Outer_Syntax.get_syntax ());
val command_reports = Outer_Syntax.command_reports outer_syntax;
- val proper_range =
- Position.set_range (Token.position_range_of (#1 (take_suffix Token.is_improper span)));
+ val proper_range = Token.range_of (#1 (take_suffix Token.is_improper span));
val pos =
(case find_first Token.is_command span of
- SOME tok => Token.position_of tok
- | NONE => proper_range);
+ SOME tok => Token.pos_of tok
+ | NONE => #1 proper_range);
val (is_malformed, token_reports) = Thy_Syntax.reports_of_tokens span;
val _ = Position.reports_text (token_reports @ maps command_reports span);
@@ -145,9 +144,9 @@
if Keyword.is_control (Toplevel.name_of tr) then
Toplevel.malformed pos "Illegal control command"
else Toplevel.modify_init init tr
- | [] => Toplevel.ignored (Position.set_range (Token.position_range_of span))
- | _ => Toplevel.malformed proper_range "Exactly one command expected")
- handle ERROR msg => Toplevel.malformed proper_range msg
+ | [] => Toplevel.ignored (#1 (Token.range_of span))
+ | _ => Toplevel.malformed (#1 proper_range) "Exactly one command expected")
+ handle ERROR msg => Toplevel.malformed (#1 proper_range) msg
end;
--- a/src/Pure/PIDE/document.scala Mon Feb 24 10:16:10 2014 +0100
+++ b/src/Pure/PIDE/document.scala Mon Feb 24 13:52:48 2014 +0100
@@ -634,6 +634,10 @@
(thy_load_commands zip other.thy_load_commands).forall(eq_commands)
}
+ override def toString: String =
+ "Snapshot(node = " + node_name.node + ", version = " + version.id +
+ (if (is_outdated) ", outdated" else "") + ")"
+
/* cumulate markup */
--- a/src/Pure/Thy/thy_load.ML Mon Feb 24 10:16:10 2014 +0100
+++ b/src/Pure/Thy/thy_load.ML Mon Feb 24 13:52:48 2014 +0100
@@ -85,7 +85,7 @@
[] =>
let
val master_dir = master_directory thy;
- val pos = Token.position_of tok;
+ val pos = Token.pos_of tok;
val src_paths = Keyword.command_files cmd (Path.explode name);
in map (Command.read_file master_dir pos) src_paths end
| files => map Exn.release files));
--- a/src/Pure/Thy/thy_syntax.ML Mon Feb 24 10:16:10 2014 +0100
+++ b/src/Pure/Thy/thy_syntax.ML Mon Feb 24 13:52:48 2014 +0100
@@ -86,7 +86,7 @@
then SOME ((pos, Markup.bad), "Malformed symbolic character") else NONE);
val is_malformed = Token.is_error tok orelse not (null malformed_symbols);
val (markup, txt) = token_markup tok;
- val reports = ((Token.position_of tok, markup), txt) :: malformed_symbols;
+ val reports = ((Token.pos_of tok, markup), txt) :: malformed_symbols;
in (is_malformed, reports) end;
in
@@ -121,7 +121,7 @@
fun make_span toks =
if not (null toks) andalso Token.is_command (hd toks) then
- Span (Command (Token.content_of (hd toks), Token.position_of (hd toks)), toks)
+ Span (Command (Token.content_of (hd toks), Token.pos_of (hd toks)), toks)
else if forall Token.is_improper toks then Span (Ignored, toks)
else Span (Malformed, toks);
@@ -162,8 +162,8 @@
if Token.is_command tok then
toks |> get_first (fn (i, tok) =>
if Token.is_name tok then
- SOME (i, (Path.explode (Token.content_of tok), Token.position_of tok))
- handle ERROR msg => error (msg ^ Token.pos_of tok)
+ SOME (i, (Path.explode (Token.content_of tok), Token.pos_of tok))
+ handle ERROR msg => error (msg ^ Position.here (Token.pos_of tok))
else NONE)
else NONE
| find_file [] = NONE;
--- a/src/Tools/induct_tacs.ML Mon Feb 24 10:16:10 2014 +0100
+++ b/src/Tools/induct_tacs.ML Mon Feb 24 13:52:48 2014 +0100
@@ -23,7 +23,8 @@
val u = singleton (Variable.polymorphic ctxt) t;
val U = Term.fastype_of u;
val _ = Term.is_TVar U andalso
- error ("Cannot determine type of " ^ Syntax.string_of_term ctxt u ^ Position.here pos);
+ error ("Cannot determine type of " ^
+ quote (Syntax.string_of_term ctxt u) ^ Position.here pos);
in (u, U) end;
fun gen_case_tac ctxt0 s opt_rule i st =
@@ -75,17 +76,17 @@
val pos = Syntax.read_token_pos name;
val (x, _) = Term.dest_Free t handle TERM _ =>
error ("Induction argument not a variable: " ^
- Syntax.string_of_term ctxt t ^ Position.here pos);
+ quote (Syntax.string_of_term ctxt t) ^ Position.here pos);
val eq_x = fn Free (y, _) => x = y | _ => false;
val _ =
if Term.exists_subterm eq_x concl then ()
else
error ("No such variable in subgoal: " ^
- Syntax.string_of_term ctxt t ^ Position.here pos);
+ quote (Syntax.string_of_term ctxt t) ^ Position.here pos);
val _ =
if (exists o Term.exists_subterm) eq_x prems then
warning ("Induction variable occurs also among premises: " ^
- Syntax.string_of_term ctxt t ^ Position.here pos)
+ quote (Syntax.string_of_term ctxt t) ^ Position.here pos)
else ();
in #1 (check_type ctxt (t, pos)) end;
--- a/src/Tools/jEdit/etc/options Mon Feb 24 10:16:10 2014 +0100
+++ b/src/Tools/jEdit/etc/options Mon Feb 24 13:52:48 2014 +0100
@@ -85,6 +85,7 @@
option keyword1_color : string = "006699FF"
option keyword2_color : string = "009966FF"
option keyword3_color : string = "0099FFFF"
+option caret_invisible_color : string = "99999980"
option tfree_color : string = "A020F0FF"
option tvar_color : string = "A020F0FF"
--- a/src/Tools/jEdit/src/completion_popup.scala Mon Feb 24 10:16:10 2014 +0100
+++ b/src/Tools/jEdit/src/completion_popup.scala Mon Feb 24 13:52:48 2014 +0100
@@ -19,7 +19,7 @@
import scala.swing.event.MouseClicked
import org.gjt.sp.jedit.View
-import org.gjt.sp.jedit.textarea.JEditTextArea
+import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea}
import org.gjt.sp.jedit.gui.{HistoryTextField, KeyEventWorkaround}
@@ -31,11 +31,20 @@
{
private val key = new Object
- def apply(text_area: JEditTextArea): Option[Completion_Popup.Text_Area] =
+ def apply(text_area: TextArea): Option[Completion_Popup.Text_Area] =
+ {
+ Swing_Thread.require()
text_area.getClientProperty(key) match {
case text_area_completion: Completion_Popup.Text_Area => Some(text_area_completion)
case _ => None
}
+ }
+
+ def active_range(text_area: TextArea): Option[Text.Range] =
+ apply(text_area) match {
+ case Some(text_area_completion) => text_area_completion.active_range
+ case None => None
+ }
def exit(text_area: JEditTextArea)
{
@@ -57,7 +66,7 @@
text_area_completion
}
- def dismissed(text_area: JEditTextArea): Boolean =
+ def dismissed(text_area: TextArea): Boolean =
{
Swing_Thread.require()
apply(text_area) match {
@@ -69,8 +78,19 @@
class Text_Area private(text_area: JEditTextArea)
{
+ // owned by Swing thread
private var completion_popup: Option[Completion_Popup] = None
+ def active_range: Option[Text.Range] =
+ completion_popup match {
+ case Some(completion) =>
+ completion.active_range match {
+ case Some((range, _)) if completion.isDisplayable => Some(range)
+ case _ => None
+ }
+ case None => None
+ }
+
/* completion action */
@@ -109,14 +129,17 @@
val font =
painter.getFont.deriveFont(Rendering.font_size("jedit_popup_font_scale"))
- val loc1 = text_area.offsetToXY(result.range.start)
+ val range = result.range
+ def invalidate(): Unit = JEdit_Lib.invalidate_range(text_area, range)
+
+ val loc1 = text_area.offsetToXY(range.start)
if (loc1 != null) {
val loc2 =
SwingUtilities.convertPoint(painter,
loc1.x, loc1.y + painter.getFontMetrics.getHeight, layered)
val completion =
- new Completion_Popup(layered, loc2, font, result.items) {
+ new Completion_Popup(Some((range, invalidate _)), layered, loc2, font, result.items) {
override def complete(item: Completion.Item) {
PIDE.completion_history.update(item)
insert(item)
@@ -128,6 +151,7 @@
override def refocus() { text_area.requestFocus }
}
completion_popup = Some(completion)
+ invalidate()
completion.show_popup()
}
}
@@ -270,6 +294,7 @@
// see https://forums.oracle.com/thread/1361677
if (GUI.is_macos_laf) text_field.setCaret(new DefaultCaret)
+ // owned by Swing thread
private var completion_popup: Option[Completion_Popup] = None
@@ -328,7 +353,8 @@
val loc =
SwingUtilities.convertPoint(text_field, fm.stringWidth(text), fm.getHeight, layered)
- val completion = new Completion_Popup(layered, loc, text_field.getFont, result.items)
+ val completion =
+ new Completion_Popup(None, layered, loc, text_field.getFont, result.items)
{
override def complete(item: Completion.Item) {
PIDE.completion_history.update(item)
@@ -395,6 +421,7 @@
class Completion_Popup private(
+ val active_range: Option[(Text.Range, () => Unit)],
layered: JLayeredPane,
location: Point,
font: Font,
@@ -535,6 +562,7 @@
private val hide_popup_delay =
Swing_Thread.delay_last(PIDE.options.seconds("jedit_completion_dismiss_delay")) {
+ active_range match { case Some((_, invalidate)) => invalidate() case _ => }
popup.hide
}
@@ -542,8 +570,10 @@
{
if (list_view.peer.isFocusOwner) refocus()
- if (PIDE.options.seconds("jedit_completion_dismiss_delay").is_zero)
+ if (PIDE.options.seconds("jedit_completion_dismiss_delay").is_zero) {
+ active_range match { case Some((_, invalidate)) => invalidate() case _ => }
popup.hide
+ }
else hide_popup_delay.invoke()
}
}
--- a/src/Tools/jEdit/src/document_view.scala Mon Feb 24 10:16:10 2014 +0100
+++ b/src/Tools/jEdit/src/document_view.scala Mon Feb 24 13:52:48 2014 +0100
@@ -18,7 +18,7 @@
import org.gjt.sp.jedit.jEdit
import org.gjt.sp.jedit.options.GutterOptionPane
-import org.gjt.sp.jedit.textarea.{JEditTextArea, TextAreaExtension, TextAreaPainter}
+import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea, TextAreaExtension, TextAreaPainter}
object Document_View
@@ -27,7 +27,7 @@
private val key = new Object
- def apply(text_area: JEditTextArea): Option[Document_View] =
+ def apply(text_area: TextArea): Option[Document_View] =
{
Swing_Thread.require()
text_area.getClientProperty(key) match {
--- a/src/Tools/jEdit/src/plugin.scala Mon Feb 24 10:16:10 2014 +0100
+++ b/src/Tools/jEdit/src/plugin.scala Mon Feb 24 13:52:48 2014 +0100
@@ -68,7 +68,7 @@
def document_model(buffer: Buffer): Option[Document_Model] = Document_Model(buffer)
- def document_view(text_area: JEditTextArea): Option[Document_View] = Document_View(text_area)
+ def document_view(text_area: TextArea): Option[Document_View] = Document_View(text_area)
def document_views(buffer: Buffer): List[Document_View] =
for {
--- a/src/Tools/jEdit/src/rendering.scala Mon Feb 24 10:16:10 2014 +0100
+++ b/src/Tools/jEdit/src/rendering.scala Mon Feb 24 13:52:48 2014 +0100
@@ -222,6 +222,9 @@
class Rendering private(val snapshot: Document.Snapshot, val options: Options)
{
+ override def toString: String = "Rendering(" + snapshot.toString + ")"
+
+
/* colors */
def color_value(s: String): Color = Color_Value(options.string(s))
@@ -257,6 +260,7 @@
val keyword1_color = color_value("keyword1_color")
val keyword2_color = color_value("keyword2_color")
val keyword3_color = color_value("keyword3_color")
+ val caret_invisible_color = color_value("caret_invisible_color")
val tfree_color = color_value("tfree_color")
val tvar_color = color_value("tvar_color")
--- a/src/Tools/jEdit/src/rich_text_area.scala Mon Feb 24 10:16:10 2014 +0100
+++ b/src/Tools/jEdit/src/rich_text_area.scala Mon Feb 24 13:52:48 2014 +0100
@@ -222,16 +222,25 @@
}
- /* text background */
+ /* caret */
private def get_caret_range(stretch: Boolean): Text.Range =
- if (caret_visible && text_area.isCaretVisible) {
+ 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
{
override def paintScreenLineRange(gfx: Graphics2D,
@@ -360,7 +369,7 @@
val astr = new AttributedString(s2)
astr.addAttribute(TextAttribute.FONT, chunk_font)
- astr.addAttribute(TextAttribute.FOREGROUND, painter.getCaretColor)
+ astr.addAttribute(TextAttribute.FOREGROUND, get_caret_color(rendering))
astr.addAttribute(TextAttribute.SWAP_COLORS, TextAttribute.SWAP_COLORS_ON)
gfx.drawString(astr.getIterator, x1 + string_width(s1), y)
@@ -446,7 +455,6 @@
start: Array[Int], end: Array[Int], y: Int, line_height: Int)
{
robust_rendering { rendering =>
- val painter = text_area.getPainter
val caret_range = get_caret_range(true)
for (i <- 0 until physical_lines.length) {
@@ -483,14 +491,22 @@
}
// completion range
- for {
- caret <- caret_range.try_restrict(line_range)
- if !hyperlink_area.is_active
- names <- rendering.completion_names(caret)
- r <- JEdit_Lib.gfx_range(text_area, names.range)
- } {
- gfx.setColor(painter.getCaretColor)
- gfx.drawRect(r.x, y + i * line_height, r.length - 1, line_height - 1)
+ if (!hyperlink_area.is_active) {
+ def paint_completion(range: Text.Range) {
+ for (r <- JEdit_Lib.gfx_range(text_area, range)) {
+ gfx.setColor(get_caret_color(rendering))
+ 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)
+ }
}
}
}
@@ -523,8 +539,8 @@
override def paintValidLine(gfx: Graphics2D,
screen_line: Int, physical_line: Int, start: Int, end: Int, y: Int)
{
- robust_rendering { _ =>
- if (caret_visible && text_area.isCaretVisible) {
+ robust_rendering { rendering =>
+ if (caret_visible) {
val caret = text_area.getCaretPosition
if (start <= caret && caret == end - 1) {
val painter = text_area.getPainter
@@ -533,7 +549,7 @@
val offset = caret - text_area.getLineStartOffset(physical_line)
val x = text_area.offsetToXY(physical_line, offset).x
- gfx.setColor(painter.getCaretColor)
+ gfx.setColor(get_caret_color(rendering))
gfx.drawRect(x, y, (metric.unit * metric.average).round.toInt - 1, fm.getHeight - 1)
}
}