[Agda] Bug in ScopeMonad?

[Andreas Abel]

Aeh, at least I cannot see an attached patch...

On 25.06.12 9:26 PM, Paul van der Walt wrote:
> 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.
>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/