search

markokoleznik / agda-writer

A simple GUI for Agda
Other
31 stars 2 forks source link

Line numbers and error messages #19

Closed andrejbauer closed 9 years ago

andrejbauer commented 9 years ago

There are no line numbers and there is no way to move automagically to the error reported by Agda, so this leaves the user in a hopeless situation. Two possible solutions would be to:

  1. Display line numbers.
  2. Parse error messages and make them active so that clicking on them places the cursor onto the location.
markokoleznik commented 9 years ago

both of those suggestions are on todo list :)

markokoleznik commented 9 years ago

Main text window now shows line numbers. Any message that has range in it (line number and range) are now parsed with custom Tokens, so when user presses that token, it selects that part of the string.

I can change color of tokens if they are too "shiny"