colors not updated when using refine or auto

[agda]

colors not updated when using refine or auto

[GoogleCodeExporter]

Original comment by nils.anders.danielsson on 5 Oct 2009 at 5:50

[GoogleCodeExporter]

Would this be easier now that we don't rely on highlighting files?

Original comment by [email protected] on 24 Nov 2009 at 11:53

[GoogleCodeExporter]

We still rely on highlighting files, but now they are written out on
demand (and deleted once read). I suspect that a nice fix to this
issue involves redesigning the interface between the frontend and the
backend, so that the backend knows more about the changes done to the
source.

Original comment by nils.anders.danielsson on 24 Nov 2009 at 2:16

[GoogleCodeExporter]

Original comment by [email protected] on 11 Sep 2011 at 11:40

• Added labels: Emacs

[GoogleCodeExporter]

Fixed for give. Still doesn't work for refine or auto, though.

Original comment by [email protected] on 24 Jan 2014 at 6:59

• Changed title: colors not updated when using refine or auto
• Added labels: Priority-Medium
• Removed labels: Priority-Low

[GoogleCodeExporter]

Fixed. All fillings of holes now get pretty colours.

For commands that aren't give, this works by the emacs mode calling a new 
command
Cmd_highlight every time it fills a hole. This command parses a given string in 
the context
of a recently filled hole and generates syntax highlighting for it.

Original comment by [email protected] on 29 Jan 2014 at 11:30

• Changed state: Fixed

[GoogleCodeExporter]

This feature doesn't interact properly with interactive highlighting.
If interactive highlighting is turned on and the goal below is filled
with "F Set", then the space character is highlighted using
agda2-highlight-typechecks-face:

  Foo : (Set₁ → Set) → Set
  Foo F = ?

Original comment by nils.anders.danielsson on 4 Apr 2014 at 5:11

• Changed state: Accepted
• Added labels: Milestone-2.3.4, Priority-High
• Removed labels: Priority-Medium

[GoogleCodeExporter]

I can't reproduce this. I had this problem before but I (thought I) fixed it. 
In any case it's not really related to this feature, but rather a bug in 
interactive highlighting. Please open a new issue.

Original comment by [email protected] on 9 Apr 2014 at 12:06

• Changed state: Fixed