From 13a92fcf34e1ecb36043745f1c2c3bbf93f5d13c Mon Sep 17 00:00:00 2001 From: "Achim D. Brucker" Date: Wed, 14 Aug 2019 20:04:37 +0100 Subject: [PATCH] Minor layout improvements. --- .../Isabelle_DOF-Manual/03_GuidedTour.thy | 9 +++---- .../Isabelle_DOF-Manual/04_RefMan.thy | 25 +++++++++---------- 2 files changed, 16 insertions(+), 18 deletions(-) diff --git a/examples/technical_report/Isabelle_DOF-Manual/03_GuidedTour.thy b/examples/technical_report/Isabelle_DOF-Manual/03_GuidedTour.thy index c47d0e7..50b75b6 100644 --- a/examples/technical_report/Isabelle_DOF-Manual/03_GuidedTour.thy +++ b/examples/technical_report/Isabelle_DOF-Manual/03_GuidedTour.thy @@ -55,7 +55,7 @@ in your \inlinebash|PATH|, you will need to invoke \inlinebash|isabelle| using i full qualified path, \eg: \begin{bash} -ë\prompt{}ë /usr/local/Isabelleë\isabelleversionë/bin/isabelle version +ë\prompt{}ë /usr/local/Isabelleë\isabelleversion/ëbin/isabelle version ë\isabellefullversionë \end{bash} \ @@ -75,11 +75,9 @@ text\ \begin{bash} ë\prompt{}ë pdftex \\expanded{Success}\\end -This is pdfTeX, Version 3.14159265-2.6-1.40.20 (TeX Live 2019/Debian) (preloaded format=pdftex) - restricted \write18 enabled. +This is pdfTeX, Version 3.14159265-2.6-1.40.20 (TeX Live 2019/Debian). entering extended mode -[1{/var/lib/texmf/fonts/map/pdftex/updmap/pdftex.map}] +[1{dftex.map}] Output written on texput.pdf (1 page, 8650 bytes). Transcript written on texput.log. \end{bash} @@ -113,6 +111,7 @@ If the \inlinebash|isabelle| tool is not in your \inlinebash|PATH|, you need to \inlinebash|install| script with the \inlinebash|--isabelle| option, passing the full-qualified path of the \inlinebash|isabelle| tool (\inlinebash|install --help| gives you an overview of all available configuration options): +\clearpage \begin{bash} ë\prompt{}ë cd ë\isadofdirnë diff --git a/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy b/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy index 7bd3ef3..ae46671 100644 --- a/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy +++ b/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy @@ -215,7 +215,8 @@ text\ with the syntactic category of \name\'s we refer to alpha-numerical identifiers (called \short_id\'s in @{cite "wenzel:isabelle-isar:2019"}) and identifiers in \inlineisar+" ... "+ which might contain certain ``quasi-letters'' such - as \inlineisar+_+, \inlineisar+-+, \inlineisar+.+. See~@{cite "wenzel:isabelle-isar:2019"} for details. + as \inlineisar+_+, \inlineisar+-+, \inlineisar+.+ (see~@{cite "wenzel:isabelle-isar:2019"} for + details). \<^item> \tyargs\:\index{tyargs@\tyargs\} \<^rail>\ typefree | ('(' (typefree * ',') ')')\ \typefree\ denotes fixed type variable(\'a\, \'b\, ...) (see~@{cite "wenzel:isabelle-isar:2019"}) @@ -280,6 +281,7 @@ A document class\bindex{document class} can be defined using the @{command "doc_ \<^rail>\ 'rejects' (class_id * ',') \ \<^item> \default_clause\:\index{default\_clause@\default_clause\} \<^rail>\ '<=' '"' expr '"' \ + \clearpage \<^item> \regexpr\:\index{regexpr@\regexpr\} \<^rail>\ '\' class_id '\' | '(' regexpr ')' | (regexpr '||' regexpr) | (regexpr '~~' regexpr) | ('\' regexpr '\') | ( '\' regexpr '\\<^sup>*') \ @@ -380,7 +382,7 @@ doc_class EC = AC + representation. Note that the \inlineltx|\newisadof{}[]{}|-command requires the full-qualified names, \eg, \inlineisar|t$$ext.CENELEC_50128.EC| for the document class and \inlineisar|CENELEC_50128.requirement.long_name| for the attribute \inlineisar|long_name|, - inherited from the document class \inlineisar|requirement|. The document representation of ECs + inherited from the document class \inlineisar|requirement|. The representation of ECs can now be defined as follows: \begin{ltx} @@ -415,12 +417,11 @@ doc_class EC = AC + \ - +(*<*) text*[aaa::assertions]\description with validations I and II\ assert*[aaa::assertions] "3 < (4::int)" assert*[aaa::assertions] "0 < (4::int)" - - +(*>*) subsection*["text-elements"::technical]\Annotatable Top-level Text-Elements\ text\ @@ -433,8 +434,7 @@ text\ title*[title::title]\Isabelle/DOF\ subtitle*[subtitle::subtitle]\User and Implementation Manual\ text*[adb:: author, email="\a.brucker@exeter.ac.uk\", - orcid="\0000-0002-6355-1200\", - http_site="\https://brucker.ch/\", + orcid="\0000-0002-6355-1200\", http_site="\https://brucker.ch/\", affiliation="\University of Exeter, Exeter, UK\"] \Achim D. Brucker\ text*[bu::author, email = "\wolff@lri.fr\", affiliation = "\Université Paris-Saclay, LRI, Paris, France\"]\Burkhart Wolff\ @@ -447,7 +447,11 @@ text\ that has an identity as a text-object labelled as \obj_id\, belongs to a document class \class_id\ that has been defined earlier, and has its class-attributes set with particular values (which are denotable in Isabelle/HOL mathematical term syntax). - +\<^item> \meta_args\ : + \<^rail>\(obj_id ('::' class_id) ((attribute '=' term)) * ',')\ +\<^item> \rich_meta_args\ : + \<^rail>\ (obj_id ('::' class_id) ((attribute (('=' | '+=') term)) * ','))\ +\clearpage \<^item> \annotated_text_element\ : \<^rail>\ ( ( @@{command "title*"} @@ -466,11 +470,6 @@ text\ | change_status_command | inspection_command \ -\clearpage -\<^item> \meta_args\ : - \<^rail>\(obj_id ('::' class_id) ((attribute '=' term)) * ',')\ -\<^item> \rich_meta_args\ : - \<^rail>\ (obj_id ('::' class_id) ((attribute (('=' | '+=') term)) * ','))\ \