# HG changeset patch
# User wenzelm
# Date 1460669470 -7200
# Node ID dc8a8a7559e7acfd936793d7c36751e2e0f2c5d0
# Parent  9d2fae6b31ccb3bc985ce9cc519ae8207415d46d
highlighting of entity def/ref positions wrt. cursor;

diff -r 9d2fae6b31cc -r dc8a8a7559e7 NEWS
--- a/NEWS	Thu Apr 14 22:55:53 2016 +0200
+++ b/NEWS	Thu Apr 14 23:31:10 2016 +0200
@@ -41,6 +41,8 @@
 results are isolated from the actual Isabelle/Pure that runs the IDE
 itself.
 
+* Highlighting of entity def/ref positions wrt. cursor.
+
 
 *** Isar ***
 
diff -r 9d2fae6b31cc -r dc8a8a7559e7 src/Pure/General/name_space.ML
--- a/src/Pure/General/name_space.ML	Thu Apr 14 22:55:53 2016 +0200
+++ b/src/Pure/General/name_space.ML	Thu Apr 14 23:31:10 2016 +0200
@@ -13,6 +13,7 @@
   val empty: string -> T
   val kind_of: T -> string
   val markup: T -> string -> Markup.T
+  val markup_def: T -> string -> Markup.T
   val the_entry: T -> string ->
     {concealed: bool, group: serial option, theory_name: string, pos: Position.T, serial: serial}
   val entry_ord: T -> string * string -> order
@@ -156,10 +157,13 @@
 
 fun kind_of (Name_Space {kind, ...}) = kind;
 
-fun markup (Name_Space {kind, entries, ...}) name =
+fun gen_markup def (Name_Space {kind, entries, ...}) name =
   (case Change_Table.lookup entries name of
     NONE => Markup.intensify
-  | SOME (_, entry) => entry_markup false kind (name, entry));
+  | SOME (_, entry) => entry_markup def kind (name, entry));
+
+val markup = gen_markup false;
+val markup_def = gen_markup true;
 
 fun undefined (space as Name_Space {kind, entries, ...}) bad =
   let
diff -r 9d2fae6b31cc -r dc8a8a7559e7 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Thu Apr 14 22:55:53 2016 +0200
+++ b/src/Pure/Isar/proof_context.ML	Thu Apr 14 23:31:10 2016 +0200
@@ -1193,6 +1193,11 @@
   let
     val (vars, _) = fold_map prep_var raw_vars ctxt;
     val (xs, ctxt') = Variable.add_fixes_binding (map #1 vars) ctxt;
+    val _ =
+      Context_Position.reports ctxt'
+        (flat (map2 (fn x => fn pos =>
+          [(pos, Variable.markup ctxt' x), (pos, Variable.markup_entity_def ctxt' x)])
+            xs (map (Binding.pos_of o #1) vars)));
     val vars' = map2 (fn x => fn (_, opt_T, mx) => (x, opt_T, mx)) xs vars;
     val (Ts, ctxt'') = fold_map declare_var vars' ctxt';
     val vars'' = map2 (fn T => fn (x, _, mx) => (x, T, mx)) Ts vars';
diff -r 9d2fae6b31cc -r dc8a8a7559e7 src/Pure/Syntax/syntax_phases.ML
--- a/src/Pure/Syntax/syntax_phases.ML	Thu Apr 14 22:55:53 2016 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML	Thu Apr 14 23:31:10 2016 +0200
@@ -51,9 +51,7 @@
   [Name_Space.markup (Consts.space_of (Proof_Context.consts_of ctxt)) c];
 
 fun markup_free ctxt x =
-  (if Variable.is_improper ctxt x then Markup.improper
-   else if Name.is_skolem x then Markup.skolem
-   else Markup.free) ::
+  Variable.markup ctxt x ::
   (if Variable.is_body ctxt orelse Variable.is_fixed ctxt x
    then [Variable.markup_fixed ctxt x]
    else []);
diff -r 9d2fae6b31cc -r dc8a8a7559e7 src/Pure/variable.ML
--- a/src/Pure/variable.ML	Thu Apr 14 22:55:53 2016 +0200
+++ b/src/Pure/variable.ML	Thu Apr 14 23:31:10 2016 +0200
@@ -43,9 +43,12 @@
   val is_newly_fixed: Proof.context -> Proof.context -> string -> bool
   val fixed_ord: Proof.context -> string * string -> order
   val intern_fixed: Proof.context -> string -> string
-  val markup_fixed: Proof.context -> string -> Markup.T
   val lookup_fixed: Proof.context -> string -> string option
   val revert_fixed: Proof.context -> string -> string
+  val markup_fixed: Proof.context -> string -> Markup.T
+  val markup: Proof.context -> string -> Markup.T
+  val markup_entity_def: Proof.context -> string -> Markup.T
+  val dest_fixes: Proof.context -> (string * string) list
   val add_fixed_names: Proof.context -> term -> string list -> string list
   val add_fixed: Proof.context -> term -> (string * typ) list -> (string * typ) list
   val add_newly_fixed: Proof.context -> Proof.context ->
@@ -58,7 +61,6 @@
   val auto_fixes: term -> Proof.context -> Proof.context
   val fix_dummy_patterns: term -> Proof.context -> term * Proof.context
   val variant_fixes: string list -> Proof.context -> string list * Proof.context
-  val dest_fixes: Proof.context -> (string * string) list
   val gen_all: Proof.context -> thm -> thm
   val export_terms: Proof.context -> Proof.context -> term list -> term list
   val exportT_terms: Proof.context -> Proof.context -> term list -> term list
@@ -375,6 +377,13 @@
   Name_Space.markup (fixes_space ctxt) x
   |> Markup.name (revert_fixed ctxt x);
 
+fun markup ctxt x =
+  if is_improper ctxt x then Markup.improper
+  else if Name.is_skolem x then Markup.skolem
+  else Markup.free;
+
+val markup_entity_def = Name_Space.markup_def o fixes_space;
+
 fun dest_fixes ctxt =
   Name_Space.fold_table (fn (x, (y, _)) => cons (y, x)) (fixes_of ctxt) []
   |> sort (Name_Space.entry_ord (fixes_space ctxt) o apply2 #2);