highlighting of entity def/ref positions wrt. cursor;
authorwenzelm
Thu Apr 14 23:31:10 2016 +0200 (2016-04-14)
changeset 62987dc8a8a7559e7
parent 62986 9d2fae6b31cc
child 62988 224e8d8a4fb8
highlighting of entity def/ref positions wrt. cursor;
NEWS
src/Pure/General/name_space.ML
src/Pure/Isar/proof_context.ML
src/Pure/Syntax/syntax_phases.ML
src/Pure/variable.ML
     1.1 --- a/NEWS	Thu Apr 14 22:55:53 2016 +0200
     1.2 +++ b/NEWS	Thu Apr 14 23:31:10 2016 +0200
     1.3 @@ -41,6 +41,8 @@
     1.4  results are isolated from the actual Isabelle/Pure that runs the IDE
     1.5  itself.
     1.6  
     1.7 +* Highlighting of entity def/ref positions wrt. cursor.
     1.8 +
     1.9  
    1.10  *** Isar ***
    1.11  
     2.1 --- a/src/Pure/General/name_space.ML	Thu Apr 14 22:55:53 2016 +0200
     2.2 +++ b/src/Pure/General/name_space.ML	Thu Apr 14 23:31:10 2016 +0200
     2.3 @@ -13,6 +13,7 @@
     2.4    val empty: string -> T
     2.5    val kind_of: T -> string
     2.6    val markup: T -> string -> Markup.T
     2.7 +  val markup_def: T -> string -> Markup.T
     2.8    val the_entry: T -> string ->
     2.9      {concealed: bool, group: serial option, theory_name: string, pos: Position.T, serial: serial}
    2.10    val entry_ord: T -> string * string -> order
    2.11 @@ -156,10 +157,13 @@
    2.12  
    2.13  fun kind_of (Name_Space {kind, ...}) = kind;
    2.14  
    2.15 -fun markup (Name_Space {kind, entries, ...}) name =
    2.16 +fun gen_markup def (Name_Space {kind, entries, ...}) name =
    2.17    (case Change_Table.lookup entries name of
    2.18      NONE => Markup.intensify
    2.19 -  | SOME (_, entry) => entry_markup false kind (name, entry));
    2.20 +  | SOME (_, entry) => entry_markup def kind (name, entry));
    2.21 +
    2.22 +val markup = gen_markup false;
    2.23 +val markup_def = gen_markup true;
    2.24  
    2.25  fun undefined (space as Name_Space {kind, entries, ...}) bad =
    2.26    let
     3.1 --- a/src/Pure/Isar/proof_context.ML	Thu Apr 14 22:55:53 2016 +0200
     3.2 +++ b/src/Pure/Isar/proof_context.ML	Thu Apr 14 23:31:10 2016 +0200
     3.3 @@ -1193,6 +1193,11 @@
     3.4    let
     3.5      val (vars, _) = fold_map prep_var raw_vars ctxt;
     3.6      val (xs, ctxt') = Variable.add_fixes_binding (map #1 vars) ctxt;
     3.7 +    val _ =
     3.8 +      Context_Position.reports ctxt'
     3.9 +        (flat (map2 (fn x => fn pos =>
    3.10 +          [(pos, Variable.markup ctxt' x), (pos, Variable.markup_entity_def ctxt' x)])
    3.11 +            xs (map (Binding.pos_of o #1) vars)));
    3.12      val vars' = map2 (fn x => fn (_, opt_T, mx) => (x, opt_T, mx)) xs vars;
    3.13      val (Ts, ctxt'') = fold_map declare_var vars' ctxt';
    3.14      val vars'' = map2 (fn T => fn (x, _, mx) => (x, T, mx)) Ts vars';
     4.1 --- a/src/Pure/Syntax/syntax_phases.ML	Thu Apr 14 22:55:53 2016 +0200
     4.2 +++ b/src/Pure/Syntax/syntax_phases.ML	Thu Apr 14 23:31:10 2016 +0200
     4.3 @@ -51,9 +51,7 @@
     4.4    [Name_Space.markup (Consts.space_of (Proof_Context.consts_of ctxt)) c];
     4.5  
     4.6  fun markup_free ctxt x =
     4.7 -  (if Variable.is_improper ctxt x then Markup.improper
     4.8 -   else if Name.is_skolem x then Markup.skolem
     4.9 -   else Markup.free) ::
    4.10 +  Variable.markup ctxt x ::
    4.11    (if Variable.is_body ctxt orelse Variable.is_fixed ctxt x
    4.12     then [Variable.markup_fixed ctxt x]
    4.13     else []);
     5.1 --- a/src/Pure/variable.ML	Thu Apr 14 22:55:53 2016 +0200
     5.2 +++ b/src/Pure/variable.ML	Thu Apr 14 23:31:10 2016 +0200
     5.3 @@ -43,9 +43,12 @@
     5.4    val is_newly_fixed: Proof.context -> Proof.context -> string -> bool
     5.5    val fixed_ord: Proof.context -> string * string -> order
     5.6    val intern_fixed: Proof.context -> string -> string
     5.7 -  val markup_fixed: Proof.context -> string -> Markup.T
     5.8    val lookup_fixed: Proof.context -> string -> string option
     5.9    val revert_fixed: Proof.context -> string -> string
    5.10 +  val markup_fixed: Proof.context -> string -> Markup.T
    5.11 +  val markup: Proof.context -> string -> Markup.T
    5.12 +  val markup_entity_def: Proof.context -> string -> Markup.T
    5.13 +  val dest_fixes: Proof.context -> (string * string) list
    5.14    val add_fixed_names: Proof.context -> term -> string list -> string list
    5.15    val add_fixed: Proof.context -> term -> (string * typ) list -> (string * typ) list
    5.16    val add_newly_fixed: Proof.context -> Proof.context ->
    5.17 @@ -58,7 +61,6 @@
    5.18    val auto_fixes: term -> Proof.context -> Proof.context
    5.19    val fix_dummy_patterns: term -> Proof.context -> term * Proof.context
    5.20    val variant_fixes: string list -> Proof.context -> string list * Proof.context
    5.21 -  val dest_fixes: Proof.context -> (string * string) list
    5.22    val gen_all: Proof.context -> thm -> thm
    5.23    val export_terms: Proof.context -> Proof.context -> term list -> term list
    5.24    val exportT_terms: Proof.context -> Proof.context -> term list -> term list
    5.25 @@ -375,6 +377,13 @@
    5.26    Name_Space.markup (fixes_space ctxt) x
    5.27    |> Markup.name (revert_fixed ctxt x);
    5.28  
    5.29 +fun markup ctxt x =
    5.30 +  if is_improper ctxt x then Markup.improper
    5.31 +  else if Name.is_skolem x then Markup.skolem
    5.32 +  else Markup.free;
    5.33 +
    5.34 +val markup_entity_def = Name_Space.markup_def o fixes_space;
    5.35 +
    5.36  fun dest_fixes ctxt =
    5.37    Name_Space.fold_table (fn (x, (y, _)) => cons (y, x)) (fixes_of ctxt) []
    5.38    |> sort (Name_Space.entry_ord (fixes_space ctxt) o apply2 #2);