--- 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);
--- 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 *)
--- 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"
--- 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"
--- 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,