From aa3cdfe65ea69d1c2e16185dce46f9ef4e284490 Mon Sep 17 00:00:00 2001 From: bu Date: Tue, 8 Jan 2019 14:44:43 +0100 Subject: [PATCH] Added 2 missing chapters of Impl paper in IsaDof_Manual. New chapters load under jedit, but do not tex. build succeedsm though, since these parts are not included --- .../IsaDof_Manual/04_IsaDofImpl.thy | 189 ++++++++ .../IsaDof_Manual/05_DesignImpl.thy | 421 ++++++++++++++++++ .../{04_Conclusion.thy => 06_Conclusion.thy} | 3 +- .../IsaDof_Manual/IsaDofManual.thy | 4 +- 4 files changed, 614 insertions(+), 3 deletions(-) create mode 100644 examples/technical_report/IsaDof_Manual/04_IsaDofImpl.thy create mode 100644 examples/technical_report/IsaDof_Manual/05_DesignImpl.thy rename examples/technical_report/IsaDof_Manual/{04_Conclusion.thy => 06_Conclusion.thy} (98%) diff --git a/examples/technical_report/IsaDof_Manual/04_IsaDofImpl.thy b/examples/technical_report/IsaDof_Manual/04_IsaDofImpl.thy new file mode 100644 index 00000000..1aacde8d --- /dev/null +++ b/examples/technical_report/IsaDof_Manual/04_IsaDofImpl.thy @@ -0,0 +1,189 @@ +(*<*) +theory "04_IsaDofImpl" + imports "02_Background" +begin +(*>*) + + +chapter*[impl1::introduction,main_author="Some(@{docitem ''adb''}::author)"] + \Isabelle Ontology Framework \isadof\ +text\ +In this section, we introduce our framework, called \isadof. \isadof +is based on several design-decisions: +\begin{compactitem} +\item the entire \isadof is conceived as ``pure add-on'', \ie, we + deliberately resign on the possibility to modify Isabelle itself + (thus accepting a minor loss in performance and some additional + complexity in the documentation generation process) +\item we decided to identify the ontology types with the Isabelle/HOL + type system, \ie, we reuse the same infrastructure for parsers and + type-checkers, but use the types on the meta-level of the document + structure +\item we decided to make the markup-generation by own means in order + to adapt it as good as possible to the needs of tracking the linking + in documents. +\end{compactitem} +\ + + +subsection*["sec:plugins"::technical]{*Writing \isadof as User-Defined Plugin in Isabelle/Isar*} +text\ +Writing an own plugin in Isabelle starts with defining the local data +and registering it in the framework. As mentioned before, contexts +are structures with independent cells/compartments having three +primitives \inlinesml+init+, \inlinesml+extend+ and +\inlinesml+merge+. Technically this is done by instantiating a functor +\inlinesml+Generic_Data+, and the following fairly typical +code-fragment is already drawn from \isadof: +\begin{sml} + structure Data = Generic_Data + ( type T = docobj_tab * docclass_tab + val empty = (initial_docobj_tab, initial_docclass_tab) + val extend = I + fun merge((d1,c1),(d2,c2)) = (merge_docobj_tab (d1, d2), + merge_docclass_tab(c1,c2)) + ); +\end{sml} +with some tables \inlinesml+docobj_tab+ and \inlinesml+docclass_tab+ +(not explained here) capturing the specific data of the application in +mind, \ie, a table of document classes and another one capturing the +document class instances. +\enlargethispage{2\baselineskip} +\ +text\ +All the text samples shown here have to be in the context of an SML +file or in an \inlineisar|ML{* ... *}| command inside a \verb|.thy| +file, which has the effect to type-check and compile these text +elements by the underlying SML compiler. +\ +text\ +Operations are organized in a model-view-controller scheme, where +Isabelle/Isar provides the controller part. A typical model operation +has the type:\ +text\ +\begin{sml} + val opn :: -> Context.generic -> Context.generic +\end{sml} +\ie, it represents a transformation on contexts. For example, the +operation of declaring a local reference in the context is presented +as follows: +\begin{sml} + fun declare_object_local oid ctxt = + let fun decl {tab,maxano} = {tab=Symtab.update_new(oid,NONE) tab, + maxano=maxano} + in (Data.map(apfst decl)(ctxt) + handle Symtab.DUP _ => + error("multiple declaration of document reference")) + end +\end{sml} +\ +text\ +where \inlineisar+Data.map+ is the update function resulting from the +above functor instantiation. This code fragment uses operations from +a library structure \inlinesml+Symtab+ that were used to update the +appropriate table for document objects in the plugin-local +state. Possible exceptions to the update operation were mapped to a +system-global error reporting function. +\ +text\ +Finally, the view-aspects where handled by an API for +parsing-combinators. The library structure \inlinesml+Scan+ provides, +for example, the operators: +\begin{sml} + op || : ('a -> 'b) * ('a -> 'b) -> 'a -> 'b + op -- : ('a -> 'b * 'c) * ('c -> 'd * 'e) -> 'a -> ('b * 'd) * 'e + op |-- : ('a -> 'b * 'c) * ('c -> 'd * 'e) -> 'a -> 'd * 'e + op --| : ('a -> 'b * 'c) * ('c -> 'd * 'e) -> 'a -> 'b * 'e + op >> : ('a -> 'b * 'c) * ('b -> 'd) -> 'a -> 'd * 'c + op option : ('a -> 'b * 'a) -> 'a -> 'b option * 'a + op repeat : ('a -> 'b * 'a) -> 'a -> 'b list * 'a +\end{sml} +for alternative, sequence, sequence-ignore-left, +sequence-ignore-right, and piping, as well as combinators for option +and repeat. The parsing combinator technology arrived meanwhile even +in mainstream languages such as Java or Scala and is nowadays +sufficiently efficient implemented to replace conventional Lex-Yacc +technology for most applications. It has the advantage to be +smoothlessly integrated into standard programs and allows for dynamic +grammar extensions. There is a more high-level structure +\inlinesml{Parse} providing specific combinators for the +command-language Isar: +\begin{sml} + val attribute = Parse.position Parse.name + -- Scan.optional (Parse.$$$ "=" |-- Parse.!!! Parse.name) ""; + val reference = Parse.position Parse.name + -- Scan.option (Parse.$$$ "::" |-- Parse.!!! + (Parse.position Parse.name)); + val attributes = (Parse.$$$ "[" |-- (reference + -- (Scan.optional(Parse.$$$ "," + |-- (Parse.enum "," attribute))) [])) + --| Parse.$$$ "]" +\end{sml} +``Model'' and ``View'' parts were combined to ``parsers'' which were +registered in the interpreter toplevel of the Isabelle/Isar framework: +\begin{sml} + val _ = Outer_Syntax.command @ {command_keyword "declare_reference"} + "declare document reference" + (attributes >> (fn (((oid,pos),cid),doc_attrs) => + (Toplevel.theory (DOF_core.declare_object_global oid)))); +\end{sml} +\ +text\ +Altogether, this gives the \emph{extension} of the Isar syntax +allowing to parse and interpret the new \emph{command} in a subsequent +\verb+.thy+ file: +\begin{isar} +declare_reference [lal::requirement, alpha="main", beta=42] +\end{isar} +where we ignore the semantics at the moment. The construction also +generates implicitely some markup information; for example, when +hovering over the \inlineisar|declare_reference| command in a +front-end supporting PIDE, a popup window with the text: ``declare +document reference'' will appear. +\ + +subsection*["sec:prog_anti"::technical]{*Programming Text Antiquotations*} +text\ +As mentioned in the introduction, Isabelle/Isar is configured with a +number of standard commands to annotate formal definitions and proofs +with text---the latter is used in particular to generate PDF and HTML +documents with internal hypertext-references. Inside these text +commands, a number of predefined antiquotations can be inserted which +were checked and decorated with markup during editing. +\ +text\ +Moreover, there is an API for user-defined antiquotations. It follows +the lines of the MVC style system extensions presented in the previous +section. An excerpt of the table defining some antiquotations can be +found in \verb+thy_output.ML+ of the Isabelle sources and give the +basic idea: +\begin{sml} + val _ = Theory.setup + (basic_entity @ {binding term} (stp -- Args.term) pretty_term_style #> + basic_entity @ {binding prop} (stp -- Args.prop) pretty_term_style #> + ... ) +\end{sml} +where \inlinesml+stp+ (=\inlinesml+Term_Style.parse+), +\inlinesml+Args.term+ and \inlinesml+Args.prop+ are parsing +combinators from higher Isar-API's (that actually do the type checking +in the surrounding HOL context) and \inlinesml+pretty_term_style+ an +operation pretty-printing the parsed term for one of the possible +targets HTML or \LaTeX{} (converted to \verb+.pdf+ in a +post-compilation process). The construct \inlinesml+@ {binding term}+ +decorates the keyword ``term'' with positioning markup (allowing +navigating to this defining place in \verb+thy_output.ML+ by +hyperlinking) and \inlinesml+Theory.setup+ the operator that +registers the entire parser/checker into the Isar framework. +\ +text\ +Together, this establishes the syntax and semantics of, for example, +the antiquotation: +\begin{isar} +text{* @{term "fac 5"} *} +\end{isar} +inside the text command. A key contribution of this paper is that such +SML code is generated \emph{automatically} from an \isadof ontology +definition introduced in the subsequent section. +\ + +end \ No newline at end of file diff --git a/examples/technical_report/IsaDof_Manual/05_DesignImpl.thy b/examples/technical_report/IsaDof_Manual/05_DesignImpl.thy new file mode 100644 index 00000000..f67a1e1f --- /dev/null +++ b/examples/technical_report/IsaDof_Manual/05_DesignImpl.thy @@ -0,0 +1,421 @@ +(*<*) +theory "05_DesignImpl" + imports "04_isaDofImpl" +begin +(*>*) + +chapter*[impl2::technical,main_author="Some(@{docitem ''bu''}::author)"] + {* \isadof: Design and Implementation*} +text\ +In this section, we present the design and implementation of \isadof. +\subsection{Document Ontology Modeling with \isadof} +First, we introduce an own language to define ontologies. +Conceptually, ontologies consist of: +\begin{compactitem} +\item a \emph{document class} that describes a concept, \ie, it + represents set of \emph{instances} of a document class, + i.e. references to document elements; +\item \emph{attributes} specific to document classes; +\item attributes should be typed (arbitrary HOL-types); +\item attributes can refer to other document classes, + thus, document classes must also be HOL-types + (Such attributes were called \emph{links}); +\item a special link, the reference to a super-class, + establishes an \emph{is-a} relation between classes; +\item classes may refer to other classes via a regular expression in a + \emph{where} clause (classes with such an optional where clauses are + called \emph{monitor classes}); +\item attributes may have default values in order to facilitate notation. +\end{compactitem} +\ +text\ + +For ontology modeling, we chose a syntax roughly similar to +Isabelle/HOL's extensible records. We present the syntax implicitly +by a conceptual example, that serves to introduce the key-features of +the modeling language: +\begin{isar} +doc_class A = + x :: "string" + +doc_class B = + y :: "string list" <= "[]" + +doc_class C = B + + z :: "A option" <= "None" + +datatype enum = "X1" | "X2" | "X3 + +doc_class D = B + + a1 :: enum <= "X2" + a2 :: int <= "0" + +doc_class F = + r :: "thm list" + b :: "(A \ B) set" <= "{}" + +doc_class M = + trace :: "(A + C + D + F) list" + where "A . (C | D)* . [F]" +\end{isar} +Isabelle uses a two level syntax: the \emph{outer syntax} which is +defined and extended using the mechanisms described in +\autoref{sec:plugins} and the \emph{inner syntax}, is used to define +type and term expressions of the Isabelle framework. Since we reuse a +lot of infrastructure of HOL (with respect to basic type library +definitions), parsing and type-checking have been specialized to HOL +and extensions thereof. The ``switch'' between outer and inner syntax +happens with the quote symbols +\inlineisar+"..."+. % In exceptional cases, the latter can be +% omitted --- notably, if the type or term consists only of one type +% constructor symbol or constant symbol respectively. +% +\ +text\ +The above ontology specification contains the document classes +\inlineisar+A+, \inlineisar+B+, \inlineisar+C+, \inlineisar+D+, +\inlineisar+F+, and \inlineisar+M+ with the respective attributes +\inlineisar+x+, \inlineisar+y+, \inlineisar+z+, \inlineisar+a1+, +\inlineisar+a2+, \inlineisar+b+ and \inlineisar+trace+. +\inlineisar+C+ and \inlineisar+D+ is are sub-classes from +\inlineisar+B+ as states the class extension \inlineisar*B + ... *. + +\enlargethispage{2\baselineskip} +\ +text\ +Each attribute is typed within the given context; the general HOL +library provides the types \inlineisar+string+, \inlineisar+_ list+, +\inlineisar+_ option+, and \inlineisar+_ set+. On the fly, other +special purpose types can be defined. We reuse here the Isabelle/HOL +\inlineisar+datatype+-statement, which can be mixed arbitrarily in +between the ontology definitions (like any other Isabelle/HOL command) +to define an enumeration type. Document classes---similar to +conventional class-definitions as in object-oriented +programming---\emph{induce} an implicit HOL type; for this reason the +class \inlineisar+C+ can have an attribute that refers to the +\inlineisar+A+ attribute classes. Document classes that contain +attributes referring to induced class types are called +\emph{links}. Links can be complex: the class \inlineisar+F+, for +example, contains a set of pairs, \ie, a relation between +\inlineisar+A+ and \inlineisar+B+ document instances. Each attribute +may be assigned (via \inlineisar+<=+) to a default value represented +by a HOL expression, whose syntax is either defined by library +operations or constant declarations like the +\inlineisar+datatype+-statement. +\ +text\ +The document class \inlineisar+M+ is a \emph{monitor class}, \ie, a +class possessing a \inlineisar+where+ clause containing a regular +expression consisting of the class identifier \inlineisar+A+, +\inlineisar+B+, etc. Its use is discussed in \autoref{sec:monitor-class}. +\ + +subsection*[editing::example]{*Editing a Document with Ontology-Conform Meta-Data*} +text\ +As already mentioned, Isabelle/Isar comes with a number of standard +\emph{text commands} such as \inlineisar+section{* ... *}+ or +\inlineisar+text{* ... *}+ that offer the usual text structuring +primitives for documents. From the user point-of-view, text commands +offer the facility of spell-checking and IDE support for text +antiquotations (as discussed before), from a system point of view, +they are particular since they are not conceived to have side effects +on the global (formal) context, which is exploited in Isabelle's +parallel execution engine.\ + +text\ +\isadof introduces an own family of text-commands based on the +standard command API of the Isar engine, which allows having +side effects of the global context and thus to store and manage own +meta-information (the standard text-command interface turned out not +to be flexible enough, and a change of this API conflicts with our +goal of not changing Isabelle itself). \isadof, \eg, provides +\inlineisar+section*[]{* ... *}+, +\inlineisar+subsection*[]{* ... *}+, +or \inlineisar+text*[]{* ... *}+, where +\inlineisar++ is a syntax to declaring instance, class and +attributes for this text element. The syntax for +\inlineisar++ follows the scheme: +\begin{isar} + :: , attr_1 = "", ..., attr_n = "" +\end{isar} +where the \inlineisar++ can be optionally omitted which represents +the implicit superclass \inlineisar+text+, where \inlineisar+attr_i+ must +be declared attributes in the class and where the \inlineisar+""+ +must have the corresponding type. Attributes from a class definition may +be left undefined; definitions of attribute values \emph{override} default +values or values of super-classes. Overloading of attributes, however, is not +permitted in \isadof. \ + +text\ +We can annotate a text as follows. First, we have to place a +particular document into the context of our conceptual example +ontology shown above: +\begin{isar} +theory Concept_Example + imports "../../ontologies/Conceptual" +begin +\end{isar} +which is contained contained a theory file +\verb+../../ontologies/Conceptual.thy+. Then we can continue to annotate +our text as follows: +\begin{isar} + section*[a::A, x = "''alpha''"] {* Lorem ipsum dolor sit amet, ... *} + + text*[c1::C, x = "''beta''"] + {* ... suspendisse non arcu malesuada mollis, nibh morbi, ... *} + + text*[d:D, a2="10"]{* Lorem ipsum dolor sit amet, consetetur ...*} +\end{isar}\ + +text\ +Let's consider the last line: +this text is the instance \inlineisar+d+ which belongs to class +\inlineisar+D+, and the default of its attribute \inlineisar+a2+ is +overridden to the value \inlineisar+"10"+. Instances are mutable in +\isadof, the subsequent \isadof command: +\begin{isar} + update_instance*[d::D, a1 := X2, a2 := "20"] +\end{isar} +This changes the attribute values of \verb+d+. The typing +annotation \verb+D+ is optional here (if present, it is checked).\ + +text\ +Document instances were used to reference textual content; in the +generated \LaTeX{} (PDF) and HTML documents they were supported by +hyperlinks. Since Isabelle/Isar has a top-down evaluation and +validation strategy for the global document, a kind of forward +declaration for references is sometimes necessary. +\begin{isar} + declare_reference* [] +\end{isar} +This declares the existence of a text-element and allows for +referencing it, although the actual text-element will occur later in +the document.\ + + +subsection*[ontolinks::technical]{*Ontology-Conform Logical Links: \isadof Antiquotations*} +text\ +Up to this point, the world of the formal and the informal document +parts are strictly separated. The main objective of \isadof are ways +to establish machine-checked links between these two universes by +instantiating automatically Isabelle/Isar's concept of +\emph{antiquoations}. The simplest form of link appears in the +following command: +\begin{isar} + text{* ... in ut tortor ... @ {docitem_ref {*a*}} ... @ {A {*a*}}*} +\end{isar}\ +text\ +This standard text-command contains two \isadof antiquotations; the +first represents just a link to the text-element \inlineisar$a$. +The second contains additionally the implicit constraint that the +reference to \inlineisar$a$ must also belong to the +\inlineisar$A$-class; the following input: +\begin{isar} + text{* ... ... ... @ {C (*a*}}*} +\end{isar} +results in the detection of an ontological inconsistency which will be +reported in PIDE at editing time. Of course, any modification of the +ontology or changes in the labeling of the meta-information will lead +to the usual re-checking of the Isabelle/Isar engine. A natural +representation of these semantic links inside \isadof documents would +be hyperlinks in generated PDF or HTML files. +\enlargethispage{2\baselineskip}\ + +text\ +Besides text antiquotations from Isabelle/Isar, we introduced a novel +concept that we call \emph{inner syntax antiquotations}. It is a +crucial technical feature for establishing links between text-items as +well as document meta-data and formal entities of Isabelle such as +types, terms and theorems (reflecting the fundamental types +\inlineisar+typ+, \inlineisar+term+ and \inlineisar+thm+ of the +Isabelle kernel.) We start with a slightly simpler case is the +establishment of links between text-elements: +\begin{isar} +section*[f::F] {* Lectus accumsan velit ultrices, ... }*} + +update_instance*[f,b:="{(@ {docitem ''a''}::A,@ {docitem ''c1''}::C), + (@ {docitem ''a''},@ {docitem ''c1''})}"] +\end{isar}\ + +text\ + +This example shows the construction of a relation between text +elements \emph{inside} HOL-expressions with the usual syntactic and +semantic machinery for sets, pairs, (thus: relations). Inside the +world of HOL-terms, we can refer to items of the ``meta-world'' by a +particular form of antiquotations called \emph{inner syntax + antiquotations}. Similarly, but conceptually different, it is +possible to refer in \isadof HOL-expressions to theorems of the +preceding context. Thus, it is possible to establish a theorem (or a +type or term), in the example below, by a proof ellipse in Isabelle: +\begin{isar} + theorem some_proof : "P" sorry + + update_instance*[f,r:="[@ {thm ''some_proof''}]"] +\end{isar}\ +text\ +The resulting theorem is stored in a theorem list as part of the +meta-information of a section. Technically, theorems were introduced +in \isadof as abstract HOL types and some unspecified (Skolem) +HOL-constants with a particular infix-syntax. They are introduced for +example by: +\begin{isar} + typedecl "thm" + consts mk_thm :: "string \ thm" ("@{thm _}") +\end{isar} +which introduces a new type \inlineisar+thm+ reflecting the internal +Isabelle type for established logical facts and the above notation to +the inner syntax parser. The \inlineisar+doc_class F+ in our schematic +example uses already this type. Whenever these expressions occur +inside an inner-syntax HOL-term, they are checked by the HOL parser +and type-checker as well as an \isadof checker that establishes that +\inlineisar+some_proof+ indeed refers to a known theorem of this name +in the current context. +% (this is, actually, the symmetry axiom of the equality in HOL). +To our knowledge, this is the first ontology-driven framework for +editing mathematical and technical documents that focuses particularly +on documents mixing formal and informal content---a type of documents +that is very common in technical certification processes. We see +mainly one area of related works: IDEs and text editors that support +editing and checking of documents based on an ontology. There is a +large group of ontology editors (\eg, Prot{\'e}g{\'e}~\cite{protege}, +Fluent Editor~\cite{cognitum}, NeOn~\cite{neon}, or +OWLGrEd~\cite{owlgred}). With them, we share the support for defining +ontologies as well as auto-completion when editing documents based on +an ontology. While our ontology definitions are, currently, based on a +textual definition, widely used ontology editors (\eg, +OWLGrEd~\cite{owlgred}) also support graphical notations. This could +be added to \isadof in the future. A unique feature of \isadof is the +deep integration of formal and informal text parts. The only other +work in this area wea are aware of is rOntorium~\cite{rontorium}, a plugin +for Prot{\'e}g{\'e} that integrates R~\cite{adler:r:2010} into an +ontology environment. Here, the main motivation behind this +integration is to allow for statistically analyze ontological +documents. Thus, this is complementary to our work.\ + +text\ +There is another form of antiquotations, so-called ML-antiquotations +in Isabelle, which we do not describe in detail in this paper. With +this specific antiquotations, it is possible to refer to the HOL-term +of all the attributes of the doc-item; by writing specific ML-code, +arbitrary user-defined criteria can be implemented establishing that +all meta-data of a document satisfies a particular validation. For +example, in the context of an ontology for scientific papers, we could +enforce that terms or theorems have a particular form or correspond to +``claims'' (contributions) listed in the introduction of the paper. +\ + +subsection*["sec:monitor-class"::technical]{*Monitor Document Classes*} +text\ +\autoref{lst:example} shows our conceptual running example in all +details. While inheritance on document classes allows for structuring +meta-data in an object-oriented manner, monitor classes such as +\inlineisar+M+ impose a structural relation on a document. The +\inlineisar+where+ clause permits to write a regular expression on +class names; the class names mentioned in the where clause are called +the ``controlled'' ones. The expression specifies that all +text-elements that are instances of controlled classes to occur in the +sequential order specified by the \inlineisar+where+-clause. Start and +end were marked by the corresponding monitor commands. Note that +monitors may be nested. +\ +text\ +\begin{isar}[float, caption={Our running example},label={lst:example}] + theory Concept_Example + imports "../../ontologies/Conceptual" + begin + + open_monitor*[struct::M] + + section*[a::A, x = "''alpha''"] {* Lorem ipsum dolor sit amet, ... *} + + text*[c1::C, x = "''beta''"] + {* ... suspendisse non arcu malesuada mollis, nibh morbi, ... *} + + text*[d::D, a1 = "X3"] + {* ... phasellus amet id massa nunc, pede suscipit repellendus, ... *} + + text*[c2::C, x = "''delta''"] + {* ... in ut tortor eleifend augue pretium consectetuer. *} + + section*[f::F] {* Lectus accumsan velit ultrices, ... @ {docitem_ref {*a*} }*} + + theorem some_proof : "P" sorry + + update_instance*[f,r:="[@ {thm ''some_proof''}]"] + + text{* ..., mauris amet, id elit aliquam aptent id, ... *} + + update_instance*[f,b:="{(@ {docitem ''a''}::A,@ {docitem ''c1''}::C), + (@ {docitem ''a''}, @ {docitem ''c1''})}"] + + close_monitor*[struct] +\end{isar} +\ + +section{*Document Generation*} +text\ +Up to know, we discussed the definition of ontologies and their +representation in an interactive development environment, \ie, +JEdit/PIDE. In many application areas, it is desirable to also +generate a ``static'' document, \eg, for long-term archiving. Isabelle +supports the generation of both HTML and PDF documents. Due to its +standardization, the latter (in particular in the variant PDF/A) is +particularly suitable for ensuring long-term access. Hence, our +prototype focuses currently on the generation of consistent PDF +documents.\ + +text\ +Technically, the PDF generation is based on \LaTeX{} (this is mostly +hidden from the end users) as standard text formatting such as +itemize-lists or italic and bold fonts can be written in JEdit without +in a ``what-you-see-is-what-you-get''-style. We extended the \LaTeX{} +generation of Isabelle in such a way that for each ontological concept +that is formally defined in \isadof, is mapped to a dedicated +\LaTeX-command. This \LaTeX-command is responsible for the actual +typesetting of the concept as well as for generating the necessary +label and references. For each defined ontology, we need to define a +\LaTeX-style that defines these commands. For the standard commands +such as \inlineisar|section*[...]{* ... *}|, default implementations +are provided by \isadof. For example, the following is the \LaTeX{} +definition for processing \inlineisar|section*[...]{* ... *}|: +\begin{ltx} +\newkeycommand\isaDofSection[reference=,class_id=][1]{% + \isamarkupsection{#1}\label{\commandkey{reference}}% +} +\end{ltx}\ +text\ +This command gets all meta-arguments of the concepts a swell as the +actual arguments. The layout is delegated to Isabelle's standard +sectioning commands +(\inlineltx|\isamarkupsection{#1}|). Additionally, a label for +linking to this section is generated. +\enlargethispage{2\baselineskip} +\ +text\ +Considering an ontology defining the concepts for writing scientific +papers, a potential definition for typesetting abstracts (where an +abstract includes a list of keywords) is: +\begin{ltx} +\newkeycommand\isaDofTextAbstract[reference=,class_id=,keywordlist=][1]{% + \begin{isamarkuptext}% + \begin{abstract}\label{\commandkey{reference}}% + #1 + + \ifthenelse{\equal{\commandkey{keywordlist}}{}}{}{% + \medskip\noindent{\textbf{Keywords:}} \commandkey{keywordlist}% + } + \end{abstract}% + \end{isamarkuptext}% +} +\end{ltx} +Our generated \LaTeX{} is conceptually very close +SALT~\cite{DBLP:conf/esws/GrozaHMD07}--- but instead of writing +\LaTeX{} manually it is automatically generated and, additionally, can +also guarantee the consistency of the formal (mathematical/logical) +content. +\ + +(*<*) +end +(*>*) diff --git a/examples/technical_report/IsaDof_Manual/04_Conclusion.thy b/examples/technical_report/IsaDof_Manual/06_Conclusion.thy similarity index 98% rename from examples/technical_report/IsaDof_Manual/04_Conclusion.thy rename to examples/technical_report/IsaDof_Manual/06_Conclusion.thy index a5a6d3e0..5eebccbb 100644 --- a/examples/technical_report/IsaDof_Manual/04_Conclusion.thy +++ b/examples/technical_report/IsaDof_Manual/06_Conclusion.thy @@ -1,6 +1,7 @@ (*<*) -theory "04_Conclusion" +theory "06_Conclusion" imports "03_IsaDof" + (* imports "05_DesignImpl *) begin (*>*) diff --git a/examples/technical_report/IsaDof_Manual/IsaDofManual.thy b/examples/technical_report/IsaDof_Manual/IsaDofManual.thy index 4faaec9b..fc19a954 100644 --- a/examples/technical_report/IsaDof_Manual/IsaDofManual.thy +++ b/examples/technical_report/IsaDof_Manual/IsaDofManual.thy @@ -1,10 +1,10 @@ (*<*) theory IsaDofManual - imports "04_Conclusion" + imports "06_Conclusion" begin (*<*) -text*[bib::bibliography]\TODO\ +text*[bib::bibliography]\References\ close_monitor*[this]