Interpreting [] in tex production

[buggymcbugfix]

I have a terminal []—is there a way of "escaping" it for purposes of tex production?

Right now I am using a workaround like this:

  | [] c A :: :: Box {{ com Box }} {{ tex \square_{[[c]]} [[A]] }}

[buggymcbugfix]

PS: I am using this terminal in more than one production.

[PeterSewell]

It's not clear what the question is. If you want some kind of parameterised terminal, then no, Ott doesn't support that. The simplest thing would be to abstract out the common typesetting into a single latex command that you use in the {{ tex ...}} hom of the multiple productions.

…

On Wed, 21 Nov 2018 at 09:54, Vilem ***@***.***> wrote: PS: I am using this terminal in more than one productions. — You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub <#44 (comment)>, or mute the thread <https://github.com/notifications/unsubscribe-auth/AErM5p1UPf1kpWmdGGu0WOYZHMGnFzRWks5uxSLlgaJpZM4Ysw9X> .

[buggymcbugfix]

Hm, no I didn't mean a parameterised terminal. I guess this is a parsing issue: I just want [] to be interpreted as a terminal. Let me give you a small (counter) example.

terminals ::=
  | <> :: :: diamond {{ tex \lozenge }}
  | [] :: :: box     {{ tex \square }}

A, B :: 'Type_' ::=
  | <> e A :: :: Diamond {{ tex [[<>]]_{[[e]]} [[A]] }}  % ok
  | [] c A :: :: Box     {{ tex [[[]]]_{[[c]]} [[A]] }}  % nope
  | ...

So, here <> does the thing I want, but [] doesn't; I believe that this is because [] interferes with the quoting [[-]] syntax.

[francesco-zappa-nardelli]

A, B :: 'Type_' ::= | <> e A :: :: Diamond {{ tex [[<>]]_{[[e]]} [[A]] }} % ok | [] c A :: :: Box {{ tex [[[]]]_{[[c]]} [[A]] }} % nope | ... So, here <> does the thing I want, but [] doesn't; I believe that this is because [] interferes with the quoting [[-]] syntax.

I am not sure and should check, but maybe adding spaces here is enough (eg. [[ [] ]]).

…

-francesco

[buggymcbugfix]

Hey, thanks for that suggestion! I had tried that, alas, it does not work.

[PeterSewell]

looks like a bug in the lexing of [[ ]], because still: metavar var, x ::= {{ com term variable }} grammar term, t :: 't_' ::= {{ com term }} | x :: :: var {{ com variable}} | t t' :: :: app {{ com app }} | <> e A :: :: Diamond {{ tex [[ <> ]]_{[[e]]} [[A]] }} % ok | [] c A :: :: Box {{ tex [[ [] ]]_{[[c]]} [[A]] }} % nope terminals :: 'terminals_' ::= | [] :: :: box {{ tex \Box }} | <> :: :: box3 {{ tex \diamond }} There is some machinery for quoting terminals, e.g. to allow | and :: to be used in object-language syntax, but it may be only in productions not inside [[ ]] inside tex homs. No time to fix, sorry - and there's an easy workaround, to just write \Box in place of [[ [] ]] wherever you use it. Peter

…

On Wed, 21 Nov 2018 at 11:50, Vilem ***@***.***> wrote: Hey, thanks for that suggestion! I had tried that, alas, it does not work. — You are receiving this because you commented. Reply to this email directly, view it on GitHub <#44 (comment)>, or mute the thread <https://github.com/notifications/unsubscribe-auth/AErM5j3_dfV_0ed_p4i4kgRjXqcVrtszks5uxTrVgaJpZM4Ysw9X> .