Wierd Error (sometimes) when displaying context and goal

From sculthor...@gmail.com on December 05, 2008 16:35:44

What steps will reproduce the problem? Difficult, as moving the file to a different directory fixes the problem inexplicably. What is the expected output? What do you see instead? I do Ctrl-c Ctrl-, to get the goal type and context in a goal. It doesn't work in the second two goals in the file. Removing the function foo starts the second goal working. (As far as I can tell, its to to with how far down the file the goal is.)

In the GHCi buffer:

Prelude Agda.Interaction.GhciTop> cmd_load "/home/nas/neil/ComputerScience/Agda/Yampa/YampaResponsive3/SigVec.agda" [".", "/home/nas/neil/ComputerScience/Agda/NeilLib/"] agda2_mode_code (agda2-highlight-reload) agda2_mode_code (agda2-load-action '(0 1 2)) agda2_mode_code (agda2-status-action "") agda2_mode_code (agda2-info-action "All Goals" "?0 : .F -> .F ?1 : .G -> .G ?2 : .H -> .H ") Prelude Agda.Interaction.GhciTop> cmd_goal_type_context Agda.Interaction.BasicOps.Normalised 2 (Range [Interval (Pn "/home/nas/neil/ComputerScience/Agda/Yampa/YampaResponsive3/SigVec.agda" 159 13 6) (Pn "/home/nas/neil/ComputerScience/Agda/Yampa/YampaResponsive3/SigVec.agda" 160 13 7)]) ""

:1:254: lexical error at character '\EOT' Prelude Agda.Interaction.GhciTop> What version of the product are you using? On what operating system? Latest darcs version downloaded today. Ubuntun 8.4. GHC 6.10 Additional Information This error crops in a few files and directorieis, but only the minority. **Attachment:** [SigVec.agda](http://code.google.com/p/agda/issues/detail?id=114) _Original issue: http://code.google.com/p/agda/issues/detail?id=114_

UlfNorell / agda-test

Wierd Error (sometimes) when displaying context and goal #114