[Agda] emacs problems

[Shin-Cheng Mu]

Hi, Nisse,

On Jun 18, 2009, at 1:22 AM, Nils Anders Danielsson wrote:
> On 2009-06-17 10:33, Nils Anders Danielsson wrote:
>>
>> The problem is that, when GHC 6.10 is used on certain platforms,  
>> there
>> is an upper limit to the length of strings that can be sent to GHCi  
>> from
>> Emacs shell buffers:
>> http://code.google.com/p/agda/issues/detail?id=136
>
> I have released a potential fix for this problem. However, I am not  
> sure
> if the fix works on Windows and MacOS, so I would be grateful if it
> could be tested. If you can load the following module and do "give"
> (C-c C-SPC) in the hole, then things should be fine.

For some reason it doesn't seem to work here on my machine. I loaded
the file, did a "give" in the hole, then the computer just seemed
to be running forever (and Emacs did slow down as if its doing some
heavy computation). I had to hit Ctrl-g-z to abort the computation.

I have attached the transcript of the *ghci* buffer below. Notice
that the last string appears ill-formed.

   Mac OS X 10.5.7
   GNU Emacs 22.3.1 (i386-apple-darwin9.6.0, Carbon Version 1.6.0)
    of 2009-02-18 on plume.sr.unh.edu - Aquamacs Distribution 1.7
   GHC 6.10.1

sincerely,
Shin

   -----------------------------------

GHCi, version 6.10.1: http://www.haskell.org/ghc/  :? for help
Loading package ghc-prim ... linking ... done.
Loading package integer ... linking ... done.
Loading package base ... linking ... done.
Prelude> :set -package Agda-2.2.3
:set -package Agda-2.2.3
package flags have changed, resetting and loading new packages...
Loading package syb ... linking ... done.
Loading package base-3.0.3.0 ... linking ... done.
Loading package mtl-1.1.0.2 ... linking ... done.
Loading package old-locale-1.0.0.1 ... linking ... done.
Loading package old-time-1.0.0.1 ... linking ... done.
Loading package random-1.0.0.1 ... linking ... done.
Loading package QuickCheck-2.1.0.1 ... linking ... done.
Loading package array-0.2.0.0 ... linking ... done.
Loading package bytestring-0.9.1.4 ... linking ... done.
Loading package containers-0.2.0.0 ... linking ... done.
Loading package binary-0.5.0.1 ... linking ... done.
Loading package filepath-1.1.0.1 ... linking ... done.
Loading package unix-2.3.1.0 ... linking ... done.
Loading package directory-1.0.0.2 ... linking ... done.
Loading package extensible-exceptions-0.1.1.0 ... linking ... done.
Loading package terminfo-0.3.0.2 ... linking ... done.
Loading package utf8-string-0.3.4 ... linking ... done.
Loading package haskeline-0.6.1.6 ... linking ... done.
Loading package process-1.0.1.0 ... linking ... done.
Loading package haskell98 ... linking ... done.
Loading package pretty-1.0.1.0 ... linking ... done.
Loading package haskell-src-1.0.1.3 ... linking ... done.
Loading package xhtml-3000.2.0.1 ... linking ... done.
Loading package zlib-0.5.0.0 ... linking ... done.
Loading package Agda-2.2.3 ... linking ... done.
Prelude> :mod + Agda.Interaction.GhciTop
:mod + Agda.Interaction.GhciTop
Prelude Agda.Interaction.GhciTop> cmd_reset
cmd_reset
Prelude Agda.Interaction.GhciTop> cmd_load "/Users/scm/Documents/Agda/ 
Test.agda" [".", "/Users/scm/Library/Agda/lib/src"]
cmd_load "/Users/scm/Documents/Agda/Test.agda" [".", "/Users/scm/ 
Library/Agda/lib/src"]
Checking /Users/scm/Documents/Agda/Test.agda.
agda2_mode_code (agda2-highlight-reload)
agda2_mode_code (agda2-annotate '(0))
agda2_mode_code (agda2-status-action "")
agda2_mode_code (agda2-info-action "*All Goals*" "?0 : Set
")
Prelude Agda.Interaction.GhciTop> cmd_give 0 (Range [Interval (Pn "/ 
Users/scm/Documents/Agda/Test.agda" 1056 6 9) (Pn "/Users/scm/ 
Documents/Agda/Test.agda" 2056 6 1009)])  
"xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx 
xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx"
cmd_give 0 (Range [Interval (Pn "/Users/scm/Documents/Agda/Test.agda"  
1056 6 9) (Pn "/Users/scm/Documents/Agda/Test.agda" 2056 6 1009)])  
"xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx