New Regrouping in the scholarly Onto + LaTeX support. Tested.
This commit is contained in:
parent
5c303a7192
commit
5b0db2efb1
|
|
@ -1860,6 +1860,16 @@ ML\<open>
|
|||
|
||||
\<close>
|
||||
*)
|
||||
ML\<open>open Thread\<close>
|
||||
|
||||
(* concurrency experiments:
|
||||
ML\<open>open Thread\<close>
|
||||
ML\<open>open Future\<close>
|
||||
ML\<open>open OS.Process\<close>
|
||||
ML\<open>ALLGOALS\<close>
|
||||
|
||||
ML\<open>open Goal\<close>
|
||||
ML \<open>future_result;\<close>
|
||||
*)
|
||||
|
||||
end
|
||||
|
|
|
|||
|
|
@ -182,6 +182,82 @@
|
|||
\end{isamarkuptext}%
|
||||
}
|
||||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||
\newisadof{text.scholarly_paper.theorem}%
|
||||
[label=,type=%
|
||||
, scholarly_paper.theorem.tag =%
|
||||
, Isa_COL.text_element.level =%
|
||||
, Isa_COL.text_element.referentiable =%
|
||||
, Isa_COL.text_element.variants =%
|
||||
, scholarly_paper.text_section.main_author =%
|
||||
, scholarly_paper.text_section.fixme_list =%
|
||||
, Isa_COL.text_element.level =%
|
||||
, scholarly_paper.technical.definition_list =%
|
||||
, scholarly_paper.technical.status =%
|
||||
]
|
||||
[1]
|
||||
{%
|
||||
\begin{isamarkuptext}%
|
||||
\ifthenelse{\equal{\commandkey{scholarly_paper.technical.status}}{semiformal}}{
|
||||
\ifthenelse{\equal{\commandkey{scholarly_paper.theorem.tag}} {} }
|
||||
{\begin{theorem} \label{\commandkey{label}} #1 \end{theorem} }
|
||||
{\begin{theorem} [\commandkey{scholarly_paper.theorem.tag}] \label{\commandkey{label}} #1 \end{theorem}}
|
||||
}{%
|
||||
#1%
|
||||
}%
|
||||
\end{isamarkuptext}%
|
||||
}
|
||||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||
\newisadof{text.scholarly_paper.lemma}%
|
||||
[label=,type=%
|
||||
, scholarly_paper.lemma.tag =%
|
||||
, Isa_COL.text_element.level =%
|
||||
, Isa_COL.text_element.referentiable =%
|
||||
, Isa_COL.text_element.variants =%
|
||||
, scholarly_paper.text_section.main_author =%
|
||||
, scholarly_paper.text_section.fixme_list =%
|
||||
, Isa_COL.text_element.level =%
|
||||
, scholarly_paper.technical.definition_list =%
|
||||
, scholarly_paper.technical.status =%
|
||||
]
|
||||
[1]
|
||||
{%
|
||||
\begin{isamarkuptext}%
|
||||
\ifthenelse{\equal{\commandkey{scholarly_paper.technical.status}}{semiformal}}{
|
||||
\ifthenelse{\equal{\commandkey{scholarly_paper.lemma.tag}} {} }
|
||||
{\begin{lemma} \label{\commandkey{label}} #1 \end{lemma} }
|
||||
{\begin{{} [\commandkey{scholarly_paper.lemma.tag}] \label{\commandkey{label}} #1 \end{{}}
|
||||
}{%
|
||||
#1%
|
||||
}%
|
||||
\end{isamarkuptext}%
|
||||
}
|
||||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||
\newisadof{text.scholarly_paper.corollary}%
|
||||
[label=,type=%
|
||||
, scholarly_paper.corollary.tag =%
|
||||
, Isa_COL.text_element.level =%
|
||||
, Isa_COL.text_element.referentiable =%
|
||||
, Isa_COL.text_element.variants =%
|
||||
, scholarly_paper.text_section.main_author =%
|
||||
, scholarly_paper.text_section.fixme_list =%
|
||||
, Isa_COL.text_element.level =%
|
||||
, scholarly_paper.technical.definition_list =%
|
||||
, scholarly_paper.technical.status =%
|
||||
]
|
||||
[1]
|
||||
{%
|
||||
\begin{isamarkuptext}%
|
||||
\ifthenelse{\equal{\commandkey{scholarly_paper.technical.status}}{semiformal}}{
|
||||
\ifthenelse{\equal{\commandkey{scholarly_paper.corollary.tag}} {} }
|
||||
{\begin{corollary} \label{\commandkey{label}} #1 \end{corollary} }
|
||||
{\begin{corollary} [\commandkey{scholarly_paper.corollary.tag}] \label{\commandkey{label}} #1 \end{corollary}}
|
||||
}{%
|
||||
#1%
|
||||
}%
|
||||
\end{isamarkuptext}%
|
||||
}
|
||||
|
||||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||
\newisadof{text.scholarly_paper.example}%
|
||||
[label=,type=%
|
||||
, scholarly_paper.example.tag =%
|
||||
|
|
|
|||
|
|
@ -65,19 +65,20 @@ A formal statement can, but must not have a reference to true formal Isabelle/Is
|
|||
\<close>
|
||||
datatype status = semiformal | description
|
||||
|
||||
text\<open>The class \<^verbatim>\<open>technical\<close> regroups a number of text-elements that contain typical
|
||||
"technical content" in mathematical or engineering papers: definitions, theorems, lemmas, examples. \<close>
|
||||
|
||||
(* OPEN PROBLEM: connection between referentiable and status. This should be explicit
|
||||
and computable. *)
|
||||
|
||||
(* TODO : RENAME "tag" by "short_name" *)
|
||||
|
||||
doc_class technical = text_section +
|
||||
definition_list :: "string list" <= "[]"
|
||||
status :: status <= "description"
|
||||
formal_results :: "thm list"
|
||||
|
||||
text\<open>A very rough formatting style could be modeled as follows:\<close>
|
||||
|
||||
|
||||
doc_class "experiment" = technical +
|
||||
tag :: "string" <= "''''"
|
||||
|
||||
doc_class example = technical +
|
||||
tag :: "string" <= "''''"
|
||||
text\<open>A rough structuring is modeled as follows:\<close>
|
||||
|
||||
doc_class "definition" = technical +
|
||||
tag :: "string" <= "''''"
|
||||
|
|
@ -85,10 +86,39 @@ doc_class "definition" = technical +
|
|||
doc_class "theorem" = technical +
|
||||
tag :: "string" <= "''''"
|
||||
|
||||
text\<open>Note that the following two text-elements are currently set to no-keyword in LNCS style.\<close>
|
||||
doc_class "lemma" = technical +
|
||||
tag :: "string" <= "''''"
|
||||
|
||||
doc_class "corollary" = technical +
|
||||
tag :: "string" <= "''''"
|
||||
|
||||
|
||||
text\<open> \<^verbatim>\<open>examples\<close> are currently considered \<^verbatim>\<open>technical\<close>. Another alternative would be to group the
|
||||
following classes into an own class: "evaluation" or "explanation" or ... \<close>
|
||||
|
||||
doc_class example = technical +
|
||||
tag :: "string" <= "''''"
|
||||
|
||||
doc_class assertion = technical +
|
||||
tag :: "string" <= "''''"
|
||||
|
||||
|
||||
(* TODO :*)
|
||||
(* attention : no LaTeX support yet >>> *)
|
||||
doc_class "code" = technical +
|
||||
checked :: bool <= "False"
|
||||
tag :: "string" <= "''''"
|
||||
|
||||
doc_class "experiment" = technical +
|
||||
tag :: "string" <= "''''"
|
||||
|
||||
doc_class "evaluation" = technical +
|
||||
tag :: "string" <= "''''"
|
||||
|
||||
doc_class "data" = technical +
|
||||
tag :: "string" <= "''''"
|
||||
|
||||
text\<open>The @{doc_class "code"} is a general stub for free-form and type-checked code-fragments
|
||||
such as:
|
||||
\<^enum> SML code
|
||||
|
|
@ -143,14 +173,14 @@ text \<open>underlying idea: a monitor class automatically receives a
|
|||
doc_class article =
|
||||
style_id :: string <= "''LNCS''"
|
||||
version :: "(int \<times> int \<times> int)" <= "(0,0,0)"
|
||||
accepts "(title ~~
|
||||
\<lbrakk>subtitle\<rbrakk> ~~
|
||||
\<lbrace>author\<rbrace>\<^sup>+ ~~
|
||||
abstract ~~
|
||||
accepts "(title ~~
|
||||
\<lbrakk>subtitle\<rbrakk> ~~
|
||||
\<lbrace>author\<rbrace>\<^sup>+ ~~
|
||||
abstract ~~
|
||||
\<lbrace>introduction\<rbrace>\<^sup>+ ~~
|
||||
\<lbrace>technical || example\<rbrace>\<^sup>+ ~~
|
||||
\<lbrace>conclusion\<rbrace>\<^sup>+ ~~
|
||||
bibliography ~~
|
||||
\<lbrace>technical\<rbrace>\<^sup>+ ~~
|
||||
\<lbrace>conclusion\<rbrace>\<^sup>+ ~~
|
||||
bibliography ~~
|
||||
\<lbrace>annex\<rbrace>\<^sup>* )"
|
||||
|
||||
|
||||
|
|
|
|||
|
|
@ -29,8 +29,10 @@ They are the key-mechanism to denote
|
|||
\<^item> Ontological Links, i.e. attributes refering to document classes defined by the ontology
|
||||
\<^item> Ontological F-Links, i.e. attributes referring to formal entities inside Isabelle (such as thm's)
|
||||
|
||||
This file contains a number of examples resulting from the @{theory "Isabelle_DOF-tests.Conceptual"} - ontology;
|
||||
the emphasis of this presentation is to present the expressivity of ODL on a paradigmatical example.
|
||||
This file contains a number of examples resulting from the
|
||||
% @ {theory "Isabelle_DOF-tests.Conceptual"} does not work here --- why ?
|
||||
\<^theory_text>\<open>Conceptual\<close> - ontology; the emphasis of this presentation is to present the expressivity of
|
||||
ODL on a paradigmatical example.
|
||||
\<close>
|
||||
|
||||
|
||||
|
|
@ -56,20 +58,20 @@ text\<open>Example for a meta-attribute of ODL-type @{typ "typ"} with an appropr
|
|||
theorem @{thm "refl"}}\<close>
|
||||
text*[xcv2::C, g="@{thm ''HOL.refl''}"]\<open>Lorem ipsum ...\<close>
|
||||
|
||||
text\<open>Major sample: test-item of doc-class \verb+F+ with a relational link, and links to formal
|
||||
Isabelle items. \<close>
|
||||
text\<open>Major sample: test-item of doc-class \<open>F\<close> with a relational link between class instances,
|
||||
and links to formal Isabelle items like \<open>typ\<close>, \<open>term\<close> and \<open>thm\<close>. \<close>
|
||||
text*[xcv4::F, r="[@{thm ''HOL.refl''},
|
||||
@{thm ''InnerSyntaxAntiquotations.murks''}]",
|
||||
b="{(@{docitem ''xcv1''},@{docitem ''xcv2''})}",
|
||||
s="[@{typ ''int list''}]",
|
||||
properties = "[@{term ''H --> H''}]"
|
||||
@{thm \<open>InnerSyntaxAntiquotations.murks\<close>}]", (* long names required *)
|
||||
b="{(@{docitem ''xcv1''},@{docitem \<open>xcv2\<close>})}", (* notations \<open>...\<close> vs. ''...'' *)
|
||||
s="[@{typ \<open>int list\<close>}]",
|
||||
properties = "[@{term \<open>H \<longrightarrow> H\<close>}]" (* notation \<open>...\<close> required for UTF8*)
|
||||
]\<open>Lorem ipsum ...\<close>
|
||||
|
||||
text*[xcv5::G, g="@{thm ''HOL.sym''}"]\<open>Lorem ipsum ...\<close>
|
||||
text*[xcv5::G, g="@{thm \<open>HOL.sym\<close>}"]\<open>Lorem ipsum ...\<close>
|
||||
|
||||
text\<open>... and here we add a relation between @{docitem \<open>xcv3\<close>} and @{docitem \<open>xcv2\<close>}
|
||||
into the relation \verb+b+ of @{docitem \<open>xcv5\<close>}. Note that in the link-relation,
|
||||
a @{typ "C"}-type is required, but a @{typ "G"}-type is offered which is leagal in
|
||||
a @{typ "C"}-type is required, but a @{typ "G"}-type is offered which is legal in
|
||||
\verb+Isa_DOF+ because of the sub-class relation between those classes: \<close>
|
||||
update_instance*[xcv4::F, b+="{(@{docitem ''xcv3''},@{docitem ''xcv5''})}"]
|
||||
|
||||
|
|
|
|||
Loading…
Reference in New Issue