JSON interaction produces fully qualified terms

[isovector]

Consider the following interaction via --interaction:

Agda2> IOTCM "/home/sandy/prj/test/src/BialgebraSorting.agda" None Direct (Cmd_load "/home/sandy/prj/test/src/BialgebraSorting.agda" [])

(agda2-info-action "*All Goals*" "?0\n  : map In (map (fold (map In)) (inᵒ x)) ≡ fold (map In) (In (inᵒ x))\n?1 : inᵒ x ≡ map In (map (fold (map In)) (inᵒ x))\n" nil)

vs --interaction-json:

JSON> IOTCM "/home/sandy/prj/test/src/BialgebraSorting.agda" None Direct (Cmd_load "/home/sandy/prj/test/src/BialgebraSorting.agda" [])

{"kind":"DisplayInfo","info":{"visibleGoals":[{"constraintObj":{"range":[{"start":{"line":58,"pos":1453,"col":8},"end":{"line":58,"pos":1454,"col":9}}],"id":0},"kind":"OfType","type":"BialgebraSorting.Example.map BialgebraSorting.Example.In\n(BialgebraSorting.Example.map\n (BialgebraSorting.Example.fold\n  (BialgebraSorting.Example.map BialgebraSorting.Example.In))\n (BialgebraSorting.Example.inᵒ x))\n≡\nBialgebraSorting.Example.fold\n(BialgebraSorting.Example.map BialgebraSorting.Example.In)\n(BialgebraSorting.Example.In (BialgebraSorting.Example.inᵒ x))"},{"constraintObj":{"range":[{"start":{"line":56,"pos":1411,"col":8},"end":{"line":56,"pos":1412,"col":9}}],"id":1},"kind":"OfType","type":"BialgebraSorting.Example.inᵒ x ≡\nBialgebraSorting.Example.map BialgebraSorting.Example.In\n(BialgebraSorting.Example.map\n (BialgebraSorting.Example.fold\n  (BialgebraSorting.Example.map BialgebraSorting.Example.In))\n (BialgebraSorting.Example.inᵒ x))"}],"kind":"AllGoalsWarnings","warnings":[],"invisibleGoals":[],"errors":[]}}

The resulting goals are very different:

?0
  : map In (map (fold (map In)) (inᵒ x)) ≡ fold (map In) (In (inᵒ x))
?1 : inᵒ x ≡ map In (map (fold (map In)) (inᵒ x))

vs

?0 : BialgebraSorting.Example.map BialgebraSorting.Example.In
     (BialgebraSorting.Example.map
      (BialgebraSorting.Example.fold
       (BialgebraSorting.Example.map BialgebraSorting.Example.In))
      (BialgebraSorting.Example.inᵒ x))
     ≡
     BialgebraSorting.Example.fold
     (BialgebraSorting.Example.map BialgebraSorting.Example.In)
     (BialgebraSorting.Example.In (BialgebraSorting.Example.inᵒ x))
?1 : BialgebraSorting.Example.inᵒ x ≡
     BialgebraSorting.Example.map BialgebraSorting.Example.In
     (BialgebraSorting.Example.map
      (BialgebraSorting.Example.fold
       (BialgebraSorting.Example.map BialgebraSorting.Example.In))
      (BialgebraSorting.Example.inᵒ x))

[isovector]

The difference here appears to be that EmacsTop calls showGoals before handing it off:

https://github.com/isovector/agda/blob/c15b484129e55d62cbab17550286cd7d2403e133/src/full/Agda/Interaction/EmacsTop.hs#L125

while JSON sends it as is:

https://github.com/isovector/agda/blob/c15b484129e55d62cbab17550286cd7d2403e133/src/full/Agda/Interaction/JSONTop.hs#L263