eliminating deprecated syntax
This commit is contained in:
parent
e98e945b53
commit
0c4a5a5fea
|
|
@ -205,7 +205,8 @@ states them as three-fold differentiable function in certain bounds concerning s
|
|||
Note that violations, in particular of the constraints on speed and acceleration, \<^emph>\<open>do\<close> occur in practice.
|
||||
In such cases, the global system adapts recovery strategies that are out of the scope of our model.
|
||||
Concepts like \inlineisar+shaft_encoder_state+ (a triple with the sensor values
|
||||
\inlineisar{C1}, \inlineisar{C2}, \inlineisar{C3}) were formalized as types, while tables were defined as recursive functions:
|
||||
\inlineisar{C1}, \inlineisar{C2}, \inlineisar{C3}) were formalized as types, while tables were
|
||||
defined as recursive functions:
|
||||
\enlargethispage{2\baselineskip}\begin{isar}
|
||||
fun phase$_0$ :: "nat \<Rightarrow> shaft_encoder_state" where
|
||||
"phase$_0$ (0) = \<lparr> C1 = False, C2 = False, C3 = True \<rparr>"
|
||||
|
|
@ -561,10 +562,10 @@ to a test-environment or test-engine. \<close>
|
|||
|
||||
text\<open>Finally some examples of references to doc-items, i.e. text-elements with declared
|
||||
meta-information and status. \<close>
|
||||
text \<open> As established by @{docref (unchecked) \<open>t10\<close>},
|
||||
@{docref (define) \<open>t10\<close>} \<close>
|
||||
text \<open> the @{docref \<open>t10\<close>}
|
||||
as well as the @{docref \<open>ass122\<close>}\<close>
|
||||
text \<open> As established by @{docitem (unchecked) \<open>t10\<close>},
|
||||
@{docitem (define) \<open>t10\<close>} \<close>
|
||||
text \<open> the @{docitem \<open>t10\<close>}
|
||||
as well as the @{docitem \<open>ass122\<close>}\<close>
|
||||
text \<open> represent a justification of the safety related applicability
|
||||
condition @{SRAC \<open>ass122\<close>} aka exported constraint @{EC \<open>ass122\<close>}.\<close>
|
||||
|
||||
|
|
|
|||
|
|
@ -111,9 +111,9 @@ text*[plan::introduction]\<open> The plan of the paper is follows: we start by i
|
|||
Isabelel sytem (@{docitem (unchecked) \<open>bgrnd\<close>}) followed by presenting the
|
||||
essentials of \isadof and its ontology language (@{docitem (unchecked) \<open>isadof\<close>}).
|
||||
It follows @{docitem (unchecked) \<open>ontomod\<close>}, where we present three application
|
||||
scenarios from the point of view of the ontology modeling. In @{docitem_ref (unchecked) \<open>ontopide\<close>}
|
||||
scenarios from the point of view of the ontology modeling. In @{docitem (unchecked) \<open>ontopide\<close>}
|
||||
we discuss the user-interaction generated from the ontological definitions. Finally, we draw
|
||||
conclusions and discuss related work in @{docitem_ref (unchecked) \<open>conclusion\<close>}. \<close>
|
||||
conclusions and discuss related work in @{docitem (unchecked) \<open>conclusion\<close>}. \<close>
|
||||
|
||||
section*[bgrnd::text_section,main_author="Some(@{docitem ''adb''}::author)"]
|
||||
\<open> Background: The Isabelle System \<close>
|
||||
|
|
@ -146,7 +146,7 @@ figure*[architecture::figure,relative_width="100",src="''figures/isabelle-archit
|
|||
asynchronous communication between the Isabelle system and
|
||||
the IDE (right-hand side). \<close>
|
||||
|
||||
text*[blug::introduction]\<open> The Isabelle system architecture shown in @{docitem_ref \<open>architecture\<close>}
|
||||
text*[blug::introduction]\<open> The Isabelle system architecture shown in @{docitem \<open>architecture\<close>}
|
||||
comes with many layers, with Standard ML (SML) at the bottom layer as implementation
|
||||
language. The architecture actually foresees a \<^emph>\<open>Nano-Kernel\<close> (our terminology) which
|
||||
resides in the SML structure \texttt{Context}. This structure provides a kind of container called
|
||||
|
|
@ -399,7 +399,7 @@ figure*[fig_figures::figure,spawn_columns=False,relative_width="85",src="''figur
|
|||
|
||||
text\<open> The document class \inlineisar+figure+ --- supported by the \isadof text command
|
||||
\inlineisar+figure*+ --- makes it possible to express the pictures and diagrams in this paper
|
||||
such as @{docitem_ref \<open>fig_figures\<close>}.
|
||||
such as @{docitem \<open>fig_figures\<close>}.
|
||||
\<close>
|
||||
|
||||
subsection*[math_exam::example]\<open> The Math-Exam Scenario \<close>
|
||||
|
|
@ -518,7 +518,7 @@ declare_reference*["fig_qcm"::figure]
|
|||
|
||||
text\<open> Using the \LaTeX{} package hyperref, it is possible to conceive an interactive
|
||||
exam-sheets with multiple-choice and/or free-response elements
|
||||
(see @{docitem_ref (unchecked) \<open>fig_qcm\<close>}). With the
|
||||
(see @{docitem (unchecked) \<open>fig_qcm\<close>}). With the
|
||||
help of the latter, it is possible that students write in a browser a formal mathematical
|
||||
derivation---as part of an algebra exercise, for example---which is submitted to the examiners
|
||||
electronically. \<close>
|
||||
|
|
@ -632,7 +632,7 @@ figure*[figDogfoodVIlinkappl::figure,relative_width="80",src="''figures/Dogfood-
|
|||
\<open> Exploring an attribute (hyperlinked to the class). \<close>
|
||||
subsection*[cenelec_pide::example]\<open> CENELEC \<close>
|
||||
declare_reference*[figfig3::figure]
|
||||
text\<open> The corresponding view in @{docitem_ref (unchecked) \<open>figfig3\<close>} shows core part of a document,
|
||||
text\<open> The corresponding view in @{docitem (unchecked) \<open>figfig3\<close>} shows core part of a document,
|
||||
coherent to the @{example \<open>cenelec_onto\<close>}. The first sample shows standard Isabelle antiquotations
|
||||
@{cite "wenzel:isabelle-isar:2017"} into formal entities of a theory. This way, the informal parts
|
||||
of a document get ``formal content'' and become more robust under change.\<close>
|
||||
|
|
@ -641,7 +641,7 @@ figure*[figfig3::figure,relative_width="80",src="''figures/antiquotations-PIDE''
|
|||
\<open> Standard antiquotations referring to theory elements.\<close>
|
||||
|
||||
declare_reference*[figfig5::figure]
|
||||
text\<open> The subsequent sample in @{docitem_ref (unchecked) \<open>figfig5\<close>} shows the definition of an
|
||||
text\<open> The subsequent sample in @{docitem (unchecked) \<open>figfig5\<close>} shows the definition of an
|
||||
\<^emph>\<open>safety-related application condition\<close>, a side-condition of a theorem which
|
||||
has the consequence that a certain calculation must be executed sufficiently fast on an embedded
|
||||
device. This condition can not be established inside the formal theory but has to be
|
||||
|
|
@ -652,7 +652,7 @@ figure*[figfig5::figure, relative_width="80", src="''figures/srac-definition''"]
|
|||
figure*[figfig7::figure, relative_width="80", src="''figures/srac-as-es-application''"]
|
||||
\<open> Using a SRAC as EC document reference. \<close>
|
||||
|
||||
text\<open> Now we reference in @{docitem_ref (unchecked) \<open>figfig7\<close>} this safety-related condition;
|
||||
text\<open> Now we reference in @{docitem (unchecked) \<open>figfig7\<close>} this safety-related condition;
|
||||
however, this happens in a context where general \<^emph>\<open>exported constraints\<close> are listed.
|
||||
\isadof's checks establish that this is legal in the given ontology.
|
||||
|
||||
|
|
|
|||
|
|
@ -70,13 +70,13 @@ This manual can be read in different ways, depending on what you want to accompl
|
|||
different main user groups:
|
||||
\<^enum> \<^emph>\<open>\isadof users\<close>, \ie, users that just want to edit a core document, be it for a paper or a
|
||||
technical report, using a given ontology. These users should focus on
|
||||
@{docitem_ref (unchecked) \<open>isadof_tour\<close>} and, depending on their knowledge of Isabelle/HOL, also
|
||||
@{docitem_ref (unchecked) \<open>background\<close>}.
|
||||
@{docitem (unchecked) \<open>isadof_tour\<close>} and, depending on their knowledge of Isabelle/HOL, also
|
||||
@{docitem (unchecked) \<open>background\<close>}.
|
||||
\<^enum> \<^emph>\<open>Ontology developers\<close>, \ie, users that want to develop new ontologies or modify existing
|
||||
document ontologies. These users should, after having gained acquaintance as a user, focus
|
||||
on @{docitem_ref (unchecked) \<open>isadof_ontologies\<close>}.
|
||||
on @{docitem (unchecked) \<open>isadof_ontologies\<close>}.
|
||||
\<^enum> \<^emph>\<open>\isadof developers\<close>, \ie, users that want to extend or modify \isadof, \eg, by adding new
|
||||
text-elements. These users should read @{docitem_ref (unchecked) \<open>isadof_developers\<close>}
|
||||
text-elements. These users should read @{docitem (unchecked) \<open>isadof_developers\<close>}
|
||||
\<close>
|
||||
|
||||
subsubsection\<open>Typographical Conventions\<close>
|
||||
|
|
|
|||
|
|
@ -45,7 +45,7 @@ The current system framework offers moreover the following features:
|
|||
the most prominent and deeply integrated system component.
|
||||
|
||||
|
||||
The Isabelle system architecture shown in @{docitem_ref \<open>architecture\<close>} comes with many layers,
|
||||
The Isabelle system architecture shown in @{docitem \<open>architecture\<close>} comes with many layers,
|
||||
with Standard ML (SML) at the bottom layer as implementation language. The architecture actually
|
||||
foresees a \<^emph>\<open>Nano-Kernel\<close> (our terminology) which resides in the SML structure \inlinesml{Context}.
|
||||
This structure provides a kind of container called \<^emph>\<open>context\<close> providing an identity, an
|
||||
|
|
|
|||
|
|
@ -389,7 +389,7 @@ figure*[fig_figures::figure,spawn_columns=False,relative_width="85",src="''figur
|
|||
|
||||
text\<open>
|
||||
The document class \inlineisar+figure+ (supported by the \isadof command \inlineisar+figure*+)
|
||||
makes it possible to express the pictures and diagrams such as @{docitem_ref \<open>fig_figures\<close>}.
|
||||
makes it possible to express the pictures and diagrams such as @{docitem \<open>fig_figures\<close>}.
|
||||
|
||||
Finally, we define a monitor class definition that enforces a textual ordering
|
||||
in the document core by a regular expression:
|
||||
|
|
@ -430,7 +430,7 @@ figure*[figDogfoodVIlinkappl::figure,relative_width="80",src="''figures/Dogfood-
|
|||
\<open> Exploring an attribute (hyperlinked to the class). \<close>
|
||||
|
||||
text\<open>
|
||||
An ontological reference application in @{docitem_ref "figDogfoodVIlinkappl"}: the
|
||||
An ontological reference application in @{docitem "figDogfoodVIlinkappl"}: the
|
||||
ontology-dependant antiquotation \inlineisar|@ {example ...}| refers to the corresponding
|
||||
text-elements. Hovering allows for inspection, clicking for jumping to the definition. If the
|
||||
link does not exist or has a non-compatible type, the text is not validated.
|
||||
|
|
@ -550,7 +550,7 @@ result communication times \ldots \<close>
|
|||
subsection*[ontopide::technical]\<open>Editing Support for CENELEC 50128\<close>
|
||||
figure*[figfig3::figure,relative_width="95",src="''figures/antiquotations-PIDE''"]
|
||||
\<open> Standard antiquotations referring to theory elements.\<close>
|
||||
text\<open> The corresponding view in @{docitem_ref \<open>figfig3\<close>} shows core part of a document
|
||||
text\<open> The corresponding view in @{docitem \<open>figfig3\<close>} shows core part of a document
|
||||
conformimg to the CENELEC 50128 ontology. The first sample shows standard Isabelle antiquotations
|
||||
@{cite "wenzel:isabelle-isar:2019"} into formal entities of a theory. This way, the informal parts
|
||||
of a document get ``formal content'' and become more robust under change.\<close>
|
||||
|
|
@ -559,11 +559,11 @@ figure*[figfig5::figure, relative_width="95", src="''figures/srac-definition''"]
|
|||
\<open> Defining a SRAC reference \ldots \<close>
|
||||
figure*[figfig7::figure, relative_width="95", src="''figures/srac-as-es-application''"]
|
||||
\<open> Using a SRAC as EC document reference. \<close>
|
||||
text\<open> The subsequent sample in @{docitem_ref \<open>figfig5\<close>} shows the definition of an
|
||||
text\<open> The subsequent sample in @{docitem \<open>figfig5\<close>} shows the definition of an
|
||||
\<^emph>\<open>safety-related application condition\<close>, a side-condition of a theorem which
|
||||
has the consequence that a certain calculation must be executed sufficiently fast on an embedded
|
||||
device. This condition can not be established inside the formal theory but has to be
|
||||
checked by system integration tests. Now we reference in @{docitem_ref \<open>figfig7\<close>} this
|
||||
checked by system integration tests. Now we reference in @{docitem \<open>figfig7\<close>} this
|
||||
safety-related condition; however, this happens in a context where general \<^emph>\<open>exported constraints\<close>
|
||||
are listed. \isadof's checks establish that this is legal in the given ontology.
|
||||
\<close>
|
||||
|
|
@ -713,7 +713,7 @@ text\<Open> This is *\<Open>emphasized\<Close> a$$nd this is a
|
|||
Clearly, this is not always possible and, in fact, often \isadof documents will contain
|
||||
\LaTeX-commands, this should be restricted to layout improvements that otherwise are (currently)
|
||||
not possible. As far as possible, the use of \LaTeX-commands should be restricted to the definition
|
||||
of ontologies and document templates (see @{docitem_ref (unchecked) \<open>isadof_ontologies\<close>}).
|
||||
of ontologies and document templates (see @{docitem (unchecked) \<open>isadof_ontologies\<close>}).
|
||||
|
||||
Restricting the use of \LaTeX has two advantages: first, \LaTeX commands can circumvent the
|
||||
consistency checks of \isadof and, hence, only if no \LaTeX commands are used, \isadof can
|
||||
|
|
|
|||
|
|
@ -770,7 +770,7 @@ text\<open>
|
|||
Moreover, you might want to add/modify the template specific configuration
|
||||
(\autoref{lst:config-start}-\ref{lst:config-end}). The new template should be stored in
|
||||
\path{src/document-templates} and its file name should start with the prefix \path{root-}. After
|
||||
adding a new template, call the \inlinebash{install} script (see @{docref "infrastructure"}
|
||||
adding a new template, call the \inlinebash{install} script (see @{docitem "infrastructure"}
|
||||
The common structure of an \isadof document template looks as follows:
|
||||
|
||||
\begin{ltx}[escapechar=ë, numbers=left,numberstyle=\tiny,xleftmargin=5mm]
|
||||
|
|
|
|||
|
|
@ -188,7 +188,7 @@ text\<open>
|
|||
section\<open>Programming Class Invariants\<close>
|
||||
text\<open>
|
||||
For the moment, there is no high-level syntax for the definition of class invariants. A
|
||||
formulation, in SML, of the first class-invariant in @{docref "sec:class_inv"} is straight-forward:
|
||||
formulation, in SML, of the first class-invariant in @{docitem "sec:class_inv"} is straight-forward:
|
||||
|
||||
\begin{sml}
|
||||
fun check_result_inv oid {is_monitor:bool} ctxt =
|
||||
|
|
@ -223,7 +223,7 @@ text\<open>
|
|||
\end{sml}
|
||||
where \inlineisar+env+ is basically a map between internal automaton states and class-id's
|
||||
(\inlineisar+cid+'s). An automaton is said to be \<^emph>\<open>enabled\<close> for a class-id,
|
||||
iff it either occurs in its accept-set or its reject-set (see @{docref "sec:monitors"}). During
|
||||
iff it either occurs in its accept-set or its reject-set (see @{docitem "sec:monitors"}). During
|
||||
top-down document validation, whenever a text-element is encountered, it is checked if a monitor
|
||||
is \emph{enabled} for this class; in this case, the \inlineisar+next+-operation is executed. The
|
||||
transformed automaton recognizing the rest-language is stored in \inlineisar+docobj_tab+ if
|
||||
|
|
@ -247,9 +247,9 @@ text\<open>
|
|||
\end{ltx}
|
||||
|
||||
The \LaTeX-generator of \isadof maps each \inlineisar{doc_item} to an \LaTeX-environment (recall
|
||||
@{docref "text-elements"}). As generic \inlineisar{doc_item} are derived from the text element,
|
||||
@{docitem "text-elements"}). As generic \inlineisar{doc_item} are derived from the text element,
|
||||
the enviornment \inlineltx|{isamarkuptext*}| builds the core of \isadof's \LaTeX{} implementation.
|
||||
For example, the @{docref "ass123"} from page \pageref{ass123} is mapped to
|
||||
For example, the @{docitem "ass123"} from page \pageref{ass123} is mapped to
|
||||
|
||||
\begin{ltx}
|
||||
\begin{isamarkuptext*}%
|
||||
|
|
@ -262,7 +262,7 @@ text\<open>
|
|||
\end{isamarkuptext*}
|
||||
\end{ltx}
|
||||
|
||||
This environment is mapped to a plain \LaTeX command via (again, recall @{docref "text-elements"}):
|
||||
This environment is mapped to a plain \LaTeX command via (again, recall @{docitem "text-elements"}):
|
||||
\begin{ltx}
|
||||
\NewEnviron{isamarkuptext*}[1][]{\isaDof[env={text},#1]{\BODY}}
|
||||
\end{ltx}
|
||||
|
|
|
|||
|
|
@ -90,7 +90,7 @@ doc_class text_element =
|
|||
variants :: "String.literal set" <= "{STR ''outline'', STR ''document''}"
|
||||
|
||||
section\<open>Some attempt to model standardized links to Standard Isabelle Formal Content\<close>
|
||||
|
||||
(* Deprecated *)
|
||||
doc_class assertions =
|
||||
properties :: "term list"
|
||||
|
||||
|
|
|
|||
|
|
@ -1597,21 +1597,18 @@ val docitem_modes = Scan.optional (Args.parens (Args.$$$ defineN || Args.$$$ unc
|
|||
|
||||
|
||||
val docitem_antiquotation_parser = (Scan.lift (docitem_modes -- Args.text_input))
|
||||
: ({define: bool, unchecked: bool} * Input.source) context_parser;
|
||||
|
||||
: ({define:bool,unchecked:bool} * Input.source) context_parser;
|
||||
|
||||
|
||||
fun pretty_docitem_antiquotation_generic cid_decl ctxt ({unchecked = x, define = y}, src ) =
|
||||
let (* val _ = writeln ("ZZZ" ^ Input.source_content src ^ "::2::" ^ cid_decl) *)
|
||||
val (str,pos) = Input.source_content src
|
||||
val _ = check_and_mark ctxt cid_decl
|
||||
({strict_checking = not x}) pos str
|
||||
in
|
||||
(if y then Latex.enclose_block ("\\csname isaDof.label\\endcsname[type={"^cid_decl^"}]{") "}"
|
||||
else Latex.enclose_block ("\\csname isaDof.ref\\endcsname[type={"^cid_decl^"}]{") "}")
|
||||
[Latex.text (Input.source_content src)]
|
||||
end
|
||||
|
||||
let (* val _ = writeln ("ZZZ" ^ Input.source_content src ^ "::2::" ^ cid_decl) *)
|
||||
val (str,pos) = Input.source_content src
|
||||
val _ = check_and_mark ctxt cid_decl ({strict_checking = not x}) pos str
|
||||
in
|
||||
(if y then Latex.enclose_block("\\csname isaDof.label\\endcsname[type={"^cid_decl^"}]{")"}"
|
||||
else Latex.enclose_block("\\csname isaDof.ref\\endcsname[type={"^cid_decl^"}]{") "}")
|
||||
[Latex.text (Input.source_content src)]
|
||||
end
|
||||
|
||||
|
||||
fun docitem_antiquotation bind cid =
|
||||
|
|
@ -1635,18 +1632,14 @@ fun check_and_mark_term ctxt oid =
|
|||
|
||||
|
||||
fun ML_antiquotation_docitem_value (ctxt, toks) =
|
||||
(Scan.lift (Args.cartouche_input)
|
||||
>> (fn inp => (ML_Syntax.atomic o ML_Syntax.print_term)
|
||||
((check_and_mark_term ctxt o fst o Input.source_content) inp)))
|
||||
(ctxt, toks)
|
||||
(Scan.lift (Args.cartouche_input)
|
||||
>> (fn inp => (ML_Syntax.atomic o ML_Syntax.print_term)
|
||||
((check_and_mark_term ctxt o fst o Input.source_content) inp)))
|
||||
(ctxt, toks)
|
||||
|
||||
(* Setup for general docrefs of the global DOF_core.default_cid - class ("text")*)
|
||||
(* Setup for general docitems of the global DOF_core.default_cid - class ("text")*)
|
||||
val _ = Theory.setup
|
||||
(docitem_antiquotation \<^binding>\<open>docref\<close> DOF_core.default_cid #>
|
||||
(* deprecated syntax ^^^^^^*)
|
||||
docitem_antiquotation \<^binding>\<open>docitem_ref\<close> DOF_core.default_cid #>
|
||||
(* deprecated syntax ^^^^^^^^^^^*)
|
||||
docitem_antiquotation \<^binding>\<open>docitem\<close> DOF_core.default_cid #>
|
||||
(docitem_antiquotation \<^binding>\<open>docitem\<close> DOF_core.default_cid #>
|
||||
|
||||
ML_Antiquotation.inline \<^binding>\<open>docitem_value\<close> ML_antiquotation_docitem_value)
|
||||
|
||||
|
|
@ -1654,14 +1647,6 @@ end (* struct *)
|
|||
\<close>
|
||||
|
||||
|
||||
ML\<open>
|
||||
Goal.prove_global;
|
||||
Specification.theorems_cmd;
|
||||
Goal.prove_common;
|
||||
\<close>
|
||||
|
||||
ML\<open>open Proof
|
||||
\<close>
|
||||
|
||||
ML\<open>
|
||||
structure AttributeAccess =
|
||||
|
|
|
|||
|
|
@ -65,7 +65,7 @@ text*[dfgdfg2::C, z = "None"]\<open> Lorem ipsum ... @{thm refl} \<close>
|
|||
|
||||
text*[omega::E, x = "''def''"]\<open> Lorem ipsum ... @{thm refl} \<close>
|
||||
|
||||
text\<open> As mentioned in @{docitem_ref \<open>dfgdfg\<close>} \<close>
|
||||
text\<open> As mentioned in @{docitem \<open>dfgdfg\<close>} \<close>
|
||||
|
||||
text\<open>Here is a simulation what happens on the level of the (HOL)-term representation:\<close>
|
||||
term "A.x (undefined\<lparr>A.x := 3\<rparr>)"
|
||||
|
|
|
|||
Loading…
Reference in New Issue