Redundant error messages #4

New Issue

aniva · 2023-08-22T20:56:13-07:00

aniva commented

2023-08-22 20:56:13 -07:00

When the command is not known, the REPL gives this error:

-- Pantograph.lean

    let error: Commands.InteractionError :=
      { error := "unknown", desc := s!"Unknown command {cmd}" }

This should be classified as a parsing error so we do not create more error categories

When the command is not known, the REPL gives this error: ```lean -- Pantograph.lean let error: Commands.InteractionError := { error := "unknown", desc := s!"Unknown command {cmd}" } ``` This should be classified as a parsing error so we do not create more error categories

aniva added this to the 0.2.6 milestone 2023-08-22 20:56:13 -07:00

aniva added the

category

doc

label 2023-08-22 20:56:13 -07:00

aniva self-assigned this 2023-08-22 20:56:13 -07:00

aniva added reference misc/cleanup

2023-08-23 13:15:21 -07:00

aniva commented

2023-08-23 13:16:07 -07:00

This error category and json error have been consolidated into one command error, used to indicate an error that makes it impossible to proceed to any individual command function.

This error category and `json` error have been consolidated into one `command` error, used to indicate an error that makes it impossible to proceed to any individual command function.

aniva referenced this issue

2023-08-23 13:21:36 -07:00

Remove dead code and consolidate error types #5

aniva closed this issue

2023-08-23 13:22:30 -07:00

Sign in to join this conversation.