search

UlfNorell / agda-test

Agda test
0 stars 0 forks source link

Broken highlighting in Emacs #936

Closed UlfNorell closed 10 years ago

UlfNorell commented 10 years ago

From vitus...@gmail.com on November 03, 2013 17:13:34

Relevant files:

-- Nat.agda module Nat where

data ℕ : Set where zero : ℕ suc : ℕ → ℕ

-- HL.agda module HL where

open import Nat

pattern 2+ n = suc (suc n) pattern 3+ n = suc (suc (suc n))

Clicking on the highlighted " n = suc " part opens Agda.Prim, as seen in the attachment hl3.png.

I'm using latest development version on Windows 7. Emacs 24.3.1.

Attachment: hl1.png hl2.png hl3.png

Original issue: http://code.google.com/p/agda/issues/detail?id=936

UlfNorell commented 10 years ago

From andreas....@gmail.com on November 03, 2013 10:58:55

My last patch (automatic import of Agda.Prim) broke the highlighting.

I am going to fix this the coming week, need some consultation with Ulf about it.

Status: Accepted
Owner: andreas....@gmail.com
Labels: Type-Defect Priority-High Highlighting

UlfNorell commented 10 years ago

From ulf.nor...@gmail.com on November 06, 2013 01:37:53

Labels: Milestone-2.3.4

UlfNorell commented 10 years ago

From andreas....@gmail.com on November 06, 2013 01:52:44

This is actually a variant of issue 495 , which was only uncovered by my latest patch. So I do not need to take the blame for this.

Owner: ulf.nor...@gmail.com
Labels: PatternSynonyms

UlfNorell commented 10 years ago

From ulf.nor...@gmail.com on November 06, 2013 02:35:19

Status: Fixed
Labels: -PatternSynonyms

UlfNorell commented 10 years ago

From ulf.nor...@gmail.com on November 06, 2013 05:39:43

And Andreas: Sorry, but it had nothing to do with pattern synonyms. It was all your fault :).

andreas commented 10 years ago

@UlfNorell, you're mentioning the wrong person ("@andreas" is me).

UlfNorell commented 10 years ago

@andreas: sorry about that, these issues were auto imported from google code.