Skip to content

Commit

Permalink
Change Latex anchor to soemthing without conflict
Browse files Browse the repository at this point in the history
  • Loading branch information
rossberg committed Feb 4, 2024
1 parent bb12b18 commit d0fc0d6
Show file tree
Hide file tree
Showing 3 changed files with 30 additions and 30 deletions.
16 changes: 8 additions & 8 deletions spectec/doc/Latex.md
Original file line number Diff line number Diff line change
Expand Up @@ -50,7 +50,7 @@ regexp ::=

The `tag` can be configured differently for different file formats. Currently, two formats are supported:

* _Latex._ Tags are `@` and `@@`, generating `$...$` and `$$...$$`, respectively.
* _Latex._ Tags are `#` and `##`, generating `$...$` and `$$...$$`, respectively.

* _Sphinx._ Tags are `$` and `$$`, generating `:math:'...'` and `.. math:: ...`, respectively.

Expand Down Expand Up @@ -98,21 +98,21 @@ The names in a definition splice refer to definitions according to the indicated

```
;; insert definitions of types
@@@{syntax: numtype vectype valtype}
$${syntax: numtype vectype valtype}
;; insert grammar for control and reference instructions together
@@@{syntax: {instr/control instr/reference}}
$${syntax: {instr/control instr/reference}}
;; insert grammar for all instructions in a single grammar
@@@{syntax: {instr/*}}
$${syntax: {instr/*}}
;; insert typing rules for `unreachable`, `nop` and `drop`,
;; putting the first on its own, the latter two on the same line
@@@{rule: Instr_ok/unreachable {Instr_ok/nop Instr_ok/drop}}
$${rule: Instr_ok/unreachable {Instr_ok/nop Instr_ok/drop}}
;; insert reduction rules for `block`, `loop` and all the ones for `if`,
;; as well as `br` and `br_if`, but with small vertical space
@@@{rule: {Step/block Step/loop Step/if-*} {Step/br Step/br_if}}
$${rule: {Step/block Step/loop Step/if-*} {Step/br Step/br_if}}
```


Expand Down Expand Up @@ -172,12 +172,12 @@ Hints of the form `hint(show <exp>)` are recognised on a number of constructs an
relation Step: instr* ~> instr* hint(show "S")
rule Step/drop: val DROP ~> eps
```
After this, the splice `@@@{rule+: Instr_ok/nop}` will generate (in proper Latex)
After this, the splice `$${rule+: Instr_ok/nop}` will generate (in proper Latex)
```
------------------------ [T-drop]
C |- DROP : t -> eps
```
Similarly, the splice `@@@{rule+: Step/nop}` will generate
Similarly, the splice `$${rule+: Step/nop}` will generate
```
[S-nop] val DROP ~> eps
```
Expand Down
4 changes: 2 additions & 2 deletions spectec/src/backend-splice/config.ml
Original file line number Diff line number Diff line change
Expand Up @@ -22,8 +22,8 @@ type t = config

let latex =
{ anchors = [
{token = "@"; prefix = "$"; suffix = "$"; indent = ""};
{token = "@@"; prefix = "$$\n"; suffix = "\n$$"; indent = ""};
{token = "#"; prefix = "$"; suffix = "$"; indent = ""};
{token = "##"; prefix = "$$\n"; suffix = "\n$$"; indent = ""};
];
latex = Backend_latex.Config.default;
prose = Backend_prose.Config.default;
Expand Down
40 changes: 20 additions & 20 deletions spectec/test-splice/spec-latex.in.tex
Original file line number Diff line number Diff line change
Expand Up @@ -19,9 +19,9 @@

\subsection*{Syntax}

@@{definition: size}
##{definition: size}

@@{syntax+:
##{syntax+:
limits
{globaltype
functype
Expand All @@ -31,50 +31,50 @@ \subsection*{Syntax}
externtype
}

@@{syntax: {instr/control}}
##{syntax: {instr/control}}

@@{syntax: {instr/numeric instr/local instr/global instr/memory} expr}
##{syntax: {instr/numeric instr/local instr/global instr/memory} expr}


\subsection*{Typing @{relation: Instr_ok}}
\subsection*{Typing #{relation: Instr_ok}}

An instruction sequence @{:instr*} is well-typed with an instruction type @{functype: t_1* -> t_2*}, written @{:instr*} $:$ @{functype: t_1* -> t_2*}, according to the following rules:
An instruction sequence #{:instr*} is well-typed with an instruction type #{functype: t_1* -> t_2*}, written #{:instr*} $:$ #{functype: t_1* -> t_2*}, according to the following rules:

@@{rule:
##{rule:
{Instrs_ok/empty Instrs_ok/seq}
{Instrs_ok/frame}
}

@@{rule+: Instrs_ok/*m* {Instrs_ok/*m*}}
##{rule+: Instrs_ok/*m* {Instrs_ok/*m*}}

@@{rule: {Instr_ok/unreachable Instr_ok/nop Instr_ok/drop}}
##{rule: {Instr_ok/unreachable Instr_ok/nop Instr_ok/drop}}

@@{rule+: Instr_ok/block}
##{rule+: Instr_ok/block}

@@{rule+: Instr_ok/loop}
##{rule+: Instr_ok/loop}

@@{rule+: Instr_ok/if}
##{rule+: Instr_ok/if}


@@{rule-ignore: Instr_ok/convert-*}
##{rule-ignore: Instr_ok/convert-*}


\subsection*{Runtime}

@@{definition: default}
##{definition: default}

@@{definition: {funcaddr funcinst} {func table}}
##{definition: {funcaddr funcinst} {func table}}


\subsection*{Reduction @{relation: Step_pure}}
\subsection*{Reduction #{relation: Step_pure}}

The relation @{Step: config ~> config} checks that a function type is well-formed.
The relation #{Step: config ~> config} checks that a function type is well-formed.

@@{rule: Step/pure Step/read}
##{rule: Step/pure Step/read}

@@{rule+: {Step_read/block Step_read/loop} {Step_pure/if-*}}
##{rule+: {Step_read/block Step_read/loop} {Step_pure/if-*}}

@@{rule+: Step_pure/if-*}
##{rule+: Step_pure/if-*}

\end{document}

Expand Down

0 comments on commit d0fc0d6

Please sign in to comment.