Documentation

Displays the current goal, the given document, and the current context.

Should not modify the state.

cmd_load' file argv unsolvedOk cmd loads the module in file file, using argv as the command-line options.

If type checking completes without any exceptions having been encountered then the command cmd r is executed, where r is the result of typeCheckMain.

Opposite of liftIO for CommandM.

This function should only be applied to computations that are guaranteed not to raise any errors (except for IOExceptions).

Displays or updates status information.

Does not change the state.

display_info does what displayInfo False does, but additionally displays some status information (see status and displayStatus).

A "give"-like action (give, refine, etc).

give_gen force ii rng s give_ref mk_newtxt acts on interaction point ii occupying range rng, placing the new content given by string s, and replacing ii by the newly created interaction points in the state if safety checks pass (unless force is applied).

Do setup and error handling for a command.

Can the command run even if the relevant file has not been loaded into the state?

Creates a command queue, and forks a thread that writes commands to the queue. The queue is returned.

Interpret an interaction.

For each goal command specific to an InteractionPoint that comes with a Range for this interaction point we first synchronize this Range with the Range Agda has stored for the interaction meta. In general, we consider the Range sent with the command as more up-to-date than the the Range Agda has stored. This is because the editor keeps track of changes (that usually modify the position of interaction points), but Agda does not.

Some goal commands carry a Range for reasons of uniformity but do not use it. For those, we do not synchronize the range.

Lift a TCM action transformer to a CommandM action transformer.

Ditto, but restore state.

If the next command from the command queue is anything but an actual command, then the command is returned.

If the command is an IOTCM command, then the following happens: The given computation is applied to the command and executed. If an abort command is encountered (and acted upon), then the computation is interrupted, the persistent state and all options are restored, and some commands are sent to the frontend. If the computation was not interrupted, then its result is returned.

A Lens for oldInteractionScopes.

A Lens for theInteractionPoints.

Parses and scope checks an expression (using the "inside scope" as the scope), performs the given command with the expression as input, and returns the result and the time it takes.

Try to parse an expression generated by Auto and feed it to the continuation if successful. If unsuccessful, just report the solution via Info_Auto.

Put a response by the callback function given by stInteractionOutputCallback.

Run an IOTCM value, catch the exceptions, emit output

If an error happens the state of CommandM does not change, but stPersistent may change (which contains successfully loaded interfaces for example).

Shows all the top-level names in scope which mention all the given identifiers in their type.

Sets the command line options and updates the status information.

Shows all the top-level names in the given module, along with their types.

Solved goals already instantiated internally The second argument potentially limits it to one specific goal.

Sorts interaction points based on their ranges.

Computes some status information.

Does not change the state.

If given range is empty, get the range of the interaction point. Otherwise, set the range of the interaction point to the given range.

The idea is that the interaction frontend may have a more recent range for an interaction point (for example, if the user has edited the file since the last command was sent).

There may be frontends that do not send ranges (like the interaction test suite), so in that case get the range from the interaction point.

Tells the Emacs mode to go to the first error position (if any).

Tell to highlight the code using the given highlighting info (unless it is Nothing).

Should Resp_InteractionPoints be issued after the command has run?

Explain why something is in scope.

Set envCurrentPath to theCurrentFile, if any.