Update Manual and code
ci/woodpecker/push/build Pipeline was successful
Details
ci/woodpecker/push/build Pipeline was successful
Details
- Update term context section - Add option to define a default class for declare_reference* - Use defined symbol identifiers \<quote> and \<doublequote> to simplify caveat section about lexical conventions - Rename Manual theories to avoid issues when using Syntax.parse_term that is not compatible with with long-names staring with a number or an underscore - Rewrite names used as mixfix annotation for the term-antiquotations to rule out mixform form excluded symbols
This commit is contained in:
Nicolas Méric
parent
0834f938a9
commit
230247de1a
|
|
@ -94,6 +94,17 @@ definition*[a2::A, x=5, level="Some 1"] xx' where "xx' \<equiv> A.x @{A \<open>a
|
|||
|
||||
lemma*[e5::E] testtest : "xx + A.x @{A \<open>a1\<close>} = yy + A.x @{A \<open>a1\<close>} \<Longrightarrow> xx = yy" by simp
|
||||
|
||||
doc_class cc_assumption_test =
|
||||
a :: int
|
||||
text*[cc_assumption_test_ref::cc_assumption_test]\<open>\<close>
|
||||
|
||||
definition tag_l :: "'a \<Rightarrow> 'b \<Rightarrow> 'b" where "tag_l \<equiv> \<lambda>x y. y"
|
||||
|
||||
lemma* tagged : "tag_l @{cc-assumption-test \<open>cc_assumption_test_ref\<close>} AA \<Longrightarrow> AA"
|
||||
by (simp add: tag_l_def)
|
||||
|
||||
find_theorems name:tagged "(_::cc_assumption_test \<Rightarrow> _ \<Rightarrow> _) _ _ \<Longrightarrow>_"
|
||||
|
||||
declare_reference-assert-error[c1::C]\<open>Duplicate instance declaration\<close> \<comment> \<open>forward declaration\<close>
|
||||
|
||||
declare_reference*[e6::E]
|
||||
|
|
|
|||
|
|
@ -16,12 +16,12 @@ session "Isabelle_DOF" (AFP) = "Functional-Automata" +
|
|||
"thys/Isa_DOF"
|
||||
"thys/Isa_COL"
|
||||
theories [document = true]
|
||||
"thys/manual/01_Introduction"
|
||||
"thys/manual/00_Frontmatter"
|
||||
"thys/manual/02_Background"
|
||||
"thys/manual/05_Implementation"
|
||||
"thys/manual/03_GuidedTour"
|
||||
"thys/manual/04_RefMan"
|
||||
"thys/manual/M_00_Frontmatter"
|
||||
"thys/manual/M_01_Introduction"
|
||||
"thys/manual/M_02_Background"
|
||||
"thys/manual/M_03_GuidedTour"
|
||||
"thys/manual/M_04_RefMan"
|
||||
"thys/manual/M_05_Implementation"
|
||||
"thys/manual/Isabelle_DOF-Manual"
|
||||
document_files
|
||||
"root.bib"
|
||||
|
|
|
|||
|
|
@ -1,7 +1,7 @@
|
|||
\input{00_Frontmatter.tex}
|
||||
\input{01_Introduction.tex}
|
||||
\input{02_Background.tex}
|
||||
\input{03_GuidedTour.tex}
|
||||
\input{04_RefMan.tex}
|
||||
\input{05_Implementation.tex}
|
||||
\input{M_00_Frontmatter.tex}
|
||||
\input{M_01_Introduction.tex}
|
||||
\input{M_02_Background.tex}
|
||||
\input{M_03_GuidedTour.tex}
|
||||
\input{M_04_RefMan.tex}
|
||||
\input{M_05_Implementation.tex}
|
||||
\input{Isabelle_DOF-Manual.tex}
|
||||
|
|
|
|||
|
|
@ -168,4 +168,6 @@
|
|||
|
||||
% notation
|
||||
\newcommand{\isactrltermUNDERSCORE}{\isakeywordcontrol{term{\isacharunderscore}}}
|
||||
\newcommand{\isactrlvalueUNDERSCORE}{\isakeywordcontrol{value{\isacharunderscore}}}
|
||||
\newcommand{\isactrlvalueUNDERSCORE}{\isakeywordcontrol{value{\isacharunderscore}}}
|
||||
\newcommand{\isasymdoublequote}{\texttt{\upshape"}}
|
||||
\newcommand{\isasymquote}{\texttt{\upshape'}}
|
||||
|
|
@ -1161,6 +1161,13 @@ fun ML_isa_check_trace_attribute thy (term, _, pos) s =
|
|||
val _ = DOF_core.get_instance_global oid thy
|
||||
in SOME term end
|
||||
|
||||
fun translate f = Symbol.explode #> map f #> implode;
|
||||
|
||||
(* convert excluded mixfix symbols *)
|
||||
val clean_string = translate
|
||||
(fn "_" => "-"
|
||||
| "'" => "-"
|
||||
| c => c);
|
||||
|
||||
fun ML_isa_elaborate_generic (_:theory) isa_name ty term_option _ =
|
||||
case term_option of
|
||||
|
|
@ -1187,9 +1194,7 @@ fun declare_ISA_class_accessor_and_check_instance doc_class_name =
|
|||
(* Unfortunately due to different lexical conventions for constant symbols and mixfix symbols
|
||||
we can not use "_" for classes names in term antiquotation.
|
||||
We chose to convert "_" to "-".*)
|
||||
val conv_class_name = String.translate (fn #"_" => "-"
|
||||
| x => String.implode [x] )
|
||||
(Binding.name_of doc_class_name)
|
||||
val conv_class_name = clean_string (Binding.name_of doc_class_name)
|
||||
val mixfix_string = "@{" ^ conv_class_name ^ " _}"
|
||||
in
|
||||
Sign.add_consts_cmd [(bind, typestring, Mixfix.mixfix(mixfix_string))]
|
||||
|
|
@ -1225,8 +1230,7 @@ fun declare_class_instances_annotation thy doc_class_name =
|
|||
(* Unfortunately due to different lexical conventions for constant symbols and mixfix symbols
|
||||
we can not use "_" for classes names in term antiquotation.
|
||||
We chose to convert "_" to "-".*)
|
||||
val conv_class_name' = String.translate (fn #"_" => "-" | x=> String.implode [x])
|
||||
((Binding.name_of doc_class_name) ^ instances_of_suffixN)
|
||||
val conv_class_name' = clean_string ((Binding.name_of doc_class_name) ^ instances_of_suffixN)
|
||||
val mixfix_string = "@{" ^ conv_class_name' ^ "}"
|
||||
in
|
||||
Sign.add_consts [(bind, class_list_typ, Mixfix.mixfix(mixfix_string))]
|
||||
|
|
@ -1716,7 +1720,7 @@ fun register_oid_cid_in_open_monitors oid pos cid_pos thy =
|
|||
let val cid_long =
|
||||
let val DOF_core.Instance cid = DOF_core.get_instance_global x thy
|
||||
in cid |> #cid end
|
||||
in DOF_core.check_ml_invs cid_long x {is_monitor=false} thy end)
|
||||
in DOF_core.check_ml_invs cid_long x {is_monitor=true} thy end)
|
||||
val delta_autoS = map is_enabled_for_cid enabled_monitors;
|
||||
fun update_info (n, aS, monitor_info) =
|
||||
let val DOF_core.Monitor_Info {accepted_cids,rejected_cids,...} = monitor_info
|
||||
|
|
@ -2195,6 +2199,11 @@ fun gen_enriched_document_cmd {inline} cid_transform attr_transform
|
|||
Value_Command.Docitem_Parser.create_and_check_docitem {is_monitor = false} {is_inline = inline}
|
||||
{define = true} oid pos (cid_transform cid_pos) (attr_transform doc_attrs);
|
||||
|
||||
fun gen_enriched_document_cmd' {inline} cid_transform attr_transform
|
||||
((((oid, pos),cid_pos), doc_attrs) : ODL_Meta_Args_Parser.meta_args_t) : theory -> theory =
|
||||
Value_Command.Docitem_Parser.create_and_check_docitem {is_monitor = false} {is_inline = inline}
|
||||
{define = false} oid pos (cid_transform cid_pos) (attr_transform doc_attrs);
|
||||
|
||||
|
||||
(* markup reports and document output *)
|
||||
|
||||
|
|
@ -2264,16 +2273,32 @@ val _ =
|
|||
(gen_enriched_document_cmd {inline=false} (* declare as macro *) I I);
|
||||
|
||||
|
||||
val (declare_reference_default_class, declare_reference_default_class_setup)
|
||||
= Attrib.config_string \<^binding>\<open>declare_reference_default_class\<close> (K "");
|
||||
|
||||
val _ = Theory.setup declare_reference_default_class_setup
|
||||
|
||||
val _ =
|
||||
let fun create_and_check_docitem (((oid, pos),cid_pos),doc_attrs)
|
||||
= (Value_Command.Docitem_Parser.create_and_check_docitem
|
||||
{is_monitor = false} {is_inline=true}
|
||||
{define = false} oid pos (cid_pos) (doc_attrs))
|
||||
let fun default_cid meta_args thy =
|
||||
let
|
||||
fun default_cid' _ NONE cid_pos = cid_pos
|
||||
| default_cid' thy (SOME ncid) NONE =
|
||||
let val name = DOF_core.get_onto_class_name_global' ncid thy
|
||||
val ns = DOF_core.get_onto_classes (Proof_Context.init_global thy)
|
||||
|> Name_Space.space_of_table
|
||||
val {pos, ...} = Name_Space.the_entry ns name
|
||||
in SOME (name,pos) end
|
||||
| default_cid' _ (SOME _) cid_pos = cid_pos
|
||||
val ncid = Config.get_global thy declare_reference_default_class
|
||||
val ncid' = if ncid = ""
|
||||
then NONE
|
||||
else SOME ncid
|
||||
in gen_enriched_document_cmd' {inline=true} (default_cid' thy ncid') I meta_args thy
|
||||
end
|
||||
in Outer_Syntax.command \<^command_keyword>\<open>declare_reference*\<close>
|
||||
"declare document reference"
|
||||
(ODL_Meta_Args_Parser.attributes
|
||||
>> (Toplevel.theory o create_and_check_docitem))
|
||||
>> (Toplevel.theory o default_cid))
|
||||
end;
|
||||
|
||||
end (* structure Monitor_Command_Parser *)
|
||||
|
|
@ -2753,8 +2778,10 @@ fun check_and_mark ctxt cid_decl ({strict_checking = strict}) {inline=inline_req
|
|||
val {pos=pos', ...} = Name_Space.the_entry ns name'
|
||||
(* this sends a report for a ref application to the PIDE interface ... *)
|
||||
val _ = if not(DOF_core.is_subclass ctxt cid cid_decl)
|
||||
then error("reference ontologically inconsistent: "^cid
|
||||
^" must be subclass of "^cid_decl^ Position.here pos')
|
||||
then error("reference ontologically inconsistent: "
|
||||
^ name ^ " is an instance of " ^ cid
|
||||
^ " and " ^ cid
|
||||
^ " is not a subclass of " ^ cid_decl ^ Position.here pos)
|
||||
else ()
|
||||
in () end
|
||||
|
||||
|
|
@ -2801,15 +2828,14 @@ fun docitem_antiquotation bind cid =
|
|||
|
||||
fun check_and_mark_term ctxt oid =
|
||||
let
|
||||
val thy = Context.theory_of ctxt;
|
||||
val ctxt' = Context.proof_of ctxt
|
||||
val DOF_core.Instance {cid,value,...} =
|
||||
DOF_core.get_instance_global oid thy
|
||||
val thy = Proof_Context.theory_of ctxt';
|
||||
val oid' = DOF_core.get_instance_name_global oid thy
|
||||
val DOF_core.Instance {cid,value,...} = DOF_core.get_instance_global oid' thy
|
||||
val instances = DOF_core.get_instances ctxt'
|
||||
val ns = instances |> Name_Space.space_of_table
|
||||
val {pos, ...} = Name_Space.the_entry ns oid
|
||||
val markup = DOF_core.get_instance_name_global oid thy
|
||||
|> Name_Space.markup (Name_Space.space_of_table instances)
|
||||
val {pos, ...} = Name_Space.the_entry ns oid'
|
||||
val markup = oid' |> Name_Space.markup (Name_Space.space_of_table instances)
|
||||
val _ = Context_Position.report ctxt' pos markup;
|
||||
(* this sends a report for a ref application to the PIDE interface ... *)
|
||||
val _ = if cid = DOF_core.default_cid
|
||||
|
|
|
|||
|
|
@ -13,7 +13,7 @@
|
|||
|
||||
(*<*)
|
||||
theory "Isabelle_DOF-Manual"
|
||||
imports "05_Implementation"
|
||||
imports "M_05_Implementation"
|
||||
begin
|
||||
close_monitor*[this]
|
||||
check_doc_global
|
||||
|
|
|
|||
|
|
@ -12,7 +12,7 @@
|
|||
*************************************************************************)
|
||||
|
||||
(*<*)
|
||||
theory "00_Frontmatter"
|
||||
theory "M_00_Frontmatter"
|
||||
imports
|
||||
"Isabelle_DOF.technical_report"
|
||||
begin
|
||||
|
|
@ -20,8 +20,6 @@ begin
|
|||
use_template "scrreprt-modern"
|
||||
use_ontology "technical_report"
|
||||
|
||||
|
||||
|
||||
section\<open>Local Document Setup.\<close>
|
||||
text\<open>Introducing document specific abbreviations and macros:\<close>
|
||||
|
||||
|
|
@ -12,8 +12,8 @@
|
|||
*************************************************************************)
|
||||
|
||||
(*<*)
|
||||
theory "01_Introduction"
|
||||
imports "00_Frontmatter"
|
||||
theory "M_01_Introduction"
|
||||
imports "M_00_Frontmatter"
|
||||
begin
|
||||
(*>*)
|
||||
|
||||
|
|
@ -12,8 +12,8 @@
|
|||
*************************************************************************)
|
||||
|
||||
(*<*)
|
||||
theory "02_Background"
|
||||
imports "01_Introduction"
|
||||
theory "M_02_Background"
|
||||
imports "M_01_Introduction"
|
||||
begin
|
||||
(*>*)
|
||||
|
||||
|
|
@ -13,9 +13,9 @@
|
|||
|
||||
(*<*)
|
||||
theory
|
||||
"03_GuidedTour"
|
||||
"M_03_GuidedTour"
|
||||
imports
|
||||
"02_Background"
|
||||
"M_02_Background"
|
||||
begin
|
||||
(*>*)
|
||||
|
||||
|
|
@ -176,7 +176,11 @@ By lexical conventions, theory-names must be unique inside a session
|
|||
(and session names must be unique too), such that long-names are unique by construction.
|
||||
There are actually different name categories that form a proper name space, \<^eg>, the name space for
|
||||
constant symbols and type symbols are distinguished.
|
||||
|
||||
Additionally, \<^isadof> objects also come with a proper name space: classes (and monitors), instances,
|
||||
low-level class invariants (SML-defined invariants) all follow the lexical conventions of
|
||||
Isabelle. For instance, a class can be referenced outside of its theory using
|
||||
its short-name or its long-name if another class with the same name is defined
|
||||
in the current theory.
|
||||
Isabelle identifies names already with the shortest suffix that is unique in the global
|
||||
context and in the appropriate name category. This also holds for pretty-printing, which can
|
||||
at times be confusing since names stemming from the same specification construct may
|
||||
|
|
@ -193,19 +197,15 @@ over decades.
|
|||
|
||||
text\<open>At times, this causes idiosyncrasies like the ones cited in the following incomplete list:
|
||||
\<^item> text-antiquotations
|
||||
\<^theory_text>\<open>text\<close>\<^latex>\<open>\isasymopen\textbf{thm} "normally\_behaved\_def"\isasymclose\ \<close>
|
||||
versus \<^theory_text>\<open>text\<close>\<^latex>\<open>\isasymopen @\{\textbf{thm} "srac$_1$\_def"\}\isasymclose\ \<close>
|
||||
(while
|
||||
\<^theory_text>\<open>text\<close>\<^latex>\<open>\isasymopen @\{\textbf{thm} \isasymopen srac$_1$\_def \isasymclose\}\isasymclose\ \<close>
|
||||
fails)
|
||||
\<^theory_text>\<open>text\<open>@{thm \<doublequote>srac\<^sub>1_def\<doublequote>}\<close>\<close>
|
||||
while \<^theory_text>\<open>text\<open>@{thm \<open>srac\<^sub>1_def\<close>}\<close>\<close> fails
|
||||
\<^item> commands \<^theory_text>\<open>thm fundamental_theorem_of_calculus\<close> and
|
||||
\<^theory_text>\<open>thm\<close>\<^latex>\<open> "fundamental\_theorem\_of\_calculus"\<close>
|
||||
or \<^theory_text>\<open>lemma\<close> \<^latex>\<open>"H"\<close> and \<^theory_text>\<open>lemma \<open>H\<close>\<close> and \<^theory_text>\<open>lemma H\<close>
|
||||
\<^item> string expressions \<^theory_text>\<open>term\<close>\<^latex>\<open>\isasymopen ''abc'' @ ''cd''\isasymclose\ \<close> and equivalent
|
||||
\<^theory_text>\<open>term\<close>\<^latex>\<open>\isasymopen \isasymopen abc\isasymclose\ @ \isasymopen cd\isasymclose\isasymclose\<close>;
|
||||
but
|
||||
\<^theory_text>\<open>term\<close>\<^latex>\<open>\isasymopen\isasymopen A \isasymlongrightarrow\ B\isasymclose\isasymclose\ \<close>
|
||||
not equivalent to \<^theory_text>\<open>term\<close>\<^latex>\<open>\isasymopen''A \isasymlongrightarrow\ B''\isasymclose\ \<close>
|
||||
\<^theory_text>\<open>thm \<doublequote>fundamental_theorem_of_calculus\<doublequote>\<close>
|
||||
or \<^theory_text>\<open>lemma \<doublequote>H\<doublequote>\<close> and \<^theory_text>\<open>lemma \<open>H\<close>\<close> and \<^theory_text>\<open>lemma H\<close>
|
||||
\<^item> string expressions
|
||||
\<^theory_text>\<open>term\<open>\<quote>\<quote>abc\<quote>\<quote> @ \<quote>\<quote>cd\<quote>\<quote>\<close>\<close> and equivalent
|
||||
\<^theory_text>\<open>term \<open>\<open>abc\<close> @ \<open>cd\<close>\<close>\<close>;
|
||||
but \<^theory_text>\<open>term\<open>\<open>A \<longrightarrow> B\<close>\<close>\<close> not equivalent to \<^theory_text>\<open>term\<open>\<quote>\<quote>A \<longrightarrow> B\<quote>\<quote>\<close>\<close>
|
||||
which fails.
|
||||
\<close>
|
||||
|
||||
|
|
@ -520,17 +520,20 @@ underlying logical context, which turns the arguments into \<^emph>\<open>formal
|
|||
source, in contrast to the free-form antiquotations which basically influence the presentation.
|
||||
|
||||
We still mention a few of these document antiquotations here:
|
||||
\<^item> \<^theory_text>\<open>@{thm \<open>refl\<close>}\<close> or \<^theory_text>\<open>@{thm [display] \<open>refl\<close>}\<close> check that \<^theory_text>\<open>refl\<close> is indeed a reference
|
||||
\<^item> \<^theory_text>\<open>@{thm \<doublequote>refl\<doublequote>}\<close> or \<^theory_text>\<open>@{thm [display] \<doublequote>refl\<doublequote>}\<close>
|
||||
check that \<^theory_text>\<open>refl\<close> is indeed a reference
|
||||
to a theorem; the additional ``style" argument changes the presentation by printing the
|
||||
formula into the output instead of the reference itself,
|
||||
\<^item> \<^theory_text>\<open>@{lemma \<open>prop\<close> } by \<open>method\<close>\<close> allows deriving \<open>prop\<close> on the fly, thus guarantee
|
||||
that it is a corrollary of the current context,
|
||||
\<^item> \<^theory_text>\<open>@{lemma \<open>prop\<close> by method} \<close> allows deriving \<open>prop\<close> on the fly, thus guarantee
|
||||
that it is a corollary of the current context,
|
||||
\<^item> \<^theory_text>\<open>@{term \<open>term\<close> }\<close> parses and type-checks \<open>term\<close>,
|
||||
\<^item> \<^theory_text>\<open>@{value \<open>term\<close> }\<close> performs the evaluation of \<open>term\<close>,
|
||||
\<^item> \<^theory_text>\<open>@{ML \<open>ml-term\<close> }\<close> parses and type-checks \<open>ml-term\<close>,
|
||||
\<^item> \<^theory_text>\<open>@{ML_file \<open>ml-file\<close> }\<close> parses the path for \<open>ml-file\<close> and
|
||||
verifies its existance in the (Isabelle-virtual) file-system.
|
||||
\<close>
|
||||
|
||||
lemma \<open>x = x\<close> by auto
|
||||
text\<open>There are options to display sub-parts of formulas etc., but it is a consequence
|
||||
of tight-checking that the information must be given complete and exactly in the syntax of
|
||||
Isabelle. This may be over-precise and a burden to readers not familiar with Isabelle, which may
|
||||
|
|
@ -538,14 +541,17 @@ motivate authors to choose the aforementioned freeform-style.
|
|||
|
||||
Additionally, documents antiquotations were added to check and evaluate terms with
|
||||
term antiquotations:
|
||||
\<^item> \<^theory_text>\<open>@{term_ \<open>term\<close> }\<close> parses and type-checks \<open>term\<close> with term antiquotations,
|
||||
for instance \<^theory_text>\<open>\<^term_> \<open>@{technical \<open>isadof\<close>}\<close>\<close> will parse and check
|
||||
that \<open>isadof\<close> is indeed an instance of the class \<^typ>\<open>technical\<close>,
|
||||
\<^item> \<^theory_text>\<open>@{value_ \<open>term\<close> }\<close> performs the evaluation of \<open>term\<close> with term antiquotations,
|
||||
for instance \<^theory_text>\<open>@{value_ \<open>mcc @{cenelec-term \<open>FT\<close>}\<close>}\<close>
|
||||
will print the value of the \<^const>\<open>mcc\<close> attribute of the instance \<open>FT\<close>.
|
||||
for instance \<^theory_text>\<open>@{value_ \<open>definition_list @{technical \<open>isadof\<close>}\<close>}\<close>
|
||||
will print the value of the \<^const>\<open>definition_list\<close> attribute of the instance \<open>isadof\<close>.
|
||||
\<^theory_text>\<open>value_\<close> may have an optional argument between square brackets to specify the evaluator but this
|
||||
argument must be specified after a default optional argument already defined
|
||||
by the text antiquotation implementation.
|
||||
So one must use the following syntax if he does not want to specify the first optional argument:
|
||||
\<open>@{value_ [] [nbe] \<open>r @{F \<open>xcv4\<close>}\<close>}\<close>. Note the empty brackets.
|
||||
\<^theory_text>\<open>@{value_ [] [nbe] \<open>definition_list @{technical \<open>isadof\<close>}\<close>}\<close>. Note the empty brackets.
|
||||
\<close>
|
||||
|
||||
(*<*)
|
||||
|
|
@ -13,9 +13,9 @@
|
|||
|
||||
(*<*)
|
||||
theory
|
||||
"04_RefMan"
|
||||
"M_04_RefMan"
|
||||
imports
|
||||
"03_GuidedTour"
|
||||
"M_03_GuidedTour"
|
||||
begin
|
||||
|
||||
declare_reference*[infrastructure::technical]
|
||||
|
|
@ -310,13 +310,24 @@ text\<open>
|
|||
section\<open>Fundamental Commands of the \<^isadof> Core\<close>
|
||||
text\<open>Besides the core-commands to define an ontology as presented in the previous section,
|
||||
the \<^isadof> core provides a number of mechanisms to \<^emph>\<open>use\<close> the resulting data to annotate
|
||||
text-elements and, in some cases, terms.
|
||||
text-elements and, in some cases, terms.
|
||||
In the following, we formally introduce the syntax of the core commands as
|
||||
supported on the Isabelle/Isar level. Some more advanced functionality of the core
|
||||
is currently only available in the SML API's of the kernel.
|
||||
|
||||
\<close>
|
||||
|
||||
subsection\<open>Syntax\<close>
|
||||
text\<open>In the following, we formally introduce the syntax of the core commands as
|
||||
supported on the Isabelle/Isar level. Some more advanced functionality of the core
|
||||
is currently only available in the SML API's of the kernel.
|
||||
text\<open>
|
||||
|
||||
|
||||
\<close>
|
||||
text\<open>Recall that except \<^theory_text>\<open>text*[]\<open>...\<close>\<close>, all \<^isadof> commands were mapped to visible
|
||||
layout; these commands have to be wrapped into
|
||||
\<^verbatim>\<open>(*<*) ... (*>*)\<close> if this is undesired. \<close>
|
||||
|
||||
subsection\<open>Ontological Text-Contexts and their Management\<close>
|
||||
text\<open>
|
||||
|
||||
\<^item> \<open>obj_id\<close>:\<^index>\<open>obj\_id@\<open>obj_id\<close>\<close> (or \<^emph>\<open>oid\<close>\<^index>\<open>oid!oid@\<open>see obj_id\<close>\<close> for short) a \<^emph>\<open>name\<close>
|
||||
as specified in @{technical \<open>odl-manual0\<close>}.
|
||||
|
|
@ -329,15 +340,10 @@ is currently only available in the SML API's of the kernel.
|
|||
symbolic evaluation using the simplifier, \<open>nbe\<close> for \<^emph>\<open>normalization by
|
||||
evaluation\<close> and \<^emph>\<open>code\<close> for code generation in SML.
|
||||
\<^item> \<open>upd_meta_args\<close> :
|
||||
\<^rail>\<open> (obj_id ('::' class_id) ((',' attribute (':=' | '+=') HOL_term) * ))\<close>
|
||||
\<^rail>\<open> (obj_id ('::' class_id) ((',' attribute (':=' | '+=') HOL_term ) * ))\<close>
|
||||
|
||||
\<^item> \<open>annotated_text_element\<close> :
|
||||
\<^rail>\<open>
|
||||
( @@{command "text*"} '[' meta_args ']' '\<open>' formal_text '\<close>'
|
||||
| @@{command "ML*"} '[' meta_args ']' '\<open>' SML_code '\<close>'
|
||||
| @@{command "term*"} ('[' meta_args ']')? '\<open>' HOL_term '\<close>'
|
||||
| (@@{command "value*"}
|
||||
| @@{command "assert*"}) \<newline> ('[' meta_args ']')? ('[' evaluator ']')? '\<open>' HOL_term '\<close>'
|
||||
)
|
||||
\<^rail>\<open>( @@{command "text*"} '[' meta_args ']' '\<open>' formal_text '\<close>' )
|
||||
\<close>
|
||||
\<^rail>\<open>
|
||||
( @@{command "open_monitor*"}
|
||||
|
|
@ -350,21 +356,10 @@ is currently only available in the SML API's of the kernel.
|
|||
\<close>
|
||||
\<^item> \<^isadof> \<open>change_status_command\<close> :
|
||||
\<^rail>\<open> (@@{command "update_instance*"} '[' upd_meta_args ']')\<close>
|
||||
\<^item> \<^isadof> \<open>inspection_command\<close> :
|
||||
\<^rail>\<open> @@{command "print_doc_classes"}
|
||||
| @@{command "print_doc_items"}
|
||||
| @@{command "check_doc_global"}\<close>
|
||||
\<^item> \<^isadof> \<open>macro_command\<close> :
|
||||
\<^rail>\<open> @@{command "define_shortcut*"} name ('\<rightleftharpoons>' | '==') '\<open>' string '\<close>'
|
||||
| @@{command "define_macro*"} name ('\<rightleftharpoons>' | '==')
|
||||
\<newline> '\<open>' string '\<close>' '_' '\<open>' string '\<close>' \<close>
|
||||
\<close>
|
||||
text\<open>Recall that except \<^theory_text>\<open>text*[]\<open>...\<close>\<close>, all \<^isadof> commands were mapped to visible
|
||||
layout; these commands have to be wrapped into
|
||||
\<^verbatim>\<open>(*<*) ... (*>*)\<close> if this is undesired. \<close>
|
||||
|
||||
subsection\<open>Ontological Text-Contexts and their Management\<close>
|
||||
text\<open> With respect to the family of text elements,
|
||||
|
||||
|
||||
With respect to the family of text elements,
|
||||
\<^theory_text>\<open>text*[oid::cid, ...] \<open> \<dots> text \<dots> \<close> \<close> is the core-command of \<^isadof>: it permits to create
|
||||
an object of meta-data belonging to the class \<^theory_text>\<open>cid\<close>\<^index>\<open>cid!cid@\<open>see class_id\<close>\<close>.
|
||||
This is viewed as the \<^emph>\<open>definition\<close> of an instance of a document class.
|
||||
|
|
@ -391,11 +386,22 @@ For a declared class \<^theory_text>\<open>cid\<close>, there exists a text anti
|
|||
The precise presentation is decided in the \<^emph>\<open>layout definitions\<close>, for example by suitable
|
||||
\<^LaTeX>-template code. Declared but not yet defined instances must be referenced with a particular
|
||||
pragma in order to enforce a relaxed checking \<^theory_text>\<open> @{cid (unchecked) \<open>oid\<close>} \<close>.
|
||||
The choice of the default class in a @{command "declare_reference*"}-command
|
||||
can be influenced by setting globally an attribute:
|
||||
@{boxed_theory_text [display]
|
||||
\<open>declare[[declare_reference_default_class = "definition"]]\<close>}
|
||||
Then in this example:
|
||||
@{boxed_theory_text [display]\<open>declare_reference*[def1]\<close>}
|
||||
\<open>def1\<close> will be a declared instance of the class \<open>definition\<close>.
|
||||
\<close>
|
||||
|
||||
subsection\<open>Ontological Code-Contexts and their Management\<close>
|
||||
|
||||
text\<open>The \<^theory_text>\<open>ML*[oid::cid, ...] \<open> \<dots> SML-code \<dots> \<close>\<close>-document elements proceed similarly:
|
||||
text\<open>
|
||||
\<^item> \<open>annotated_code_element\<close>:
|
||||
\<^rail>\<open>(@@{command "ML*"} '[' meta_args ']' '\<open>' SML_code '\<close>')\<close>
|
||||
|
||||
The \<^theory_text>\<open>ML*[oid::cid, ...] \<open> \<dots> SML-code \<dots> \<close>\<close>-document elements proceed similarly:
|
||||
a referentiable meta-object of class \<^theory_text>\<open>cid\<close> is created, initialized with the optional
|
||||
attributes and bound to \<^theory_text>\<open>oid\<close>. In fact, the entire the meta-argument list is optional.
|
||||
The SML-code is type-checked and executed
|
||||
|
|
@ -403,39 +409,139 @@ in the context of the SML toplevel of the Isabelle system as in the correspondin
|
|||
\<^theory_text>\<open>ML\<open> \<dots> SML-code \<dots> \<close>\<close>-command.
|
||||
Additionally, ML antiquotations were added to check and evaluate terms with
|
||||
term antiquotations:
|
||||
\<^item> \<^theory_text>\<open>@{term_ \<open>term\<close> }\<close> parses and type-checks \<open>term\<close> with term antiquotations,
|
||||
for instance \<^theory_text>\<open>@{term_ \<open>@{technical \<open>odl-manual1\<close>}\<close>}\<close> will parse and check
|
||||
that \<open>odl-manual1\<close> is indeed an instance of the class \<^typ>\<open>technical\<close>,
|
||||
\<^item> \<^theory_text>\<open>@{value_ \<open>term\<close> }\<close> performs the evaluation of \<open>term\<close> with term antiquotations,
|
||||
for instance \<^theory_text>\<open>@{value_ \<open>mcc @{cenelec-term \<open>FT\<close>}\<close>}\<close>
|
||||
will print the value of the \<^const>\<open>mcc\<close> attribute of the instance \<open>FT\<close>.
|
||||
for instance \<^theory_text>\<open>@{value_ \<open>definition_list @{technical \<open>odl-manual1\<close>}\<close>}\<close>
|
||||
will get the value of the \<^const>\<open>definition_list\<close> attribute of the instance \<open>odl-manual1\<close>.
|
||||
\<^theory_text>\<open>value_\<close> may have an optional argument between square brackets to specify the evaluator:
|
||||
\<open>@{value_ [nbe] \<open>mcc @{cenelec-term \<open>FT\<close>}\<close>}\<close> forces \<open>value_\<close> to evaluate
|
||||
\<^theory_text>\<open>@{value_ [nbe] \<open>definition_list @{technical \<open>odl-manual1\<close>}\<close>}\<close> forces \<open>value_\<close> to evaluate
|
||||
the term using normalization by evaluation (see @{cite "wenzel:isabelle-isar:2020"}).
|
||||
\<close>
|
||||
|
||||
(*<*)
|
||||
doc_class A =
|
||||
level :: "int option"
|
||||
x :: int
|
||||
definition*[a1::A, x=5, level="Some 1"] xx' where "xx' \<equiv> A.x @{A \<open>a1\<close>}" if "A.x @{A \<open>a1\<close>} = 5"
|
||||
|
||||
doc_class E =
|
||||
x :: "string" <= "''qed''"
|
||||
|
||||
doc_class cc_assumption_test =
|
||||
a :: int
|
||||
text*[cc_assumption_test_ref::cc_assumption_test]\<open>\<close>
|
||||
|
||||
definition tag_l :: "'a \<Rightarrow> 'b \<Rightarrow> 'b" where "tag_l \<equiv> \<lambda>x y. y"
|
||||
|
||||
lemma* tagged : "tag_l @{cc-assumption-test \<open>cc_assumption_test_ref\<close>} AA \<Longrightarrow> AA"
|
||||
by (simp add: tag_l_def)
|
||||
|
||||
find_theorems name:tagged "(_::cc_assumption_test \<Rightarrow> _ \<Rightarrow> _) _ _ \<Longrightarrow>_"
|
||||
|
||||
lemma*[e5::E] testtest : "xx + A.x @{A \<open>a1\<close>} = yy + A.x @{A \<open>a1\<close>} \<Longrightarrow> xx = yy" by simp
|
||||
|
||||
doc_class B'_test' =
|
||||
b::int
|
||||
|
||||
text*[b::B'_test']\<open>\<close>
|
||||
|
||||
term*\<open>@{B--test- \<open>b\<close>}\<close>
|
||||
|
||||
declare_reference*["text-elements-expls"::technical]
|
||||
(*>*)
|
||||
ML\<open>
|
||||
|
||||
\<close>
|
||||
subsection*["subsec:onto-term-ctxt"::technical]\<open>Ontological Term-Contexts and their Management\<close>
|
||||
text\<open>The major commands providing term-contexts are
|
||||
text\<open>
|
||||
\<^item> \<open>annotated_term_element\<close>
|
||||
\<^rail>\<open>
|
||||
(@@{command "term*"} ('[' meta_args ']')? '\<open>' HOL_term '\<close>'
|
||||
| (@@{command "value*"}
|
||||
| @@{command "assert*"}) \<newline> ('[' meta_args ']')? ('[' evaluator ']')? '\<open>' HOL_term '\<close>'
|
||||
| (@@{command "definition*"}) ('[' meta_args ']')?
|
||||
('... see ref manual')
|
||||
| (@@{command "lemma*"} | @@{command "theorem*"} | @@{command "corollary*"}
|
||||
| @@{command "proposition*"} | @@{command "schematic_goal*"}) ('[' meta_args ']')?
|
||||
('... see ref manual')
|
||||
)
|
||||
\<close>
|
||||
|
||||
For a declared class \<^theory_text>\<open>cid\<close>, there exists a term-antiquotation of the form \<^theory_text>\<open>@{cid \<open>oid\<close>}\<close>.
|
||||
Due to implementation of term-antiquotation using mixfix annotation
|
||||
(see @{cite "wenzel:isabelle-isar:2020"}),
|
||||
should a class \<open>cid\<close> contains an underscore or a single quote,
|
||||
they will be converted to hyphens in the term-antiquotation.
|
||||
For example:
|
||||
@{boxed_theory_text [display]
|
||||
\<open>doc_class B'_test' =
|
||||
b::int
|
||||
|
||||
text*[b::B'_test']\<open>\<close>
|
||||
|
||||
term*\<open>@{B--test- \<open>b\<close>}\<close>\<close>}
|
||||
|
||||
The major commands providing term-contexts are
|
||||
\<^theory_text>\<open>term*[oid::cid, ...] \<open> \<dots> HOL-term \<dots> \<close>\<close>,
|
||||
\<^theory_text>\<open>value*[oid::cid, ...] \<open> \<dots> HOL-term \<dots> \<close>\<close> and
|
||||
\<^theory_text>\<open>assert*[oid::cid, ...] \<open> \<dots> HOL-term \<dots> \<close>\<close>\<^footnote>\<open>The meta-argument list is optional.\<close>.
|
||||
Wrt. creation, track-ability and checking they are analogous to the ontological text and
|
||||
Wrt. creation, track-ability and checking these commands are analogous to the ontological text and
|
||||
code-commands. However the argument terms may contain term-antiquotations stemming from an
|
||||
ontology definition. Both term-contexts were type-checked and \<^emph>\<open>validated\<close> against
|
||||
the global context (so: in the term @{term_ \<open>@{author \<open>bu\<close>}\<close>}, \<open>bu\<close>
|
||||
ontology definition. Term-contexts were type-checked and \<^emph>\<open>validated\<close> against
|
||||
the global context (so: in the term @{term_ [source] \<open>@{author \<open>bu\<close>}\<close>}, \<open>bu\<close>
|
||||
is indeed a string which refers to a meta-object belonging
|
||||
to the document class \<^typ>\<open>author\<close>, for example).
|
||||
The term-context in the \<open>value*\<close>-command and \<^emph>\<open>assert*\<close>-command is additionally expanded
|
||||
Putting aside @{command "term*"}-command,
|
||||
the term-context in the other commands is additionally expanded
|
||||
(\<^eg> replaced) by a term denoting the meta-object.
|
||||
This expansion happens \<^emph>\<open>before\<close> evaluation of the term, thus permitting
|
||||
executable HOL-functions to interact with meta-objects.
|
||||
The \<^emph>\<open>assert*\<close>-command allows for logical statements to be checked in the global context
|
||||
The @{command "assert*"}-command allows for logical statements to be checked in the global context
|
||||
(see @{technical (unchecked) \<open>text-elements-expls\<close>}).
|
||||
% TODO:
|
||||
% Section reference @{docitem (unchecked) \<open>text-elements-expls\<close>} has not the right number
|
||||
This is particularly useful to explore formal definitions wrt. their border cases.
|
||||
|
||||
The @{command "definition*"}-command allows \<open>prop\<close>, \<open>spec_prems\<close>, and \<open>for_fixes\<close>
|
||||
(see the @{command "definition"} command in @{cite "wenzel:isabelle-isar:2020"}) to contain
|
||||
term-antiquotations. For example:
|
||||
@{boxed_theory_text [display]
|
||||
\<open>doc_class A =
|
||||
level :: "int option"
|
||||
x :: int
|
||||
definition*[a1::A, x=5, level="Some 1"] xx' where "xx' \<equiv> A.x @{A \<open>a1\<close>}" if "A.x @{A \<open>a1\<close>} = 5"\<close>}
|
||||
|
||||
The @{term_ [source] \<open>@{A \<open>a1\<close>}\<close>} term-antiquotation is used both in \<open>prop\<close> and in \<open>spec_prems\<close>.
|
||||
|
||||
@{command "lemma*"}, @{command "theorem*"}, etc., are extended versions of the goal commands
|
||||
defined in @{cite "wenzel:isabelle-isar:2020"}. Term-antiquotations can be used either in
|
||||
a \<open>long_statement\<close> or in a \<open>short_statement\<close>.
|
||||
For instance:
|
||||
@{boxed_theory_text [display]
|
||||
\<open>lemma*[e5::E] testtest : "xx + A.x @{A \<open>a1\<close>} = yy + A.x @{A \<open>a1\<close>} \<Longrightarrow> xx = yy"
|
||||
by simp\<close>}
|
||||
|
||||
This @{command "lemma*"}-command is defined using the @{term_ [source] \<open>@{A \<open>a1\<close>}\<close>}
|
||||
term-antiquotation and attaches the @{docitem_name "e5"} instance meta-data to the \<open>testtest\<close>-lemma.
|
||||
|
||||
@{boxed_theory_text [display]
|
||||
\<open>doc_class cc_assumption_test =
|
||||
a :: int
|
||||
text*[cc_assumption_test_ref::cc_assumption_test]\<open>\<close>
|
||||
|
||||
definition tag_l :: "'a \<Rightarrow> 'b \<Rightarrow> 'b" where "tag_l \<equiv> \<lambda>x y. y"
|
||||
|
||||
lemma* tagged : "tag_l @{cc-assumption-test \<open>cc_assumption_test_ref\<close>} AA \<Longrightarrow> AA"
|
||||
by (simp add: tag_l_def)
|
||||
|
||||
find_theorems name:tagged "(_::cc_assumption_test \<Rightarrow> _ \<Rightarrow> _) _ _ \<Longrightarrow>_"\<close>}
|
||||
|
||||
In this example, the definition \<^const>\<open>tag_l\<close> adds a tag to the \<open>tagged\<close> lemma using
|
||||
the term-antiquotation @{term_ [source] \<open>@{cc-assumption-test \<open>cc_assumption_test_ref\<close>}\<close>}
|
||||
inside the \<open>prop\<close> declaration.
|
||||
|
||||
Note unspecified attribute values were represented by free fresh variables which constrains \<^dof>
|
||||
to choose either the normalization-by-evaluation strategy \<^theory_text>\<open>nbe\<close> or a proof attempt via
|
||||
the \<^theory_text>\<open>auto\<close> method. A failure of these strategies will be reported and regarded as non-validation
|
||||
|
|
@ -447,7 +553,13 @@ declare_reference*["sec:advanced"::technical]
|
|||
(*>*)
|
||||
|
||||
subsection\<open>Status and Query Commands\<close>
|
||||
text\<open>\<^isadof> provides a number of inspection commands.
|
||||
|
||||
text\<open>
|
||||
\<^item> \<^isadof> \<open>inspection_command\<close> :
|
||||
\<^rail>\<open> @@{command "print_doc_classes"}
|
||||
| @@{command "print_doc_items"}
|
||||
| @@{command "check_doc_global"}\<close>
|
||||
\<^isadof> provides a number of inspection commands.
|
||||
\<^item> \<^theory_text>\<open>print_doc_classes\<close> allows to view the status of the internal
|
||||
class-table resulting from ODL definitions,
|
||||
\<^item> \<^ML>\<open>DOF_core.print_doc_class_tree\<close> allows for presenting (fragments) of
|
||||
|
|
@ -469,7 +581,13 @@ text\<open>\<^isadof> provides a number of inspection commands.
|
|||
\<close>
|
||||
|
||||
subsection\<open>Macros\<close>
|
||||
text\<open>There is a mechanism to define document-local macros which
|
||||
text\<open>
|
||||
\<^item> \<^isadof> \<open>macro_command\<close> :
|
||||
\<^rail>\<open> @@{command "define_shortcut*"} name ('\<rightleftharpoons>' | '==') '\<open>' string '\<close>'
|
||||
| @@{command "define_macro*"} name ('\<rightleftharpoons>' | '==')
|
||||
\<newline> '\<open>' string '\<close>' '_' '\<open>' string '\<close>' \<close>
|
||||
|
||||
There is a mechanism to define document-local macros which
|
||||
were PIDE-supported but lead to an expansion in the integrated source; this feature
|
||||
can be used to define
|
||||
\<^item> \<^theory_text>\<open>shortcuts\<close>, \<^ie>, short names that were expanded to, for example,
|
||||
|
|
@ -1016,6 +1134,7 @@ text\<open>
|
|||
closing of a monitor.
|
||||
For this use-case you can use low-level class invariants
|
||||
(see @{technical (unchecked) "sec:low_level_inv"}).
|
||||
Also, for now, term-antiquotations can not be used in an invariant formula.
|
||||
\<close>
|
||||
|
||||
subsection*["sec:monitors"::technical]\<open>ODL Monitors\<close>
|
||||
|
|
@ -1108,27 +1227,28 @@ text\<open>
|
|||
(note the long name of the class),
|
||||
is straight-forward:
|
||||
|
||||
\begin{sml}
|
||||
fun check_result_inv oid {is_monitor:bool} ctxt =
|
||||
@{boxed_sml [display]
|
||||
\<open>fun check_result_inv oid {is_monitor:bool} ctxt =
|
||||
let
|
||||
val kind =
|
||||
ISA_core.compute_attr_access ctxt "evidence" oid NONE <@>{here}
|
||||
ISA_core.compute_attr_access ctxt "evidence" oid NONE @{here}
|
||||
val prop =
|
||||
ISA_core.compute_attr_access ctxt "property" oid NONE <@>{here}
|
||||
ISA_core.compute_attr_access ctxt "property" oid NONE @{here}
|
||||
val tS = HOLogic.dest_list prop
|
||||
in case kind of
|
||||
<@>{term "proof"} => if not(null tS) then true
|
||||
@{term "proof"} => if not(null tS) then true
|
||||
else error("class result invariant violation")
|
||||
| _ => false
|
||||
| _ => true
|
||||
end
|
||||
val _ = Theory.setup (DOF_core.update_class_invariant
|
||||
"Low_Level_Syntax_Invariants.result" check_result_inv)
|
||||
\end{sml}
|
||||
val cid_long = DOF_core.get_onto_class_name_global "result" @{theory}
|
||||
val bind = Binding.name "Check_Result"
|
||||
val _ = Theory.setup (DOF_core.make_ml_invariant (check_result_inv, cid_long)
|
||||
|> DOF_core.add_ml_invariant bind)\<close>}
|
||||
|
||||
The \<^ML>\<open>Theory.setup\<close>-command (last line) registers the \<^boxed_theory_text>\<open>check_result_inv\<close> function
|
||||
into the \<^isadof> kernel, which activates any creation or modification of an instance of
|
||||
\<^boxed_theory_text>\<open>result\<close>. We cannot replace \<^boxed_theory_text>\<open>compute_attr_access\<close> by the
|
||||
corresponding antiquotation \<^boxed_theory_text>\<open>@{docitem_value kind::oid}\<close>, since
|
||||
corresponding antiquotation \<^boxed_theory_text>\<open>\<^value_>\<open>evidence @{result \<open>oid\<close>}\<close>\<close>, since
|
||||
\<^boxed_theory_text>\<open>oid\<close> is bound to a variable here and can therefore not be statically expanded.
|
||||
\<close>
|
||||
|
||||
|
|
@ -12,8 +12,8 @@
|
|||
*************************************************************************)
|
||||
|
||||
(*<*)
|
||||
theory "05_Implementation"
|
||||
imports "04_RefMan"
|
||||
theory "M_05_Implementation"
|
||||
imports "M_04_RefMan"
|
||||
begin
|
||||
(*>*)
|
||||
|
||||
|
|
@ -108,15 +108,21 @@ val attributes =(Parse.$$$ "[" |-- (reference
|
|||
|--(Parse.enum ","attribute)))[]))--| Parse.$$$ "]"
|
||||
\end{sml}
|
||||
|
||||
The ``model'' \<^boxed_sml>\<open>declare_reference_opn\<close> and ``new'' \<^boxed_sml>\<open>attributes\<close> parts were
|
||||
The ``model'' \<^boxed_sml>\<open>create_and_check_docitem\<close> and ``new''
|
||||
\<^boxed_sml>\<open>ODL_Meta_Args_Parser.attributes\<close> parts were
|
||||
combined via the piping operator and registered in the Isar toplevel:
|
||||
|
||||
@{boxed_sml [display]
|
||||
\<open>fun declare_reference_opn (((oid,_),_),_) =
|
||||
(Toplevel.theory (DOF_core.declare_object_global oid))
|
||||
val _ = Outer_Syntax.command <@>{command_keyword "declare_reference"}
|
||||
"declare document reference"
|
||||
(attributes >> declare_reference_opn);\<close>}
|
||||
\<open>val _ =
|
||||
let fun create_and_check_docitem (((oid, pos),cid_pos),doc_attrs)
|
||||
= (Value_Command.Docitem_Parser.create_and_check_docitem
|
||||
{is_monitor = false} {is_inline=true}
|
||||
{define = false} oid pos (cid_pos) (doc_attrs))
|
||||
in Outer_Syntax.command @{command_keyword "declare_reference*"}
|
||||
"declare document reference"
|
||||
(ODL_Meta_Args_Parser.attributes
|
||||
>> (Toplevel.theory o create_and_check_docitem))
|
||||
end;\<close>}
|
||||
|
||||
Altogether, this gives the extension of Isabelle/HOL with Isar syntax and semantics for the
|
||||
new \emph{command}:
|
||||
|
|
@ -126,7 +132,7 @@ declare_reference* [lal::requirement, alpha="main", beta=42]
|
|||
\<close>}
|
||||
|
||||
The construction also generates implicitly some markup information; for example, when hovering
|
||||
over the \<^boxed_theory_text>\<open>declare_reference\<close> command in the IDE, a popup window with the text:
|
||||
over the \<^boxed_theory_text>\<open>declare_reference*\<close> command in the IDE, a popup window with the text:
|
||||
``declare document reference'' will appear.
|
||||
\<close>
|
||||
|
||||
|
|
@ -137,12 +143,10 @@ text\<open>
|
|||
can be added to the system that works on the internal plugin-data freely. For example, in
|
||||
|
||||
@{boxed_sml [display]
|
||||
\<open>val _ = Theory.setup(
|
||||
Thy_Output.antiquotation <@>{binding docitem}
|
||||
docitem_antiq_parser
|
||||
(docitem_antiq_gen default_cid) #>
|
||||
ML_Antiquotation.inline <@>{binding docitem_value}
|
||||
ML_antiq_docitem_value)\<close>}
|
||||
\<open>val _ = Theory.setup
|
||||
(docitem_antiquotation @{binding "docitem"} DOF_core.default_cid #>
|
||||
|
||||
ML_Antiquotation.inline @{binding "docitem_value"} ML_antiquotation_docitem_value)\<close>}
|
||||
the text antiquotation \<^boxed_sml>\<open>docitem\<close> is declared and bounded to a parser for the argument
|
||||
syntax and the overall semantics. This code defines a generic antiquotation to be used in text
|
||||
elements such as
|
||||
Loading…
Reference in New Issue