[Agda] Bug in ScopeMonad?

[Paul van der Walt]

Hi all,

I've been using literate Agda to start writing up some stuff,
and I'd like automatic syntax highlighting. My first attempt has
been to get the compiler to type-check my module, then output a
list of symbols which are in-scope, which I format as LHS-format
rules. See the attached patch; it's not really world-ready, but
since something is broken, I thought I'd include the example. It
should apply cleanly on the darcs HEAD of Agda.

Anyway, the way to test it would be to run something like the
following:

$ cd your-stdlib-dir/src
$ agda Algebra.agda --lagda

...at which point you should get (after a wait - the
type-checking progress output is silenced) a list of rules like

%format IsPartialOrder = "\defin{IsPartialOrder}"

i.e. something I can pipe into an LHS .fmt file, the idea being
that I then just need to define formatting (colouring) commands
like \defin{}. Anyway, that's only working if the .agdai file
_doesn't_ exist. If it does, I get this error:

ERROR: In scope
ScopeInfo
  current = 
  context = TopCtx
  modules
    * scope 

NO SUCH SCOPE Algebra
An internal error has occurred. Please report this as a bug.
Location of the error: src/full/Agda/Syntax/Scope/Monad.hs:80

I'm not sure if this is really a bug, which is why I'm posting
here first. If anyone really thinks something is broken, I'll
send the report off to the tracker at code.google.com. The
interesting (and broken?) bit is in my modifications to
Agda.Main. It looks very similar to the analogous bit in
Agda.Interaction.InteractionTop, though, and I've tried a number
of variations on retrieving the current module or scope, to no
avail.

If anyone has any ideas, I'd be much obliged.

Thanks in advance, and kind regards,

Paul van der Walt

PS: assuming the code gets cleaned up a little, is this a
feature others would use? I'm finding it a huge time-saver.
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/pgp-signature
Size: 836 bytes
Desc: Digital signature
Url : http://lists.chalmers.se/pipermail/agda/attachments/20120625/8eca5a5b/attachment.bin