From 59c6a1304b89542e3dfa912045296a0fe3b6e870 Mon Sep 17 00:00:00 2001 From: "Achim D. Brucker" Date: Thu, 15 Aug 2019 13:45:56 +0100 Subject: [PATCH] Removed outdated stuff that never should have been comitted in the first place. --- .../Isabelle_DOF-Manual/05_IsaDofLaTeX.thy | 107 ------------------ 1 file changed, 107 deletions(-) delete mode 100644 examples/technical_report/Isabelle_DOF-Manual/05_IsaDofLaTeX.thy diff --git a/examples/technical_report/Isabelle_DOF-Manual/05_IsaDofLaTeX.thy b/examples/technical_report/Isabelle_DOF-Manual/05_IsaDofLaTeX.thy deleted file mode 100644 index 6976951c..00000000 --- a/examples/technical_report/Isabelle_DOF-Manual/05_IsaDofLaTeX.thy +++ /dev/null @@ -1,107 +0,0 @@ -(*<*) -theory "05_IsaDofLaTeX" - imports "04_RefMan" -begin -(*>*) - -chapter*[latex::technical,main_author="Some(@{docitem ''adb''}::author)"]\ PDF Generation with \isadof \ - - -section*[latex1::technical]\How to adapt \isadof to a new document style file\ - -text\Current \isadof comes with a number of setups for the PDF generation, notably -Springer LNCS, lipics, ..., as well as setupqs of technical reports this the present one. - -The question arises, what to do if \isadof has to be accoustomed to a new LaTeX style -file configuration in order to generate PDF. -\ -text\ -In theory, this is simple - in practice, the efforts required -depends mostly on two factors: - -\<^item> how compatible is the required LaTeX class with Isabelle's LateX - setup in general (e.g., does it work with an antique version - of \comment.sty\ required by Isabelle) - -\<^item> how much magic does the required LaTeX class wrt the title page - information (author, affiliation). - -\<^item> which ontologies should be supported. While most ontologies are - generic, some only support a very specific subset of LaTeX - templates (classes). For example, \<^theory_text>\scholarly_paper\ does currently - \<^emph>\only\ support \llncs\, \rartcl\, and \lipics\. - -The general process as such is straight-forward: - -\<^enum> From the supported LaTeX classes, try to find the one that is - most similar to the one that you want to support. For the sake - of the this example, let's assume this is llncs -\<^enum> Use the template for this class (llncs) as starting point, i.e., - \<^verbatim>\cp document-generator/document-template/root-lncs.tex - document-generator/document-template/root-eptcs.tex\ - - The mandatory naming scheme for the templates is - - \<^verbatim>\root-.tex\ - - That is to say that \<^verbatim>\\ should be the name of the - new LaTeX class (all lowercase preferred) that will be used - in config files and also will be shown in the help text - shown by executing - - \<^verbatim>\isabelle DOF_mkroot -h\ - -\<^enum> Edit the new template as necessary (using the provided - example from the target class as reference): - - \<^verbatim>\vim document-generator/document-template/root-foo.tex\ - - and do the needful. - -\<^enum> Install the new template: - - \<^verbatim>\./install\ - - (If you have a working installation of the required AFP entries - and the Isabelle/DOF patch, you can use \<^verbatim>\./install -s\ - which will \<^emph>\ONLY\ install the \<^verbatim>\LaTeX styles/templates\, see - \<^verbatim>\./install -h)\ - -\<^enum> Now the new template should be available, you can check this with - - \<^verbatim>\isabelle DOF_mkroot -h\ - -\<^enum> Create an "tiny/empty" Isabelle project using the ontology "core" - and test your template. If everything works, celebrate. If it does - not work, understand what you need to change and continue - with step 3. - - (of course, if the new class is not available in TeXLive, you need - to add them locally to the documents folder of your Isabelle - project and, as usual, it needs to be registered in your ROOTS - file) - -\<^enum> If the ontologies that should be used together with this LaTeX - class do not require specific adaptions (e.g., CENELEC 50128), - everything should work. If one of the required ontology LaTeX - setups only supports a subset of LaTeX classes (e.g., \<^theory_text>\scholarly_paper\ - due to the different setups for authors/affiliations blurb), - you need to develop support for you new class in the ontology - specific LaTeX styles, e.g., - \document-generator/latex/DOF-scholarly_paper.sty\ - (mandatory naming convention: \DOF-.sty\) - -\<^enum> After updating the ontology style (or styles), you need - to install them (again, you might want to use ./install -s) - and test your setup with a paper configuration using - your new LaTeX template and the required styles. In case - of errors, go back to step 7. - -\ - - - -(*<*) -end -(*>*) -