added support for math_content-class in scholarly_paper in Knuth's Urschleim.
This commit is contained in:
parent
aa4e1acf84
commit
f1b376d4b6
|
|
@ -1857,21 +1857,23 @@ fun add_doc_class_cmd overloaded (raw_params, binding)
|
|||
|
||||
end;
|
||||
|
||||
val parse_invariants = Parse.and_list (Args.name_position --| Parse.$$$ "::" -- Parse.term)
|
||||
|
||||
val _ =
|
||||
Outer_Syntax.command \<^command_keyword>\<open>doc_class\<close> "define document class"
|
||||
((Parse_Spec.overloaded
|
||||
-- (Parse.type_args_constrained -- Parse.binding)
|
||||
-- (\<^keyword>\<open>=\<close>
|
||||
|-- Scan.option (Parse.typ --| \<^keyword>\<open>+\<close>)
|
||||
|-- Scan.option (Parse.typ --| \<^keyword>\<open>+\<close>)
|
||||
-- Scan.repeat1 (Parse.const_binding -- Scan.option (\<^keyword>\<open><=\<close> |-- Parse.term))
|
||||
)
|
||||
-- ( Scan.optional (\<^keyword>\<open>rejects\<close> |-- Parse.enum1 "," Parse.term) []
|
||||
-- Scan.repeat (\<^keyword>\<open>accepts\<close> |-- Parse.term)
|
||||
-- Scan.repeats ((\<^keyword>\<open>invariant\<close>) |--
|
||||
Parse.and_list (Args.name_position --| Parse.$$$ "::" -- Parse.term)))
|
||||
-- ( Scan.optional (\<^keyword>\<open>rejects\<close> |-- Parse.enum1 "," Parse.term) []
|
||||
-- Scan.repeat (\<^keyword>\<open>accepts\<close> |-- Parse.term)
|
||||
-- Scan.repeats ((\<^keyword>\<open>invariant\<close>) |-- parse_invariants))
|
||||
)
|
||||
>> (fn (((overloaded, x), (y, z)),((rejectS,accept_rex),invs)) =>
|
||||
Toplevel.theory (add_doc_class_cmd {overloaded = overloaded} x y z rejectS accept_rex invs)));
|
||||
>> (fn (((overloaded, hdr), (parent, attrs)),((rejects,accept_rex),invars)) =>
|
||||
Toplevel.theory (add_doc_class_cmd {overloaded = overloaded} hdr parent
|
||||
attrs rejects accept_rex invars)));
|
||||
|
||||
end (* struct *)
|
||||
\<close>
|
||||
|
|
@ -1900,22 +1902,5 @@ 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>
|
||||
*)
|
||||
|
||||
ML\<open> String.isSuffix "_asd" "sdfgsd_asd";
|
||||
|
||||
String.substring ("sdfgsd_asd", 0, size "sdfgsd_asd" - 4)\<close>
|
||||
ML\<open>Long_Name.qualifier "dgfdfg.dfgdfg.qwe"\<close>
|
||||
|
||||
|
||||
end
|
||||
|
|
|
|||
|
|
@ -154,14 +154,16 @@
|
|||
\end{isamarkuptext}%
|
||||
}
|
||||
|
||||
\newtheorem{axiom}{Axiom}
|
||||
\newtheorem{ruleX}{Rule} % apparent name-clash with s th from libraries...
|
||||
\newtheorem{assertion}{Assertion}
|
||||
|
||||
% end: scholarly_paper.abstract
|
||||
|
||||
|
||||
% "def" | "axm" | "thm" | "lem" | "prop" | "rule" | "assn"
|
||||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||
\newisadof{text.scholarly_paper.math_content}%
|
||||
[label=,type=%
|
||||
, scholarly_paper.math_content.short_name =%
|
||||
, scholarly_paper.math_content.short_name ={\relax}% {} or \relax
|
||||
, scholarly_paper.math_content.mcc =%
|
||||
, Isa_COL.text_element.level =%
|
||||
, Isa_COL.text_element.referentiable =%
|
||||
|
|
@ -175,18 +177,89 @@
|
|||
[1]
|
||||
{%
|
||||
\begin{isamarkuptext}%
|
||||
\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.mcc}}{def}}{
|
||||
\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.short_name}} {} }
|
||||
{\begin{definition} \label{\commandkey{label}} #1 \end{definition} }
|
||||
{\begin{definition} [\commandkey{scholarly_paper.math_content.short_name}]
|
||||
\label{\commandkey{label}} #1
|
||||
\end{definition}}
|
||||
}{%
|
||||
#1%
|
||||
\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.mcc}}{def}}
|
||||
{%
|
||||
\begin{definition}[\commandkey{scholarly_paper.math_content.short_name}]
|
||||
\label{\commandkey{label}} #1
|
||||
\end{definition}%
|
||||
}%
|
||||
{\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.mcc}}{axm}}
|
||||
{%
|
||||
\begin{axiom}[\commandkey{scholarly_paper.math_content.short_name}]
|
||||
\label{\commandkey{label}} #1
|
||||
\end{axiom}%
|
||||
}%
|
||||
{\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.mcc}}{thm}}
|
||||
{%
|
||||
\begin{theorem}[\commandkey{scholarly_paper.math_content.short_name}]
|
||||
\label{\commandkey{label}} #1
|
||||
\end{theorem}%
|
||||
}%
|
||||
{\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.mcc}}{lem}}
|
||||
{%
|
||||
\begin{lemma}[\commandkey{scholarly_paper.math_content.short_name}]
|
||||
\label{\commandkey{label}} #1
|
||||
\end{lemma}%
|
||||
}%
|
||||
{\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.mcc}}{prop}}
|
||||
{%
|
||||
\begin{property}[\commandkey{scholarly_paper.math_content.short_name}]
|
||||
\label{\commandkey{label}} #1
|
||||
\end{property}%
|
||||
}%
|
||||
{\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.mcc}}{rule}}
|
||||
{%
|
||||
\begin{ruleX}[\commandkey{scholarly_paper.math_content.short_name}]
|
||||
\label{\commandkey{label}} #1
|
||||
\end{ruleX}%
|
||||
}%
|
||||
{\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.mcc}}{assn}}
|
||||
{%
|
||||
\begin{assertion}[\commandkey{scholarly_paper.math_content.short_name}]
|
||||
\label{\commandkey{label}} #1
|
||||
\end{assertion}%
|
||||
}%
|
||||
{%
|
||||
#1% BETTER: Since enumeration, there should be here the best possible error-msg here
|
||||
}%
|
||||
}%
|
||||
}%
|
||||
}%
|
||||
}%
|
||||
}%
|
||||
}%
|
||||
\end{isamarkuptext}%
|
||||
}
|
||||
|
||||
%\newisadof{text.scholarly_paper.math_content}%
|
||||
%[label=,type=%
|
||||
% , scholarly_paper.math_content.short_name ={} % or \relax
|
||||
% , scholarly_paper.math_content.mcc =%
|
||||
% , 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.math_content.mcc}}{def}}{
|
||||
% \ifthenelse{\equal{\commandkey{scholarly_paper.math_content.short_name}} {} }
|
||||
% {\begin{definition} \label{\commandkey{label}} #1 \end{definition} }
|
||||
% {\begin{definition} [\commandkey{scholarly_paper.math_content.short_name}]
|
||||
% \label{\commandkey{label}} #1
|
||||
% \end{definition}}
|
||||
% }{%
|
||||
% #1%
|
||||
% }%
|
||||
% \end{isamarkuptext}%
|
||||
% }
|
||||
|
||||
|
||||
% end: scholarly_paper.abstract
|
||||
|
||||
|
||||
|
|
|
|||
|
|
@ -119,8 +119,7 @@ type_synonym tc = technical (* technical content *)
|
|||
|
||||
subsection\<open>Mathematical Content\<close>
|
||||
|
||||
datatype math_content_class =
|
||||
"def" | "axm" | "thm" | "lem" | "prop" | "rule" | "assn"
|
||||
datatype math_content_class = "def" | "axm" | "thm" | "lem" | "prop" | "rule" | "assn"
|
||||
|
||||
text\<open>Instances of the \<open>doc_class\<close> \<^verbatim>\<open>math_content\<close> are by definition @{term "semiformal"}; they may
|
||||
be non-referential, but in this case they will not have a @{term "short_name"}.\<close>
|
||||
|
|
@ -129,7 +128,7 @@ doc_class math_content = tc +
|
|||
referentiable :: bool <= True
|
||||
short_name :: string <= "''''"
|
||||
status :: status <= "semiformal"
|
||||
mcc :: "math_content_class"
|
||||
mcc :: "math_content_class" <= "lem"
|
||||
invariant s1 :: "\<lambda> \<sigma>. \<not>referentiable \<sigma> \<longrightarrow> short_name \<sigma> = ''''"
|
||||
invariant s2 :: "\<lambda> \<sigma>. status \<sigma> = semiformal"
|
||||
|
||||
|
|
@ -147,6 +146,8 @@ type_synonym math_exp = math_explanation
|
|||
|
||||
doc_class math_example = tc +
|
||||
referentiable :: bool <= False
|
||||
short_name :: string <= "''''"
|
||||
invariant s1 :: "\<lambda> \<sigma>. \<not>referentiable \<sigma> \<longrightarrow> short_name \<sigma> = ''''"
|
||||
type_synonym math_ex = math_example
|
||||
|
||||
|
||||
|
|
|
|||
Loading…
Reference in New Issue