How can I overlay cetz diagrams on top of code?

Questions
5

It’s certainly possible to some extent. You can use codly for a code display with many features, for example line highlights and line labels (detailed by code line and code column).

The label gives you access to the absolute position of that word in the code through the query system. I wonder if there’s some way to use labels as coordinates in cetz.

Proof of concept / "bad example"

This example shows that it is possible. I think it would be better to do this with cetz instead of typst drawing primitives. As seen in the example, the text after the figure starts without taking the extent of the annotation boxes into account.

bild
bild780×328 55.1 KB

#import "@preview/codly:1.3.0": *
#show: codly-init.with()

// Testing out codly's feature that allows labels on individual lines of code

#let code = raw(block: true, 
"example : ∀ (p q: Prop), p ∨ q → q ∨ p := by
  intro p q h
  cases h
  ⋅ apply Or.inr
    assumption
  ⋅ apply Or.inl
    assumption
")
#codly(highlights:(
  (line: 2, start: 3, end: none, label: <mark1>),
  (line: 3, start: 3, end: none, label: <mark2>),
), annotations: (
))
#figure(
  code
)<myfigure>

Test my labels @mark1 and @mark2


/// Draw a line from the label's code line down to a box
/// xoffset: x-offset from label coordinate to the start of the line
/// xline, yline: length of the line to the box.
#let drawbox(at-label, content, yoffset: 1em, xoffset: 20em, xline: 5em, yline: 5em,
  line-style: (:), block-style: (:)) = context {
  let codeline = query(at-label).first()
  let pos = codeline.location().position()
  let xstart = pos.x - 30mm // page margin, needs to be updated
  let ystart = pos.y - 30mm

  let xbox = xstart + xoffset + xline 
  let ybox = ystart + yoffset + yline
  place(top + left, dx: xoffset + xstart, dy: ystart + yoffset,
    line(start: (0%, 0%), end: (xline, yline), ..line-style))
  place(top + left, dx: xbox, dy: ybox, block(..block-style, content))
}

#let drawbox = drawbox.with(
  block-style: (inset: 0.75em, stroke: 0.5pt + purple.darken(60%), fill: gray.lighten(90%).transparentize(25%), radius: 0.5em),
  line-style: (stroke: (thickness: 0.5pt, dash: "dashed")))

#let annot1 = $
  p, q & : sans("Prop") \
  h & : p or q \
  & tack q or p
$
#drawbox(<mark1>, annot1, xline: 4em, yline: 1em)

#let annot2 = $
  p, q & : sans("Prop") \
  h & : p \
  & tack q or p \
  p, q & : sans("Prop") \
  h & : q \
  & tack q or p
$

#drawbox(<mark2>, annot2, yline: 2em, xoffset: 11.5em)


#lorem(20)
2 Likes