forked from Isabelle_DOF/Isabelle_DOF
Added slightly better popup explanation for document classes.
This commit is contained in:
parent
7bca4e8954
commit
7305efc159
16
Isa_DOF.thy
16
Isa_DOF.thy
|
@ -27,19 +27,23 @@ op #>;
|
||||||
op |>> : ('a * 'c) * ('a -> 'b) -> 'b * 'c;
|
op |>> : ('a * 'c) * ('a -> 'b) -> 'b * 'c;
|
||||||
op ||> : ('c * 'a) * ('a -> 'b) -> 'c * 'b;
|
op ||> : ('c * 'a) * ('a -> 'b) -> 'c * 'b;
|
||||||
|
|
||||||
val docrefN = "docref";
|
val docrefN = "docref";
|
||||||
|
val docclassN = "doc_class";
|
||||||
|
|
||||||
(* derived from: theory_markup *)
|
(* derived from: theory_markup *)
|
||||||
fun docref_markup def name id pos =
|
fun docref_markup_gen refN def name id pos =
|
||||||
if id = 0 then Markup.empty
|
if id = 0 then Markup.empty
|
||||||
else
|
else
|
||||||
Markup.properties (Position.entity_properties_of def id pos)
|
Markup.properties (Position.entity_properties_of def id pos)
|
||||||
(Markup.entity docrefN name); (* or better store the thy-name as property ? ? ? *)
|
(Markup.entity refN name); (* or better store the thy-name as property ? ? ? *)
|
||||||
|
|
||||||
|
val docref_markup = docref_markup_gen docrefN
|
||||||
|
|
||||||
|
val docclass_markup = docref_markup_gen docclassN
|
||||||
|
|
||||||
*}
|
*}
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
ML{*
|
ML{*
|
||||||
|
|
||||||
structure DOF_core =
|
structure DOF_core =
|
||||||
|
@ -203,7 +207,7 @@ fun define_doc_class_global (params', binding) parent fields thy =
|
||||||
else ()
|
else ()
|
||||||
val cid_long = name2doc_class_name thy cid
|
val cid_long = name2doc_class_name thy cid
|
||||||
val id = serial ();
|
val id = serial ();
|
||||||
val _ = Position.report pos (docref_markup true cid id pos);
|
val _ = Position.report pos (docclass_markup true cid id pos);
|
||||||
|
|
||||||
val info = {params=params',
|
val info = {params=params',
|
||||||
name = binding,
|
name = binding,
|
||||||
|
@ -345,7 +349,7 @@ Context_Position.report_generic;
|
||||||
*)
|
*)
|
||||||
val {id, name=bind_target,...} =
|
val {id, name=bind_target,...} =
|
||||||
the(DOF_core.get_doc_class_global cid_long thy)
|
the(DOF_core.get_doc_class_global cid_long thy)
|
||||||
val markup = docref_markup false cid id (Binding.pos_of bind_target);
|
val markup = docclass_markup false cid id (Binding.pos_of bind_target);
|
||||||
val ctxt = Context.Theory thy
|
val ctxt = Context.Theory thy
|
||||||
val _ = Context_Position.report_generic ctxt pos' markup;
|
val _ = Context_Position.report_generic ctxt pos' markup;
|
||||||
|
|
||||||
|
|
Reference in New Issue