report class parameters within instantiation;
authorwenzelm
Wed Jun 22 16:04:03 2016 +0200 (2016-06-22 ago)
changeset 63347e344dc82f6c2
parent 63346 c8366fb67538
child 63348 b3e5bdb784f5
child 63352 4eaf35781b23
report class parameters within instantiation;
src/Pure/Isar/class.ML
src/Pure/PIDE/markup.ML
src/Pure/PIDE/markup.scala
src/Tools/jEdit/etc/options
src/Tools/jEdit/src/rendering.scala
     1.1 --- a/src/Pure/Isar/class.ML	Wed Jun 22 11:10:18 2016 +0200
     1.2 +++ b/src/Pure/Isar/class.ML	Wed Jun 22 16:04:03 2016 +0200
     1.3 @@ -12,18 +12,18 @@
     1.4    val base_sort: theory -> class -> sort
     1.5    val rules: theory -> class -> thm option * thm
     1.6    val these_defs: theory -> sort -> thm list
     1.7 -  val these_operations: theory -> sort
     1.8 -    -> (string * (class * ((typ * term) * bool))) list
     1.9 +  val these_operations: theory -> sort -> (string * (class * ((typ * term) * bool))) list
    1.10    val print_classes: Proof.context -> unit
    1.11    val init: class -> theory -> Proof.context
    1.12    val begin: class list -> sort -> Proof.context -> Proof.context
    1.13 -  val const: class -> (binding * mixfix) * term -> term list * term list -> local_theory -> local_theory
    1.14 -  val abbrev: class -> Syntax.mode -> (binding * mixfix) * term -> local_theory -> (term * term) * local_theory
    1.15 +  val const: class -> (binding * mixfix) * term -> term list * term list ->
    1.16 +    local_theory -> local_theory
    1.17 +  val abbrev: class -> Syntax.mode -> (binding * mixfix) * term -> local_theory ->
    1.18 +    (term * term) * local_theory
    1.19    val redeclare_operations: theory -> sort -> Proof.context -> Proof.context
    1.20    val class_prefix: string -> string
    1.21 -  val register: class -> class list -> ((string * typ) * (string * typ)) list
    1.22 -    -> sort -> morphism -> morphism -> thm option -> thm option -> thm
    1.23 -    -> theory -> theory
    1.24 +  val register: class -> class list -> ((string * typ) * (string * typ)) list ->
    1.25 +    sort -> morphism -> morphism -> thm option -> thm option -> thm -> theory -> theory
    1.26  
    1.27    (*instances*)
    1.28    val instantiation: string list * (string * sort) list * sort -> theory -> local_theory
    1.29 @@ -160,6 +160,11 @@
    1.30  
    1.31  val export_morphism = #export_morph oo the_class_data;
    1.32  
    1.33 +fun pretty_param ctxt (c, ty) =
    1.34 +  Pretty.block
    1.35 +   [Name_Space.pretty ctxt (Proof_Context.const_space ctxt) c, Pretty.str " ::",
    1.36 +    Pretty.brk 1, Syntax.pretty_typ ctxt ty];
    1.37 +
    1.38  fun print_classes ctxt =
    1.39    let
    1.40      val thy = Proof_Context.theory_of ctxt;
    1.41 @@ -167,7 +172,6 @@
    1.42  
    1.43      val class_space = Proof_Context.class_space ctxt;
    1.44      val type_space = Proof_Context.type_space ctxt;
    1.45 -    val const_space = Proof_Context.const_space ctxt;
    1.46  
    1.47      val arities =
    1.48        Symtab.empty
    1.49 @@ -183,10 +187,7 @@
    1.50          val Ss = Sorts.mg_domain algebra tyco [class];
    1.51        in Syntax.pretty_arity ctxt (tyco, Ss, [class]) end;
    1.52  
    1.53 -    fun prt_param (c, ty) =
    1.54 -      Pretty.block
    1.55 -       [Name_Space.pretty ctxt const_space c, Pretty.str " ::",
    1.56 -        Pretty.brk 1, Syntax.pretty_typ ctxt (Type.strip_sorts_dummy ty)];
    1.57 +    fun prt_param (c, ty) = pretty_param ctxt (c, Type.strip_sorts_dummy ty);
    1.58  
    1.59      fun prt_entry class =
    1.60        Pretty.block
    1.61 @@ -607,16 +608,28 @@
    1.62  
    1.63  (* target *)
    1.64  
    1.65 -fun define_overloaded (c, U) v (b_def, rhs) =
    1.66 -  Local_Theory.background_theory_result (Axclass.declare_overloaded (c, U)
    1.67 -  ##>> Axclass.define_overloaded b_def (c, rhs))
    1.68 -  ##> (map_instantiation o apsnd) (filter_out (fn (_, (v', _)) => v' = v))
    1.69 -  ##> Local_Theory.map_contexts (K synchronize_inst_syntax);
    1.70 +fun define_overloaded (c, U) b (b_def, rhs) lthy =
    1.71 +  let
    1.72 +    val name = Binding.name_of b;
    1.73 +    val pos = Binding.pos_of b;
    1.74 +    val _ =
    1.75 +      if Context_Position.is_reported lthy pos then
    1.76 +        Position.report_text pos Markup.class_parameter
    1.77 +          (Pretty.string_of
    1.78 +            (Pretty.block [Pretty.keyword1 "class", Pretty.brk 1,
    1.79 +                Pretty.str "parameter", Pretty.brk 1, pretty_param lthy (c, U)]))
    1.80 +      else ();
    1.81 +  in
    1.82 +    lthy |> Local_Theory.background_theory_result
    1.83 +      (Axclass.declare_overloaded (c, U) ##>> Axclass.define_overloaded b_def (c, rhs))
    1.84 +    ||> (map_instantiation o apsnd) (filter_out (fn (_, (v', _)) => v' = name))
    1.85 +    ||> Local_Theory.map_contexts (K synchronize_inst_syntax)
    1.86 +  end;
    1.87  
    1.88  fun foundation (((b, U), mx), (b_def, rhs)) params lthy =
    1.89    (case instantiation_param lthy b of
    1.90      SOME c =>
    1.91 -      if Mixfix.is_empty mx then lthy |> define_overloaded (c, U) (Binding.name_of b) (b_def, rhs)
    1.92 +      if Mixfix.is_empty mx then lthy |> define_overloaded (c, U) b (b_def, rhs)
    1.93        else error ("Illegal mixfix syntax for overloaded constant " ^ quote c)
    1.94    | NONE => lthy |> Generic_Target.theory_target_foundation (((b, U), mx), (b_def, rhs)) params);
    1.95  
     2.1 --- a/src/Pure/PIDE/markup.ML	Wed Jun 22 11:10:18 2016 +0200
     2.2 +++ b/src/Pure/PIDE/markup.ML	Wed Jun 22 16:04:03 2016 +0200
     2.3 @@ -103,6 +103,7 @@
     2.4    val token_rangeN: string val token_range: T
     2.5    val sortingN: string val sorting: T
     2.6    val typingN: string val typing: T
     2.7 +  val class_parameterN: string val class_parameter: T
     2.8    val ML_keyword1N: string val ML_keyword1: T
     2.9    val ML_keyword2N: string val ML_keyword2: T
    2.10    val ML_keyword3N: string val ML_keyword3: T
    2.11 @@ -468,6 +469,7 @@
    2.12  
    2.13  val (sortingN, sorting) = markup_elem "sorting";
    2.14  val (typingN, typing) = markup_elem "typing";
    2.15 +val (class_parameterN, class_parameter) = markup_elem "class_parameter";
    2.16  
    2.17  
    2.18  (* ML *)
     3.1 --- a/src/Pure/PIDE/markup.scala	Wed Jun 22 11:10:18 2016 +0200
     3.2 +++ b/src/Pure/PIDE/markup.scala	Wed Jun 22 16:04:03 2016 +0200
     3.3 @@ -267,6 +267,7 @@
     3.4  
     3.5    val SORTING = "sorting"
     3.6    val TYPING = "typing"
     3.7 +  val CLASS_PARAMETER = "class_parameter"
     3.8  
     3.9    val ATTRIBUTE = "attribute"
    3.10    val METHOD = "method"
     4.1 --- a/src/Tools/jEdit/etc/options	Wed Jun 22 11:10:18 2016 +0200
     4.2 +++ b/src/Tools/jEdit/etc/options	Wed Jun 22 16:04:03 2016 +0200
     4.3 @@ -133,6 +133,7 @@
     4.4  option inner_cartouche_color : string = "CC6600FF"
     4.5  option inner_comment_color : string = "CC0000FF"
     4.6  option dynamic_color : string = "7BA428FF"
     4.7 +option class_parameter_color : string = "D2691EFF"
     4.8  
     4.9  option markdown_item_color1 : string = "DAFEDAFF"
    4.10  option markdown_item_color2 : string = "FFF0CCFF"
     5.1 --- a/src/Tools/jEdit/src/rendering.scala	Wed Jun 22 11:10:18 2016 +0200
     5.2 +++ b/src/Tools/jEdit/src/rendering.scala	Wed Jun 22 16:04:03 2016 +0200
     5.3 @@ -156,7 +156,7 @@
     5.4    private val highlight_elements =
     5.5      Markup.Elements(Markup.EXPRESSION, Markup.CITATION, Markup.LANGUAGE, Markup.ML_TYPING,
     5.6        Markup.TOKEN_RANGE, Markup.ENTITY, Markup.PATH, Markup.DOC, Markup.URL, Markup.SORTING,
     5.7 -      Markup.TYPING, Markup.FREE, Markup.SKOLEM, Markup.BOUND,
     5.8 +      Markup.TYPING, Markup.CLASS_PARAMETER, Markup.FREE, Markup.SKOLEM, Markup.BOUND,
     5.9        Markup.VAR, Markup.TFREE, Markup.TVAR, Markup.ML_BREAKPOINT,
    5.10        Markup.MARKDOWN_PARAGRAPH, Markup.Markdown_List.name)
    5.11  
    5.12 @@ -185,9 +185,9 @@
    5.13  
    5.14    private val tooltip_elements =
    5.15      Markup.Elements(Markup.LANGUAGE, Markup.EXPRESSION, Markup.TIMING, Markup.ENTITY,
    5.16 -      Markup.SORTING, Markup.TYPING, Markup.ML_TYPING, Markup.ML_BREAKPOINT, Markup.PATH,
    5.17 -      Markup.DOC, Markup.URL, Markup.MARKDOWN_PARAGRAPH, Markup.Markdown_List.name) ++
    5.18 -    Markup.Elements(tooltip_descriptions.keySet)
    5.19 +      Markup.SORTING, Markup.TYPING, Markup.CLASS_PARAMETER, Markup.ML_TYPING,
    5.20 +      Markup.ML_BREAKPOINT, Markup.PATH, Markup.DOC, Markup.URL, Markup.MARKDOWN_PARAGRAPH,
    5.21 +      Markup.Markdown_List.name) ++ Markup.Elements(tooltip_descriptions.keySet)
    5.22  
    5.23    private val gutter_elements =
    5.24      Markup.Elements(Markup.WRITELN, Markup.INFORMATION, Markup.WARNING, Markup.LEGACY, Markup.ERROR)
    5.25 @@ -287,6 +287,7 @@
    5.26    val inner_cartouche_color = color_value("inner_cartouche_color")
    5.27    val inner_comment_color = color_value("inner_comment_color")
    5.28    val dynamic_color = color_value("dynamic_color")
    5.29 +  val class_parameter_color = color_value("class_parameter_color")
    5.30  
    5.31    val markdown_item_color1 = color_value("markdown_item_color1")
    5.32    val markdown_item_color2 = color_value("markdown_item_color2")
    5.33 @@ -635,6 +636,9 @@
    5.34            if name == Markup.SORTING || name == Markup.TYPING =>
    5.35              Some(add(prev, r, (true, pretty_typing("::", body))))
    5.36  
    5.37 +          case (prev, Text.Info(r, XML.Elem(Markup(Markup.CLASS_PARAMETER, _), body))) =>
    5.38 +            Some(add(prev, r, (true, Pretty.block(0, body))))
    5.39 +
    5.40            case (prev, Text.Info(r, XML.Elem(Markup(Markup.ML_TYPING, _), body))) =>
    5.41              Some(add(prev, r, (false, pretty_typing("ML:", body))))
    5.42  
    5.43 @@ -867,6 +871,7 @@
    5.44        Markup.INNER_CARTOUCHE -> inner_cartouche_color,
    5.45        Markup.INNER_COMMENT -> inner_comment_color,
    5.46        Markup.DYNAMIC_FACT -> dynamic_color,
    5.47 +      Markup.CLASS_PARAMETER -> class_parameter_color,
    5.48        Markup.ANTIQUOTE -> antiquote_color,
    5.49        Markup.ML_KEYWORD1 -> keyword1_color,
    5.50        Markup.ML_KEYWORD2 -> keyword2_color,