forked from Isabelle_DOF/Isabelle_DOF
- restructuring in IsaDOF :
factoring out create_and_check_docitem - correction IsaDofApplication side_by_side figure commented in and works. - reaactivated open_monitor. - changing types of monitor traces : simpler calculation now, but more obscure type - first simulation of monitor trace construction.
This commit is contained in:
parent
0914a1fc5c
commit
86e145f723
73
Isa_DOF.thy
73
Isa_DOF.thy
|
|
@ -442,7 +442,7 @@ type meta_args_t = (((string * Position.T) *
|
|||
(string * Position.T) option)
|
||||
* ((string * Position.T) * string) list)
|
||||
|
||||
fun meta_args_2_string thy (((lab, _), cid_opt), attr_list) =
|
||||
fun meta_args_2_string thy ((((lab, _), cid_opt), attr_list) : meta_args_t) =
|
||||
(* for the moment naive, i.e. without textual normalization of
|
||||
attribute names and adapted term printing *)
|
||||
let val l = "label = "^ (enclose "{" "}" lab)
|
||||
|
|
@ -526,10 +526,8 @@ fun calc_update_term thy cid_long (S:(string * Position.T * string * term)list)
|
|||
val generalize_term = Term.map_types (generalize_typ 0)
|
||||
fun toString t = Syntax.string_of_term (Proof_Context.init_global thy) t
|
||||
fun instantiate_term S t = Term_Subst.map_types_same (Term_Subst.instantiateT S) (t)
|
||||
val _ = (SPY5:=thy)
|
||||
fun read_assn (lhs, _:Position.T, opr, rhs) term =
|
||||
let val _ = (SPY6:=lhs)
|
||||
val info_opt = DOF_core.get_attribute_info cid_long
|
||||
let val info_opt = DOF_core.get_attribute_info cid_long
|
||||
(Long_Name.base_name lhs) thy
|
||||
val (ln,lnt,lnu,lnut) = case info_opt of
|
||||
NONE => error ("unknown attribute >"
|
||||
|
|
@ -572,42 +570,48 @@ fun calc_update_term thy cid_long (S:(string * Position.T * string * term)list)
|
|||
end
|
||||
in Sign.certify_term thy (fold read_assn S term) end
|
||||
|
||||
|
||||
|
||||
fun create_and_check_docitem oid pos cid_pos doc_attrs thy =
|
||||
let val id = serial ();
|
||||
val _ = Position.report pos (docref_markup true oid id pos);
|
||||
(* creates a markup label for this position and reports it to the PIDE framework;
|
||||
this label is used as jump-target for point-and-click feature. *)
|
||||
val cid_long = check_classref cid_pos thy
|
||||
val defaults_init = base_default_term cid_long thy
|
||||
fun conv (na, _(*ty*), term) = (Binding.name_of na, Binding.pos_of na, "=", term);
|
||||
val S = map conv (DOF_core.get_attribute_defaults cid_long thy);
|
||||
val (defaults, _(*ty*), _) = calc_update_term thy cid_long S defaults_init;
|
||||
fun markup2string x = XML.content_of (YXML.parse_body x)
|
||||
fun conv_attrs ((lhs, pos), rhs) = (markup2string lhs,pos,"=", Syntax.read_term_global thy rhs)
|
||||
val assns' = map conv_attrs doc_attrs
|
||||
val (value_term, _(*ty*), _) = calc_update_term thy cid_long assns' defaults
|
||||
in thy |> DOF_core.define_object_global (oid, {pos = pos,
|
||||
thy_name = Context.theory_name thy,
|
||||
value = value_term,
|
||||
id = id,
|
||||
cid = cid_long})
|
||||
end
|
||||
|
||||
|
||||
fun enriched_document_command markdown (((((oid,pos),cid_pos), doc_attrs) : meta_args_t,
|
||||
xstring_opt:(xstring * Position.T) option),
|
||||
toks:Input.source)
|
||||
: Toplevel.transition -> Toplevel.transition =
|
||||
let
|
||||
val id = serial ();
|
||||
val _ = Position.report pos (docref_markup true oid id pos);
|
||||
(* creates a markup label for this position and reports it to the PIDE framework;
|
||||
this label is used as jump-target for point-and-click feature. *)
|
||||
fun enrich_trans thy =
|
||||
let val cid_long = check_classref cid_pos thy
|
||||
val defaults_init = base_default_term cid_long thy
|
||||
fun conv (na, _(*ty*), term) = (Binding.name_of na, Binding.pos_of na, "=", term);
|
||||
val S = map conv (DOF_core.get_attribute_defaults cid_long thy);
|
||||
val (defaults, _(*ty*), _) = calc_update_term thy cid_long S defaults_init;
|
||||
fun markup2string x = XML.content_of (YXML.parse_body x)
|
||||
fun conv_attrs ((lhs, pos), rhs) = (markup2string lhs,pos,"=", Syntax.read_term_global thy rhs)
|
||||
val assns' = map conv_attrs doc_attrs
|
||||
(* NEW : *)
|
||||
val (value_term, _(*ty*), _) = calc_update_term thy cid_long assns' defaults
|
||||
(* OLD :
|
||||
val value_term = (fold convert assns defaults) |> (infer_type thy) *)
|
||||
in thy |> DOF_core.define_object_global (oid, {pos = pos,
|
||||
thy_name = Context.theory_name thy,
|
||||
value = value_term,
|
||||
id = id,
|
||||
cid = cid_long})
|
||||
end
|
||||
|
||||
fun check_text thy = (Thy_Output.output_text(Toplevel.theory_toplevel thy) markdown toks; thy)
|
||||
(* as side-effect, generates markup *)
|
||||
in
|
||||
Toplevel.theory(enrich_trans #> check_text)
|
||||
Toplevel.theory(create_and_check_docitem oid pos cid_pos doc_attrs #> check_text)
|
||||
(* Thanks Frederic Tuong! ! ! *)
|
||||
end;
|
||||
|
||||
|
||||
fun open_monitor_command ((((oid,pos),cid_pos), doc_attrs) : meta_args_t) =
|
||||
Toplevel.theory(create_and_check_docitem oid pos cid_pos doc_attrs)
|
||||
|
||||
|
||||
fun update_instance_command (((oid:string,pos),cid_pos),
|
||||
doc_attrs: (((string*Position.T)*string)*string)list)
|
||||
: Toplevel.transition -> Toplevel.transition =
|
||||
|
|
@ -693,12 +697,17 @@ val _ =
|
|||
"declare document reference"
|
||||
(attributes >> (fn (((oid,pos),cid),doc_attrs) =>
|
||||
(Toplevel.theory (DOF_core.declare_object_global oid))));
|
||||
|
||||
(*
|
||||
val _ =
|
||||
Outer_Syntax.command @{command_keyword "open_monitor*"}
|
||||
"open a document reference monitor"
|
||||
(attributes >> (fn (((oid,pos),cid),doc_attrs) =>
|
||||
(Toplevel.theory (DOF_core.declare_object_global oid))));
|
||||
*)
|
||||
val _ =
|
||||
Outer_Syntax.command @{command_keyword "open_monitor*"}
|
||||
"open a document reference monitor"
|
||||
(attributes >> open_monitor_command);
|
||||
|
||||
val _ =
|
||||
Outer_Syntax.command @{command_keyword "close_monitor*"}
|
||||
|
|
@ -1032,7 +1041,11 @@ doc_class side_by_side_figure = figure +
|
|||
anchor2 :: "string"
|
||||
caption2 :: "string"
|
||||
|
||||
(* dito the future monitor: figure - block *)
|
||||
doc_class figure_group =
|
||||
trace :: "doc_class rexp list" <= "[]"
|
||||
anchor :: "string"
|
||||
caption :: "string"
|
||||
where "\<lbrace>figure\<rbrace>\<^sup>+"
|
||||
|
||||
(* dito the future table *)
|
||||
|
||||
|
|
|
|||
Binary file not shown.
|
|
@ -605,9 +605,9 @@ Clicking on a document class identifier permits to hyperlink into the correspond
|
|||
class definition (\autoref{fig:Dogfood-IV-jumpInDocCLass}); hovering over an attribute-definition
|
||||
(which is qualified in order to disambiguate; \autoref{fig:Dogfood-V-attribute}).
|
||||
\<close>
|
||||
(*
|
||||
side_by_s ide_figure*["text-elements"::side_by_side_figure,
|
||||
side_by_side_figure.anchor="''fig-Dogfood-II-bgnd1''"
|
||||
|
||||
side_by_side_figure*["text-elements"::side_by_side_figure,
|
||||
anchor="''fig-Dogfood-II-bgnd1''"
|
||||
,caption="''Exploring a Reference of a Text-Element.''"
|
||||
,relative_width="''48''"
|
||||
,src="''figures/Dogfood-II-bgnd1''"
|
||||
|
|
@ -625,8 +625,8 @@ side_by_side_figure*["hyperlinks"::side_by_side_figure,anchor="''fig:Dogfood-IV-
|
|||
,caption2="''Exploring an attribute.''"
|
||||
,relative_width2="''47''"
|
||||
,src2="''figures/Dogfood-III-bgnd-text_section''"
|
||||
]\<open> Hyperlinks. \<close>
|
||||
*)
|
||||
]\<open> Hyperlinks.\<close>
|
||||
|
||||
|
||||
|
||||
declare_reference*["figDogfoodVIlinkappl"::figure]
|
||||
|
|
@ -675,7 +675,7 @@ This example shows that ontological modeling is indeed adequate for large techni
|
|||
collaboratively developed documentations, where modifications can lead easily to incoherence.
|
||||
The current checks help to systematically avoid this type of incoherence between formal and
|
||||
informal parts. \<close>
|
||||
(*
|
||||
|
||||
section*[onto_future::technical]\<open> Monitor Classes \<close>
|
||||
text\<open> Besides sub-typing, there is another relation between
|
||||
document classes: a class can be a \emph{monitor} to other ones,
|
||||
|
|
@ -699,7 +699,7 @@ classes and imposing different sets of structural constraints in a
|
|||
Classes which are neither directly nor indirectly (via inheritance) mentioned in the
|
||||
monitor are \emph{independent} from a monitor; instances of independent test elements
|
||||
may occur freely. \<close>
|
||||
*)
|
||||
|
||||
|
||||
section*[conclusion::conclusion]\<open> Conclusion and Related Work\<close>
|
||||
text\<open> We have demonstrated the use of \isadof, a novel ontology modeling and enforcement
|
||||
|
|
|
|||
|
|
@ -85,7 +85,7 @@ ML\<open> HOLogic.dest_number @{docitem_attr a2::omega} \<close>
|
|||
update_instance*[omega::E, x+="''inition''"]
|
||||
|
||||
ML\<open> val s = HOLogic.dest_string ( @{docitem_attr x::omega}) \<close>
|
||||
|
||||
|
||||
update_instance*[omega::E, y+="[''defini'',''tion'']"]
|
||||
|
||||
update_instance*[omega::E, y+="[''en'']"]
|
||||
|
|
@ -93,4 +93,28 @@ update_instance*[omega::E, y+="[''en'']"]
|
|||
ML\<open>val s = map HOLogic.dest_string (HOLogic.dest_list @{docitem_attr y::omega});
|
||||
\<close>
|
||||
|
||||
|
||||
section\<open>Simulation of a Monitor\<close>
|
||||
|
||||
open_monitor*[fig1::figure_group,
|
||||
anchor="''fig-demo''",
|
||||
caption="''Sample ''"]
|
||||
|
||||
|
||||
figure*[fig_A::figure, spawn_columns=False,relative_width="''90''",
|
||||
src="''figures/A.png''"]
|
||||
\<open> The A train \ldots \<close>
|
||||
update_instance*[fig1::figure_group, trace+="[figure]"]
|
||||
|
||||
|
||||
figure*[fig_B::figure, spawn_columns=False,relative_width="''90''",
|
||||
src="''figures/B.png''"]
|
||||
\<open> The B train \ldots \<close>
|
||||
update_instance*[fig1::figure_group, trace+="[figure]"]
|
||||
|
||||
close_monitor*[fig1]
|
||||
|
||||
ML\<open> (HOLogic.dest_list @{docitem_attr trace::fig1}) \<close>
|
||||
|
||||
|
||||
end
|
||||
Loading…
Reference in New Issue