|
|
|
|
Synopsis |
|
|
|
Documentation |
|
|
Constructors | State | | theTCState :: TCState | | theInteractionPoints :: [InteractionId] | The interaction points of the buffer, in the order in which
they appear in the buffer. The interaction points are
recorded in theTCState, but when new interaction points are
added by give or refine Agda does not ensure that the ranges
of later interaction points are updated.
| theCurrentFile :: Maybe (AbsolutePath, ClockTime) | The file which the state applies to. Only stored if the
module was successfully type checked (potentially with
warnings). The ClockTime is the modification time stamp of
the file when it was last loaded.
|
|
|
|
|
|
|
|
|
|
An interactive computation.
| Constructors | Interaction | | isIndependent :: Bool | Can the command run even if the relevant file has not been
loaded into the state?
| command :: TCM (Maybe ModuleName) | If a module name is returned, then syntax highlighting
information will be written for the given module (by ioTCM).
|
|
|
|
|
|
Run a TCM computation in the current state. Should only
be used for debugging.
|
|
|
:: FilePath | The current file. If this file does not match
theCurrentFile, and the Interaction is not
"independent", then an error is raised.
| -> Maybe FilePath | Syntax highlighting information will be written to this
file, if any.
| -> Interaction | | -> IO () | | Runs a TCM computation. All calls from the Emacs mode should be
wrapped in this function.
|
|
|
|
cmd_load m includes loads the module in file m, using
includes as the include directories.
|
|
|
:: FilePath | | -> [FilePath] | | -> Bool | Allow unsolved meta-variables?
| -> (Interface, Maybe Warnings) -> TCM () | | -> Interaction | | cmd_load' m includes cmd cmd2 loads the module in file m,
using includes as the include directories.
If type checking completes without any exceptions having been
encountered then the command cmd r is executed, where r is the
result of typeCheck.
|
|
|
|
cmd_compile m includes compiles the module in file m, using
includes as the include directories.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Sorts interaction points based on their ranges.
|
|
|
Pretty-prints the type of the meta-variable.
|
|
|
|
|
|
prettyContext lays out n : e on (at least) two lines if n
has at least longNameLength characters.
|
|
|
|
|
|
|
Displays the current goal and context plus the given document.
Displays the current goal and context.
|
|
|
Displays the current goal and context and infers the type of an
expression.
|
|
|
Sets the command line options and updates the status information.
|
|
|
Status information.
| Constructors | Status | | sShowImplicitArguments :: Bool | Are implicit arguments displayed?
| sChecked :: Bool | Has the module been successfully type checked?
|
|
|
|
|
|
Computes some status information.
|
|
|
Shows status information.
|
|
|
Displays/updates status information.
|
|
|
display_info' header content displays content (with header
header) in some suitable way.
|
|
|
display_info does what display_info' does, but additionally
displays some status information (see status and
displayStatus).
|
|
|
Like display_info, but takes a Doc instead of a String.
|
|
|
Formats a response command.
|
|
|
Formats a response string.
|
|
|
Responds to a query.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
:: Expr -> TCM Expr | The command to perform.
| -> String | The name to used for the buffer displaying the output.
| -> String | The expression to parse.
| -> Interaction | | Parses and scope checks an expression (using the "inside scope"
as the scope), performs the given command with the expression as
input, and displays the result.
|
|
|
|
:: Rewrite | Normalise the type?
| -> String | | -> Interaction | | Parse the given expression (as if it were defined at the
top-level of the current module) and infer its type.
|
|
|
|
:: Bool | Ignore abstract?
| -> String | | -> Interaction | | Parse and type check the given expression (as if it were defined
at the top-level of the current module) and normalise it.
|
|
|
|
cmd_write_highlighting_info source target writes syntax
highlighting information for the module in source into target.
If the module does not exist, or its module name is malformed or
cannot be determined, or the module has not already been visited,
or the cached info is out of date, then the representation of "no
highlighting information available" is instead written to
target.
|
|
|
:: FilePath | If the module name in this file does not match that
of the current module (or the module name cannot be
determined), then an empty list of goals is returned.
| -> Interaction | | Returns the interaction ids for all goals in the current module,
in the order in which they appear in the module. If there is no
current module, then an empty list of goals is returned.
|
|
|
|
Tells the Emacs mode to go to the first error position (if any).
|
|
|
:: Bool | Show them?
| -> Interaction | | Tells Agda whether or not to show implicit arguments.
|
|
|
|
Toggle display of implicit arguments.
|
|
|
When an error message is displayed the following title should be
used, if appropriate.
|
|
|
:: | | => Status | | -> Range | | -> String | | -> IO a | | Displays an error, instructs Emacs to jump to the site of the
error, and terminates the program. Because this function may switch
the focus to another file the status information is also updated.
|
|
|
module Agda.TypeChecker |
|
module Agda.TypeChecking.MetaVars |
|
module Agda.TypeChecking.Reduce |
|
module Agda.TypeChecking.Errors |
|
module Agda.Syntax.Position |
|
module Agda.Syntax.Parser |
|
module Agda.Syntax.Scope.Base |
|
module Agda.Syntax.Scope.Monad |
|
module Agda.Syntax.Translation.ConcreteToAbstract |
|
module Agda.Syntax.Translation.AbstractToConcrete |
|
module Agda.Syntax.Translation.InternalToAbstract |
|
module Agda.Syntax.Abstract.Name |
|
module Agda.Interaction.Exceptions |
|
|
Constructs AbsolutePaths.
Precondition: The path must be absolute.
|
|
Produced by Haddock version 2.6.0 |