# HG changeset patch
# User wenzelm
# Date 1393246368 -3600
# Node ID 601ea66c5bcdda5c878a0f032b8ae6edf926d92b
# Parent  50cf04dd258433d8bf1f34c52a71c01dd09d0d0d# Parent  2a6a8f9d52e1f48a91d562b961e31c19bce5258f
merged

diff -r 50cf04dd2584 -r 601ea66c5bcd NEWS
--- 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.
diff -r 50cf04dd2584 -r 601ea66c5bcd src/Pure/General/completion.scala
--- 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)
diff -r 50cf04dd2584 -r 601ea66c5bcd src/Pure/General/symbol_pos.ML
--- 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 =>
diff -r 50cf04dd2584 -r 601ea66c5bcd src/Pure/Isar/args.ML
--- 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 *)
diff -r 50cf04dd2584 -r 601ea66c5bcd src/Pure/Isar/method.ML
--- 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 *)
diff -r 50cf04dd2584 -r 601ea66c5bcd src/Pure/Isar/outer_syntax.ML
--- 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 [];
 
diff -r 50cf04dd2584 -r 601ea66c5bcd src/Pure/Isar/parse.ML
--- 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;
 
diff -r 50cf04dd2584 -r 601ea66c5bcd src/Pure/Isar/proof.ML
--- 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);
 
 
 
diff -r 50cf04dd2584 -r 601ea66c5bcd src/Pure/Isar/token.ML
--- 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 *)
diff -r 50cf04dd2584 -r 601ea66c5bcd src/Pure/PIDE/command.ML
--- 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;
 
 
diff -r 50cf04dd2584 -r 601ea66c5bcd src/Pure/PIDE/document.scala
--- 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 */
 
diff -r 50cf04dd2584 -r 601ea66c5bcd src/Pure/Thy/thy_load.ML
--- 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));
diff -r 50cf04dd2584 -r 601ea66c5bcd src/Pure/Thy/thy_syntax.ML
--- 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;
diff -r 50cf04dd2584 -r 601ea66c5bcd src/Tools/induct_tacs.ML
--- 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;
 
diff -r 50cf04dd2584 -r 601ea66c5bcd src/Tools/jEdit/etc/options
--- 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"
diff -r 50cf04dd2584 -r 601ea66c5bcd src/Tools/jEdit/src/completion_popup.scala
--- 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()
   }
 }
diff -r 50cf04dd2584 -r 601ea66c5bcd src/Tools/jEdit/src/document_view.scala
--- 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 {
diff -r 50cf04dd2584 -r 601ea66c5bcd src/Tools/jEdit/src/plugin.scala
--- 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 {
diff -r 50cf04dd2584 -r 601ea66c5bcd src/Tools/jEdit/src/rendering.scala
--- 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")
diff -r 50cf04dd2584 -r 601ea66c5bcd src/Tools/jEdit/src/rich_text_area.scala
--- 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)
           }
         }