From b1d39bd9ec3e99b831ef2986200d79567aff65b1 Mon Sep 17 00:00:00 2001 From: "Achim D. Brucker" Date: Tue, 6 Mar 2018 09:44:07 +0000 Subject: [PATCH] Added: simple test setup. --- .gitignore | 1 + document-generator/example/DOF_example.thy | 63 ++++++++++++++++++++ document-generator/example/ROOT | 10 ++++ document-generator/example/document/build | 47 +++++++++++++++ document-generator/example/document/root.tex | 55 +++++++++++++++++ 5 files changed, 176 insertions(+) create mode 100644 document-generator/example/DOF_example.thy create mode 100644 document-generator/example/ROOT create mode 100755 document-generator/example/document/build create mode 100644 document-generator/example/document/root.tex diff --git a/.gitignore b/.gitignore index b5046c1..1e3ccba 100644 --- a/.gitignore +++ b/.gitignore @@ -1 +1,2 @@ document-generator/converter/bin/*.jar +output diff --git a/document-generator/example/DOF_example.thy b/document-generator/example/DOF_example.thy new file mode 100644 index 0000000..db567da --- /dev/null +++ b/document-generator/example/DOF_example.thy @@ -0,0 +1,63 @@ +theory DOF_example + imports "../../CENELEC_50126" +begin + +section{* Some show-off's of general antiquotations. *} + + +(* some show-off of standard anti-quotations: *) +text{* @{thm refl} + @{file "../../Isa_DOF.thy"} + @{value "3+4::int"} + @{const hd} + @{theory List} + @{term "3"} + @{type bool} + @{term [show_types] "f x = a + x"} *} + + + +section{* Some Tests for Ontology Framework and its CENELEC Instance *} + +declare_reference [lalala::requirement, alpha="main", beta=42] + +(* +declare_reference [lalala::quod] (* shouldn't work *) +*) + +declare_reference [blablabla::cid, alpha=beta, beta=gamma] + +paragraph*[sdf]{* just a paragraph *} +(* +subsection*[sdf]{* shouldn't work, multiple ref. *} +*) +section*[sedf::requirement]{* works again. One can hover over the class constraint and + jump to its definition. *} +text\\label{sedf}\ (* Hack to make the LaTeX-ing running. Should disappear. *) + +section*[seedf::test_case, dfg=34,fgdfg=zf]{* and another example with attribute setting, +but wrong doc_class constraint. *} + +section{* Text Antiquotation Infrastructure ... *} + +text{* @{docref \lalala\} -- produces warning. *} + +text{* @{docref \ass122\} -- global reference to a text-item in another file. *} + +text{* @{ec \ass122\} -- global reference to a exported constraint in another file. + Note that the link is actually a srac, which, according to + the ontology, happens to be an "ec". *} + +(* +text{* @{test_specification \ass122\} -- wrong: "reference ontologically inconsistent". *} +*) + + +text{* Here is a reference to @{docref \sedf\} *} +(* works currently only in connection with the above label-hack. + Try to hover over the sedf - link and activate it !!! *) + + +end + + diff --git a/document-generator/example/ROOT b/document-generator/example/ROOT new file mode 100644 index 0000000..81d00ad --- /dev/null +++ b/document-generator/example/ROOT @@ -0,0 +1,10 @@ +session "DOF_example" = "HOL" + + options [document = pdf, document_output = "output"] + theories [document = false] + (* Foo *) + (* Bar *) + theories + DOF_example + document_files + "root.tex" + "build" diff --git a/document-generator/example/document/build b/document-generator/example/document/build new file mode 100755 index 0000000..b3dfd8b --- /dev/null +++ b/document-generator/example/document/build @@ -0,0 +1,47 @@ +#!/usr/bin/env bash +# Copyright (c) 2018 The University of Sheffield. All rights reserved. +# 2018 The University of Paris-Sud. All rights reserved. +# +# Redistribution and use in source and binary forms, with or without +# modification, are permitted provided that the following conditions +# are met: +# 1. Redistributions of source code must retain the above copyright +# notice, this list of conditions and the following disclaimer. +# 2. Redistributions in binary form must reproduce the above copyright +# notice, this list of conditions and the following disclaimer in +# the documentation and/or other materials provided with the +# distribution. +# THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS +# "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT +# LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS +# FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE +# COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, +# INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, +# BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; +# LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER +# CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT +# LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN +# ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE +# POSSIBILITY OF SUCH DAMAGE. +# +# SPDX-License-Identifier: BSD-2-Clause + +OUTFORMAT=${1:-pdf} +NAME=${2:-root} + +set -e + +ROOT_NAME="root_$NAME" +[ ! -f "$DIR/$ROOT_NAME.tex" ] && ROOT_NAME="root" + +$ISABELLE_TOOL scala $ISABELLE_HOME_USER/DOF/lib/dof_latex_converter.jar . + +cp $ISABELLE_HOME_USER/DOF/latex/DOF.sty . + +$ISABELLE_TOOL latex -o sty "$ROOT_NAME.tex" && \ +$ISABELLE_TOOL latex -o "$OUTFORMAT" "$ROOT_NAME.tex" && \ +{ [ ! -f "$ROOT_NAME.bib" ] || $ISABELLE_TOOL latex -o bbl "$ROOT_NAME.tex"; } && \ +{ [ ! -f "$ROOT_NAME.idx" ] || $ISABELLE_TOOL latex -o idx "$ROOT_NAME.tex"; } && \ +$ISABELLE_TOOL latex -o "$OUTFORMAT" "$ROOT_NAME.tex" && \ +$ISABELLE_TOOL latex -o "$OUTFORMAT" "$ROOT_NAME.tex" + diff --git a/document-generator/example/document/root.tex b/document-generator/example/document/root.tex new file mode 100644 index 0000000..439383a --- /dev/null +++ b/document-generator/example/document/root.tex @@ -0,0 +1,55 @@ +\RequirePackage{ifvtex} +\documentclass[fontsize=10pt,DIV12,paper=a4,open=right,twoside,abstract=true]{scrreprt} +\usepackage{fixltx2e} +\usepackage[T1]{fontenc} +\usepackage[utf8]{inputenc} +\usepackage{textcomp} +\usepackage[english]{babel} +\usepackage{isabelle} +\usepackage{DOF} +\usepackage{isabellesym} +\usepackage{amsmath} +\usepackage{amssymb} +\usepackage[numbers, sort&compress, sectionbib]{natbib} +\usepackage{hyperref} +\setcounter{tocdepth}{3} +\hypersetup{% + bookmarksdepth=3 + ,pdfpagelabels + ,pageanchor=false + ,bookmarksnumbered + ,plainpages=false +} % more detailed digital TOC (aka bookmarks) +\sloppy +\allowdisplaybreaks[4] +\urlstyle{rm} +\isabellestyle{it} +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +%%% Overrides the (rightfully issued) warning by Koma Script that \rm +%%% etc. should not be used (they are deprecated since more than a +%%% decade) + \DeclareOldFontCommand{\rm}{\normalfont\rmfamily}{\mathrm} + \DeclareOldFontCommand{\sf}{\normalfont\sffamily}{\mathsf} + \DeclareOldFontCommand{\tt}{\normalfont\ttfamily}{\mathtt} + \DeclareOldFontCommand{\bf}{\normalfont\bfseries}{\mathbf} + \DeclareOldFontCommand{\it}{\normalfont\itshape}{\mathit} +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + + +\title{DOF-example} +\author{By brucker} +\begin{document} +\maketitle +\tableofcontents +\input{session} +% optional bibliography +\IfFileExists{root.bib}{% + \bibliographystyle{abbrvnat} + \bibliography{root} +}{} +\end{document} + +%%% Local Variables: +%%% mode: latex +%%% TeX-master: t +%%% End: