markokoleznik/agda-writer

A simple GUI for Agda

agda-writer's Issues

Newlines in status reports

Error messages and normalize results should end with \n.

Parse \ as backslash

Parse \ as '`, that is in Agda the backslash is an ordinary charater (actually, it stands for lambda).

Agda Writer vs. Agda Wrapper

The project is called "Agda Writer" but the application icon says "Agda Wrapper". Which will it be?

How to type Unicode

1. We can have a translation table which maps words to words, possibly configurable through Preferences.
2. Whenever the user types a whitespace character, we look at the word at the cursor and map it using the translation table.
3. We may also add a command which tokenizes everything in a file (or in the selection if there is a selection).

Add included libraries when sending action

User can add libraries when interacting with Agda. Libraries can be included in Preferences.

Highlight goal when inside it.

It would be nice to hhighlight the goal in the upper-right when the cursor is inside the corresponding {! ... !}. Also, I tend to use spaces, so {! blah !} instead of {!blah!}, but I do not know if there is an adopted standard.

Version v1.2.3 (binary) forgets path to the agda binary

I set Path to Agda in preferences, closed the window. Opened it again, and nothing's there.
I tried working around this by editing the defaults.plist file, but after that I started getting:

*Error*
only one input file allowed

The part of the plist:

        <key>agdaLaunchPath</key>
        <string>/usr/local/Cellar/agda/2.5.3_1/bin/agda</string>

Auto-complete too eager

Suppose I have the following text:

g : Set -> Set
g x = x

and I place the cursor just after the = sign. Then autocomplete shows up an offers that I change = to ⇒. This is slightly annoying but ok. Then if I press Esc to cancel the suggestion, it shows up again and it seems hard to get rid of it. Also, it is annoying that any movement (say right arrow key) confirms the suggestion.

I would rather see auto-complete mini-windows disabled than showing up like this in annoying ways. Even if it is a user-defined preference, auto-complete shouldn't be popping up quite so eagerly.

Where to look for the agda executable?

Reasonable places to look:

• ~/.cabal/bin/agda
• ~/Library/Haskell/bin/agda
• /Library/Haskell/bin/agda

The procedure:

1. If executable is set in preferences, use that.
2. If agda found in PATH then use that (but do not set in preferences).
3. If not found, then open a dialog for the user to specify agda.
4. The dialog may provide a default choice, namely agda found in one of the reasonable places above (but user must confirm this choice, and has the ability to change).
5. The choice made by the user is remembered. Henceforth he can change the executable through Preferences.

Agda path in preferences

1. In the preferences, the file browser for Agda path does not allow me to select the agda executable (it's greyed out).
2. The input field for Agda path does not seem to accept Paste (⌘V) instead the paste went into the main editing window.

Can't launch Agda it seems

I set my Agda executable in preferences to /Users/andrej/.cabal/bin/agda and as far as I can tell this is correct. However, this seems insufficient to launch Agda. How can I perform further tests to see what actually died? The output window shows that the launch response was empty.

Disable smart input method

The input method changes -- to –, so it's kind of hard to write comments. See "smart dashes" setting in Interface Builder.

Missing `.pbxproj` file?

When I try to open AgdaWriter.xcodeproj Xcode says:

Project /Users/andrej/Documents/agda-writer/AgdaWriter.xcodeproj
cannot be opened because it is missing its project.pbxproj file.

Now what?

Unicode input in goals windows

User should be able to write unicode characters in goals popup window, not just in main text window.

enable autocompletion in dialog (global or goal specific)

unicode tranformation works, but it would be nice to see autocompletion dialog as well when normalizing, for example.

How to close the "normalize" dialog?

In the "normalize" input dialog, how do I cancel it? Esc does not seem to work.

`startRow` in `selectedGoal` isn't correct

I'm sending wrong indexes to Agda, that's why error messages shows wrong range of an error.

Translate to Unicode after newline and tab, ignore ( and )

The automatic translation to unicode should work also when user presses Enter and Tab, ( or ), not just Space. It should consider ( and ) as delimiters -- they are not part of the words. For instance, if I type:

g : (N -> N) -> N
g _ = zero

then all three Ns should become ℕ (I am not really sure about this particular translation).

NSTableView doesn't get retained

After creating a NSTableView with appropriate delegate and datasource, it gets drawn on the screen, but ARC (automatic reference counting) immediately sets self.table to nil.
If you click or scroll (any interaction with table), exception with EXC_BAD_ACCESS is thrown.

Line numbers and error messages

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.

Issue with multiple libraries...

Strangley, it seems to look into given directory but still "throws" an error.

Insert spaces when hitting 'tab' key

Perhaps how many spaces to insert can be a configurable setting.

Disable completions on all irrelevant text inputs.

If you press esc in any of text input, words completions pops up. That's annoying :)

Load deletes {| ... |}

On Load in the following code sup ? disappears:

 module Foo where

 data bool : Set where
   false : bool
   true : bool

 or : bool -> bool -> bool
 or false y = y
 or true _ = true

 data N : Set where
   zero : N
   succ : N -> N

 data Ordinal : Set where
   zer : Ordinal
   suc : Ordinal -> Ordinal
   sup : (N -> Ordinal) -> Ordinal

 sum : Ordinal -> Ordinal -> Ordinal
 sum zer y = y
 sum (suc x) y = suc (sum x y)
 sum (sup xs) y = {! sup ? !}

Error: Only one input allowed

Since the version 2.5 Agda uses new package management.

Now, the error is thrown when loading a file:
Error: Only one input file allowed

The easiest way (I think) is to check the Agda version and decide what execution command to perform but that is a rather ugly one. Any suggestions?

@banacorn How did you solve this? Also by "hacking" ? :)

Primitive.agda: openFile: does not exist (No such file or directory)

Really excited about this project!

Compiled myself using Xcode and tried to typecheck:

*Error*
/Users/nikita/Library/Developer/Xcode/DerivedData/Agda_Writer-bkhyhfeszfmmsyclqnrcntveamnu/Build/Products/Debug/Agda
Writer.app/Contents/Resources/Agda-2.4.2.2/lib/prim/Agda/Primitive.agda:
openFile: does not exist (No such file or directory)

How do I configure it? I just ran it from the command line from the DerivedData directory.

Make this cross-platform

Can you modify it so it compiles on linux?

Crashing on this example.

module Foo where

data bool : Set where
  false : bool
  true : bool

or : bool -> bool -> bool
or false y = y
or true _ = true

f : bool -> bool
f x = {!!}

g : bool -> bool
g y = f {!? y!}

Commit version 07db2f0

Pasting should not preserve style

When pasting code from somewhere else, style is also applied on that string (bold, color, background color...)

Undo redo

Implement undo, redo.

Reload file when case splitting

I was surprised that it didn't reload after a case split.

Package Agda with agda-writer

The Agda license allows that the Agda executable be packaged with another piece of software. It would be a complete win if we could package Agda with agda-writer and bring the cost of installation down to zero: just get it from the AppStore and viola!