Automated linebreaks in manual (tamarin-prover#677)

* updates script, new keys * fix directory * github workflow * make pdf * add * deploy to manual repo, not to code repo * set key before checking out * directory * Error search * fixed latex template * update pandoc version * Manual: Automated linebreaks in latex template * Missing linebreak. --------- Co-authored-by: Jannik Dreier <[email protected]> Co-authored-by: jdreier <[email protected]> Co-authored-by: Robert Künnemann <[email protected]>
rkunnema · Sep 9, 2024 · 0396410 · 0396410
1 parent 7c33569
commit 0396410
Show file tree

Hide file tree

Showing 3 changed files with 13 additions and 4 deletions.
diff --git a/manual/grammar/grammar.ebnf b/manual/grammar/grammar.ebnf
@@ -92,8 +92,10 @@ rules:
   variants  ::=  'variants' simple_rule (',' simple_rule)*
   modulo  ::=  '(' 'modulo' ('E' | 'AC') ')'
   rule_attrs  ::=  '[' rule_attr (',' rule_attr)* ','? ']'
-  rule_attr  ::=  rule_attr_color | 'no_derivcheck'
+  rule_attr  ::=  rule_attr_color | 'no_derivcheck' | 'issapicrule' | rule_process | rule_role
   rule_attr_color  ::=  ('color=' | 'colour=') hexcolor
+  rule_role  ::=  'role' '=' '"' (ident: role_identifier) '"'
+  rule_process  ::=  'process' '=' '"' ident '"'
   rule_let_block  ::=  'let' rule_let_term+ 'in'
   rule_let_term  ::=  ((msg_var_or_nullary_fun | nat_var): left) '=' (_term: right)
   macros  ::=  'macros' ':' macro (',' macro)*

diff --git a/manual/src/016_syntax_description.md b/manual/src/016_syntax_description.md
@@ -104,6 +104,7 @@ When exporting, one may indicate which lemmas should only be included in certain
 ~~~~
 
 In observational equivalence mode, lemmas can be associated to one side.
+
 ~~~~ {.tamarin grammar="grammar/grammar.ebnf" rules="diff_lemma,diff_lemma_attrs,diff_lemma_attr"}
 ~~~~
 
@@ -213,8 +214,6 @@ after the first character. Moreover, they must not be one of the
 reserved keywords `let`, `in`, or `rule`. Although identifiers beginning with
 a number are valid, they are not allowed as the names of facts (which
 must begin with an upper-case letter).
-~~~~ {.tamarin grammar="grammar/grammar.ebnf" rules="ident"}
-~~~~
 
 Full syntax
 -----------

diff --git a/manual/templates/template.latex b/manual/templates/template.latex
@@ -8,6 +8,14 @@
 \usepackage[labelformat=empty]{caption}
 \usepackage{afterpage}
 
+% added for line breaks in "fenced code blocks"
+% https://github.com/jgm/pandoc/issues/4302
+\usepackage{fvextra}
+\DefineVerbatimEnvironment{Highlighting}{Verbatim}{commandchars=\\\\\\{\\}, breaklines, breaknonspaceingroup, breakanywhere}
+\fvset{breaklines}
+\fvset{breaknonspaceingroup}
+\fvset{breakanywhere}
+
 \newcommand\blankpage{%
     \null
     \thispagestyle{empty}%
@@ -166,7 +174,7 @@ $if(listings)$
 \usepackage{listings}
 $endif$
 $if(lhs)$
-\lstnewenvironment{code}{\lstset{language=Haskell,basicstyle=\small\ttfamily}}{}
+\lstnewenvironment{code}{\lstset{language=Haskell,basicstyle=\small\ttfamily,breaklines=true,breakatwhitespace=true,breakautoindent=true}}{}
 $endif$
 $if(highlighting-macros)$
 $highlighting-macros$