Dobule pipes in language not rendered

[leafac]

EDIT: I figured my mistake. See post below.

Minimal working example

#lang racket
(require redex)

(define-language pipe
  [operator ::= \| || \|||])

(module+ test
  (test-equal (redex-match? pipe operator (term \|)) #t)
  (test-equal (redex-match? pipe operator (term ||)) #t)
  (test-equal (redex-match? pipe operator (term \|||)) #t))

(render-language pipe)

Expected behavior

The typeset version of the grammar should include the double pipes in || and |||.

Current behavior

The typeset version of the grammar omits double pipes.

Caveat

Granted, having pipes on the grammar confuses things, since pipes are already used as or in BNF notation. But I'm fine with the font alone distinguishing between BNF operator and language terminal—this lets me stay closer to the language I'm modeling, in which || is an operator.

---

Can you please confirm that my proposal is indeed expected behavior? If so, can you please help me fix it?

Thanks a lot!

[leafac]

Opening this Issue revealed a fundamental misunderstanding of Racket's syntax when it comes to pipes (|). It turns out that my expectations were wrong—Redex's typesetting was right.

See the corrected snippet, with escapes on every | within the identifier:

#lang racket
(require redex)

(define-language pipe
  [operator ::= \| \|\| \|\|\|])

(module+ test
  (test-equal (redex-match? pipe operator (term \|)) #t)
  (test-equal (redex-match? pipe operator (term \|\|)) #t)
  (test-equal (redex-match? pipe operator (term \|\|\|)) #t))

(render-language pipe)

Now the typeset version is what I wanted:

If someone wants to explain what || means and how typesetting worked on my wrong example, I'd be thankful.

[rfindler]

Glad you got this sorted out!

[bennn]

In Racket, || is the empty identifier.

Because identifiers are scoped symbols, and any string can be turned to a symbol -- even "⇒" or "λ" or "hello world" -- and we need something to delimit symbols containing whitespace. The delimiter happens to be |:

> (string->symbol "hello world")
'|hello world|

I guess | is the delimiter because it's close to the other delimiters on many keyboards and looks kind of like braces.

For the official explanation, search for "|" in the docs: link

[leafac]

@bennn: Thank you for the explanation. I understand what is going on, now.

I didn't know I could search for punctuation on Racket documentation. In all other search engines that I used, it doesn't work, so I just never thought of trying.

Racket keeps impressing me! 👍