[Agda] emacs problems

Andreas Buechele andreas.buechele at googlemail.com
Wed Jun 17 00:01:04 CEST 2009


Hi *,

I'm using emacs-23 and some strange behaviour of the Agda interface
arise. I'm using Agda frequently and everything worked fine till yesterday.

In some of my new source files the "context and goal type" feature isn't
working. If I press "Ctrl-," the status line says "Wrote /tmp/***" and
the ghci buffer says:

---8<---
Prelude Agda.Interaction.GhciTop> cmd_goal_type_context
Agda.Interaction.BasicOps.Normalised 0 (Range [Interval (Pn
"SomeAgdaFile.agda" 2260 52 41) (Pn "SomeAgdaFile.agda" 2260 52 41)]) ""

<interactive>:1:254: lexical error at character '\EOT'
Prelude Agda.Interaction.GhciTop>
--->8---

I've tested the current stable and development version of Agda -> same
behaviour.

I have attached a example file. If I try to use "Ctrl-," at the goal,
the above described problem arise. If I delete the comment, the problem
disappear. If I rename the module to someting shorter, the problem
disappear. Uhh??? I don't get it!

Kind regards,
  Andreas
-------------- next part --------------
module Trees.Properties.xxxxxxxxxxxxDelete where
{-
import Relations.Properties.Closure
-}
xxx : Set -> Set
xxx x = {!!}


More information about the Agda mailing list