# HG changeset patch
# User wenzelm
# Date 1466604243 -7200
# Node ID e344dc82f6c22c97ccf4ea86042d0ebd7c4dfdd2
# Parent  c8366fb67538e43b127929ec3b745bcb957d5e8a
report class parameters within instantiation;

diff -r c8366fb67538 -r e344dc82f6c2 src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Wed Jun 22 11:10:18 2016 +0200
+++ b/src/Pure/Isar/class.ML	Wed Jun 22 16:04:03 2016 +0200
@@ -12,18 +12,18 @@
   val base_sort: theory -> class -> sort
   val rules: theory -> class -> thm option * thm
   val these_defs: theory -> sort -> thm list
-  val these_operations: theory -> sort
-    -> (string * (class * ((typ * term) * bool))) list
+  val these_operations: theory -> sort -> (string * (class * ((typ * term) * bool))) list
   val print_classes: Proof.context -> unit
   val init: class -> theory -> Proof.context
   val begin: class list -> sort -> Proof.context -> Proof.context
-  val const: class -> (binding * mixfix) * term -> term list * term list -> local_theory -> local_theory
-  val abbrev: class -> Syntax.mode -> (binding * mixfix) * term -> local_theory -> (term * term) * local_theory
+  val const: class -> (binding * mixfix) * term -> term list * term list ->
+    local_theory -> local_theory
+  val abbrev: class -> Syntax.mode -> (binding * mixfix) * term -> local_theory ->
+    (term * term) * local_theory
   val redeclare_operations: theory -> sort -> Proof.context -> Proof.context
   val class_prefix: string -> string
-  val register: class -> class list -> ((string * typ) * (string * typ)) list
-    -> sort -> morphism -> morphism -> thm option -> thm option -> thm
-    -> theory -> theory
+  val register: class -> class list -> ((string * typ) * (string * typ)) list ->
+    sort -> morphism -> morphism -> thm option -> thm option -> thm -> theory -> theory
 
   (*instances*)
   val instantiation: string list * (string * sort) list * sort -> theory -> local_theory
@@ -160,6 +160,11 @@
 
 val export_morphism = #export_morph oo the_class_data;
 
+fun pretty_param ctxt (c, ty) =
+  Pretty.block
+   [Name_Space.pretty ctxt (Proof_Context.const_space ctxt) c, Pretty.str " ::",
+    Pretty.brk 1, Syntax.pretty_typ ctxt ty];
+
 fun print_classes ctxt =
   let
     val thy = Proof_Context.theory_of ctxt;
@@ -167,7 +172,6 @@
 
     val class_space = Proof_Context.class_space ctxt;
     val type_space = Proof_Context.type_space ctxt;
-    val const_space = Proof_Context.const_space ctxt;
 
     val arities =
       Symtab.empty
@@ -183,10 +187,7 @@
         val Ss = Sorts.mg_domain algebra tyco [class];
       in Syntax.pretty_arity ctxt (tyco, Ss, [class]) end;
 
-    fun prt_param (c, ty) =
-      Pretty.block
-       [Name_Space.pretty ctxt const_space c, Pretty.str " ::",
-        Pretty.brk 1, Syntax.pretty_typ ctxt (Type.strip_sorts_dummy ty)];
+    fun prt_param (c, ty) = pretty_param ctxt (c, Type.strip_sorts_dummy ty);
 
     fun prt_entry class =
       Pretty.block
@@ -607,16 +608,28 @@
 
 (* target *)
 
-fun define_overloaded (c, U) v (b_def, rhs) =
-  Local_Theory.background_theory_result (Axclass.declare_overloaded (c, U)
-  ##>> Axclass.define_overloaded b_def (c, rhs))
-  ##> (map_instantiation o apsnd) (filter_out (fn (_, (v', _)) => v' = v))
-  ##> Local_Theory.map_contexts (K synchronize_inst_syntax);
+fun define_overloaded (c, U) b (b_def, rhs) lthy =
+  let
+    val name = Binding.name_of b;
+    val pos = Binding.pos_of b;
+    val _ =
+      if Context_Position.is_reported lthy pos then
+        Position.report_text pos Markup.class_parameter
+          (Pretty.string_of
+            (Pretty.block [Pretty.keyword1 "class", Pretty.brk 1,
+                Pretty.str "parameter", Pretty.brk 1, pretty_param lthy (c, U)]))
+      else ();
+  in
+    lthy |> Local_Theory.background_theory_result
+      (Axclass.declare_overloaded (c, U) ##>> Axclass.define_overloaded b_def (c, rhs))
+    ||> (map_instantiation o apsnd) (filter_out (fn (_, (v', _)) => v' = name))
+    ||> Local_Theory.map_contexts (K synchronize_inst_syntax)
+  end;
 
 fun foundation (((b, U), mx), (b_def, rhs)) params lthy =
   (case instantiation_param lthy b of
     SOME c =>
-      if Mixfix.is_empty mx then lthy |> define_overloaded (c, U) (Binding.name_of b) (b_def, rhs)
+      if Mixfix.is_empty mx then lthy |> define_overloaded (c, U) b (b_def, rhs)
       else error ("Illegal mixfix syntax for overloaded constant " ^ quote c)
   | NONE => lthy |> Generic_Target.theory_target_foundation (((b, U), mx), (b_def, rhs)) params);
 
diff -r c8366fb67538 -r e344dc82f6c2 src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Wed Jun 22 11:10:18 2016 +0200
+++ b/src/Pure/PIDE/markup.ML	Wed Jun 22 16:04:03 2016 +0200
@@ -103,6 +103,7 @@
   val token_rangeN: string val token_range: T
   val sortingN: string val sorting: T
   val typingN: string val typing: T
+  val class_parameterN: string val class_parameter: T
   val ML_keyword1N: string val ML_keyword1: T
   val ML_keyword2N: string val ML_keyword2: T
   val ML_keyword3N: string val ML_keyword3: T
@@ -468,6 +469,7 @@
 
 val (sortingN, sorting) = markup_elem "sorting";
 val (typingN, typing) = markup_elem "typing";
+val (class_parameterN, class_parameter) = markup_elem "class_parameter";
 
 
 (* ML *)
diff -r c8366fb67538 -r e344dc82f6c2 src/Pure/PIDE/markup.scala
--- a/src/Pure/PIDE/markup.scala	Wed Jun 22 11:10:18 2016 +0200
+++ b/src/Pure/PIDE/markup.scala	Wed Jun 22 16:04:03 2016 +0200
@@ -267,6 +267,7 @@
 
   val SORTING = "sorting"
   val TYPING = "typing"
+  val CLASS_PARAMETER = "class_parameter"
 
   val ATTRIBUTE = "attribute"
   val METHOD = "method"
diff -r c8366fb67538 -r e344dc82f6c2 src/Tools/jEdit/etc/options
--- a/src/Tools/jEdit/etc/options	Wed Jun 22 11:10:18 2016 +0200
+++ b/src/Tools/jEdit/etc/options	Wed Jun 22 16:04:03 2016 +0200
@@ -133,6 +133,7 @@
 option inner_cartouche_color : string = "CC6600FF"
 option inner_comment_color : string = "CC0000FF"
 option dynamic_color : string = "7BA428FF"
+option class_parameter_color : string = "D2691EFF"
 
 option markdown_item_color1 : string = "DAFEDAFF"
 option markdown_item_color2 : string = "FFF0CCFF"
diff -r c8366fb67538 -r e344dc82f6c2 src/Tools/jEdit/src/rendering.scala
--- a/src/Tools/jEdit/src/rendering.scala	Wed Jun 22 11:10:18 2016 +0200
+++ b/src/Tools/jEdit/src/rendering.scala	Wed Jun 22 16:04:03 2016 +0200
@@ -156,7 +156,7 @@
   private val highlight_elements =
     Markup.Elements(Markup.EXPRESSION, Markup.CITATION, Markup.LANGUAGE, Markup.ML_TYPING,
       Markup.TOKEN_RANGE, Markup.ENTITY, Markup.PATH, Markup.DOC, Markup.URL, Markup.SORTING,
-      Markup.TYPING, Markup.FREE, Markup.SKOLEM, Markup.BOUND,
+      Markup.TYPING, Markup.CLASS_PARAMETER, Markup.FREE, Markup.SKOLEM, Markup.BOUND,
       Markup.VAR, Markup.TFREE, Markup.TVAR, Markup.ML_BREAKPOINT,
       Markup.MARKDOWN_PARAGRAPH, Markup.Markdown_List.name)
 
@@ -185,9 +185,9 @@
 
   private val tooltip_elements =
     Markup.Elements(Markup.LANGUAGE, Markup.EXPRESSION, Markup.TIMING, Markup.ENTITY,
-      Markup.SORTING, Markup.TYPING, Markup.ML_TYPING, Markup.ML_BREAKPOINT, Markup.PATH,
-      Markup.DOC, Markup.URL, Markup.MARKDOWN_PARAGRAPH, Markup.Markdown_List.name) ++
-    Markup.Elements(tooltip_descriptions.keySet)
+      Markup.SORTING, Markup.TYPING, Markup.CLASS_PARAMETER, Markup.ML_TYPING,
+      Markup.ML_BREAKPOINT, Markup.PATH, Markup.DOC, Markup.URL, Markup.MARKDOWN_PARAGRAPH,
+      Markup.Markdown_List.name) ++ Markup.Elements(tooltip_descriptions.keySet)
 
   private val gutter_elements =
     Markup.Elements(Markup.WRITELN, Markup.INFORMATION, Markup.WARNING, Markup.LEGACY, Markup.ERROR)
@@ -287,6 +287,7 @@
   val inner_cartouche_color = color_value("inner_cartouche_color")
   val inner_comment_color = color_value("inner_comment_color")
   val dynamic_color = color_value("dynamic_color")
+  val class_parameter_color = color_value("class_parameter_color")
 
   val markdown_item_color1 = color_value("markdown_item_color1")
   val markdown_item_color2 = color_value("markdown_item_color2")
@@ -635,6 +636,9 @@
           if name == Markup.SORTING || name == Markup.TYPING =>
             Some(add(prev, r, (true, pretty_typing("::", body))))
 
+          case (prev, Text.Info(r, XML.Elem(Markup(Markup.CLASS_PARAMETER, _), body))) =>
+            Some(add(prev, r, (true, Pretty.block(0, body))))
+
           case (prev, Text.Info(r, XML.Elem(Markup(Markup.ML_TYPING, _), body))) =>
             Some(add(prev, r, (false, pretty_typing("ML:", body))))
 
@@ -867,6 +871,7 @@
       Markup.INNER_CARTOUCHE -> inner_cartouche_color,
       Markup.INNER_COMMENT -> inner_comment_color,
       Markup.DYNAMIC_FACT -> dynamic_color,
+      Markup.CLASS_PARAMETER -> class_parameter_color,
       Markup.ANTIQUOTE -> antiquote_color,
       Markup.ML_KEYWORD1 -> keyword1_color,
       Markup.ML_KEYWORD2 -> keyword2_color,