diff --git a/asai/Asai/Diagnostic/index.html b/asai/Asai/Diagnostic/index.html index 0b65023..77b65f6 100644 --- a/asai/Asai/Diagnostic/index.html +++ b/asai/Asai/Diagnostic/index.html @@ -1,5 +1,5 @@ -Diagnostic (asai.Asai.Diagnostic)

Module Asai.Diagnostic

The definition of diagnostics and some utility functions.

Types

type severity =
  1. | Hint
  2. | Info
  3. | Warning
  4. | Error
  5. | Bug

The type of severity.

module type Code = sig ... end

The signature of message code. An implementer should specify the message code used in their library or application.

type text = Stdlib.Format.formatter -> unit

The type of text.

When we render a diagnostic, the layout engine of the rendering backend should be the one making layout choices. Therefore, we cannot pass already formatted strings. Instead, a text is defined to be a function that takes a formatter and uses it to render the content. The following two conditions must be satisfied:

  1. All string (and character) literals must be encoded using UTF-8.
  2. All string (and character) literals must not contain control characters (such as the newline character \n). It is okay to have break hints (such as @, and @ ) but not literal control characters. This means you should avoid pre-formatted strings, and if you must use them, use text to convert newline characters. Control characters include `U+0000-001F` (C0 controls), `U+007F` (backspace) and `U+0080-009F` (C1 controls). These characters are banned because they would mess up the cursor position.

Pro-tip: to format a text in another text, use %t:

let t2 = textf "@[<2>The network doesn't seem to work:@ %t@]" t1
type message = text Span.located

A message is a located text.

type backtrace = message Bwd.bwd

A backtrace is a (backward) list of messages.

type 'code t = {
  1. severity : severity;
    (*

    Severity of the diagnostic.

    *)
  2. code : 'code;
    (*

    The message code.

    *)
  3. message : message;
    (*

    The main message.

    *)
  4. backtrace : backtrace;
    (*

    The backtrace leading to this diagnostic.

    *)
  5. additional_messages : message list;
    (*

    Additional messages relevant to the main message that are not part of the backtrace.

    *)
}

The type of diagnostics.

Constructing Messages

val text : string -> text

text str converts the string str into a text, converting each '\n' into a call to Format.pp_force_newline.

val textf : ('a, Stdlib.Format.formatter, unit, text) Stdlib.format4 -> 'a

textf format ... constructs a text. It is an alias of Format.dprintf. Note that there should not be any literal control characters (e.g., literal newline characters).

val ktextf : +Diagnostic (asai.Asai.Diagnostic)

Module Asai.Diagnostic

The definition of diagnostics and some utility functions.

Types

type severity =
  1. | Hint
    (*

    This corresponds to the Hint severity level from LSP (Language Server Protocol). The official specification did not give much guidance on the difference between this level and Info. However, according to the LSP developers, "the idea of the hint severity" is that "for example we in VS Code don't render in the UI as squiggles." They are often used to indicate code smell, along with edit suggestions to fix it.

    *)
  2. | Info
    (*

    This corresponds to the Information severity level from LSP (Language Server Protocol). The official specification did not give much guidance on the difference between this level and Hint.

    *)
  3. | Warning
    (*

    Something went wrong or looked suspicious, but the end user (the user of your proof assistant or compiler) may choose to ignore the issue. For example, maybe some named arguments were not used in a definition.

    *)
  4. | Error
    (*

    A serious error caused by the end user (the user of your proof assistant or compiler) or other external factors (e.g., internet not working).

    *)
  5. | Bug
    (*

    A serious error likely caused by a bug in the proof assistant. You would want the end user to report the bug back to you. This is useful for indicating that certain branches in a pattern matching should be "impossible", while printing out debugging information in case the program logic is flawed.

    *)

The type of severity.

type text = Stdlib.Format.formatter -> unit

The type of text.

When we render a diagnostic, the layout engine of the rendering backend should be the one making layout choices. Therefore, we cannot pass already formatted strings. Instead, a text is defined to be a function that takes a formatter and uses it to render the content. The following two conditions must be satisfied:

  1. All string (and character) literals must be encoded using UTF-8.
  2. All string (and character) literals must not contain control characters (such as the newline character \n). It is okay to have break hints (such as @, and @ ) but not literal control characters. This means you should avoid pre-formatted strings, and if you must use them, use text to convert newline characters. Control characters include `U+0000-001F` (C0 controls), `U+007F` (backspace) and `U+0080-009F` (C1 controls). These characters are banned because they would mess up the cursor position.

Pro-tip: to format a text in another text, use %t:

let t2 = textf "@[<2>The network doesn't seem to work:@ %t@]" t1
type message = text Span.located

A message is a located text.

type backtrace = message Bwd.bwd

A backtrace is a (backward) list of messages.

type 'code t = {
  1. severity : severity;
    (*

    Severity of the diagnostic.

    *)
  2. code : 'code;
    (*

    The message code.

    *)
  3. message : message;
    (*

    The main message.

    *)
  4. backtrace : backtrace;
    (*

    The backtrace leading to this diagnostic.

    *)
  5. additional_messages : message list;
    (*

    Additional messages relevant to the main message that are not part of the backtrace.

    *)
}

The type of diagnostics.

Constructing Messages

val text : string -> text

text str converts the string str into a text, converting each '\n' into a call to Format.pp_force_newline.

val textf : ('a, Stdlib.Format.formatter, unit, text) Stdlib.format4 -> 'a

textf format ... constructs a text. It is an alias of Format.dprintf. Note that there should not be any literal control characters (e.g., literal newline characters).

val ktextf : (text -> 'b) -> ('a, Stdlib.Format.formatter, unit, 'b) Stdlib.format4 -> 'a

ktextf kont format ... is kont (textf code format ...). It is an alias of Format.kdprintf.

val message : ?loc:Span.t -> string -> message

message str converts the string str into a message.

  • parameter loc

    The location of the message (usually the code) to highlight.

val messagef : diff --git a/asai/Asai/Diagnostic/module-type-Code/index.html b/asai/Asai/Diagnostic/module-type-Code/index.html deleted file mode 100644 index 3aea99b..0000000 --- a/asai/Asai/Diagnostic/module-type-Code/index.html +++ /dev/null @@ -1,2 +0,0 @@ - -Code (asai.Asai.Diagnostic.Code)

Module type Diagnostic.Code

The signature of message code. An implementer should specify the message code used in their library or application.

type t

The type of all message codes.

val default_severity : t -> severity

The default severity of the code. The severity of a message is about whether the message is an error or a warning, etc. To clarify, it is about how serious the message is to the end user, not whether the program should stop or continue. The severity may be overwritten at the time of issuing a message to the end user.

val to_string : t -> string

A concise, ideally Google-able string representation of each message code. Detailed or long descriptions of code should be avoided. For example, E001 works better than type-checking error. The shorter, the better. It will be assumed that the string representation only uses ASCII printable characters.

diff --git a/asai/Asai/GitHub/Make/index.html b/asai/Asai/GitHub/Make/index.html index 2db6696..b4ed87b 100644 --- a/asai/Asai/GitHub/Make/index.html +++ b/asai/Asai/GitHub/Make/index.html @@ -1,2 +1,2 @@ -Make (asai.Asai.GitHub.Make)

Module GitHub.Make

The functor to create a printer for GitHub Actions workflow commands.

Parameters

Signature

val print : Code.t Diagnostic.t -> unit

Print a diagnostic as a GitHub Actions workflow command. Only the main message will be printed; backtraces and additional messages are ignored.

Example output:

::error file=examples/stlc/example.lambda,line=2,endLine=2,title=E002::Variable 'x' is not in scope
+Make (asai.Asai.GitHub.Make)

Module GitHub.Make

The functor to create a printer for GitHub Actions workflow commands.

Parameters

Signature

val print : Code.t Diagnostic.t -> unit

Print a diagnostic as a GitHub Actions workflow command. Only the main message will be printed; backtraces and additional messages are ignored.

Example output:

::error file=examples/stlc/example.lambda,line=2,endLine=2,title=E002::Variable 'x' is not in scope
diff --git a/asai/Asai/GitHub/index.html b/asai/Asai/GitHub/index.html index 55490c3..3b76faa 100644 --- a/asai/Asai/GitHub/index.html +++ b/asai/Asai/GitHub/index.html @@ -1,2 +1,2 @@ -GitHub (asai.Asai.GitHub)

Module Asai.GitHub

GitHub Actions workflow commands.

  • alert unstable The GitHub Actions backend will likely change significantly in the future to account for more features.
module Make (Code : Diagnostic.Code) : sig ... end

The functor to create a printer for GitHub Actions workflow commands.

+GitHub (asai.Asai.GitHub)

Module Asai.GitHub

GitHub Actions workflow commands.

  • alert unstable The GitHub Actions backend will likely change significantly in the future to account for more features.
module Make (Code : Reporter.Code) : sig ... end

The functor to create a printer for GitHub Actions workflow commands.

diff --git a/asai/Asai/Lsp/Make/index.html b/asai/Asai/Lsp/Make/index.html index 996d6d1..c5cc48a 100644 --- a/asai/Asai/Lsp/Make/index.html +++ b/asai/Asai/Lsp/Make/index.html @@ -1,5 +1,5 @@ -Make (asai.Asai.Lsp.Make)

Module Lsp.Make

This module provides a rudimentary and incomplete implementation of the LSP protocol.

Note: many features are missing and it does not handle positionEncoding.

Parameters

Signature

val start : +Make (asai.Asai.Lsp.Make)

Module Lsp.Make

This module provides a rudimentary and incomplete implementation of the LSP protocol.

Note: many features are missing and it does not handle positionEncoding.

Parameters

Signature

val start : source:string option -> init:(root:string option -> unit) -> load_file:(display:(Code.t Diagnostic.t -> unit) -> string -> unit) -> diff --git a/asai/Asai/Lsp/index.html b/asai/Asai/Lsp/index.html index bff2cae..f654b40 100644 --- a/asai/Asai/Lsp/index.html +++ b/asai/Asai/Lsp/index.html @@ -1,2 +1,2 @@ -Lsp (asai.Asai.Lsp)

Module Asai.Lsp

An LSP (Language Service Protocol) server for asai

  • alert unstable The LSP backend may change significantly in the future.

Language Service Protocol

module Make (Code : Diagnostic.Code) : sig ... end

This module provides a rudimentary and incomplete implementation of the LSP protocol.

+Lsp (asai.Asai.Lsp)

Module Asai.Lsp

An LSP (Language Service Protocol) server for asai

  • alert unstable The LSP backend may change significantly in the future.

Language Service Protocol

module Make (Code : Reporter.Code) : sig ... end

This module provides a rudimentary and incomplete implementation of the LSP protocol.

diff --git a/asai/Asai/Reporter/Make/index.html b/asai/Asai/Reporter/Make/index.html index de8d28c..4adc3fe 100644 --- a/asai/Asai/Reporter/Make/index.html +++ b/asai/Asai/Reporter/Make/index.html @@ -1,5 +1,5 @@ -Make (asai.Asai.Reporter.Make)

Module Reporter.Make

The functor to generate a logger.

Parameters

Signature

Sending Messages

val emit : +Make (asai.Asai.Reporter.Make)

Module Reporter.Make

The functor to generate a logger.

Parameters

module Code : Code

Signature

Sending Messages

val emit : ?severity:Diagnostic.severity -> ?loc:Span.t -> ?backtrace:Diagnostic.backtrace -> diff --git a/asai/Asai/Reporter/index.html b/asai/Asai/Reporter/index.html index 0edd9c5..ca98421 100644 --- a/asai/Asai/Reporter/index.html +++ b/asai/Asai/Reporter/index.html @@ -1,2 +1,2 @@ -Reporter (asai.Asai.Reporter)

Module Asai.Reporter

Generating and handling diagnostics using algebraic effects.

module type S = sig ... end

The signature of a logger.

module Make (Code : Diagnostic.Code) : S with module Code := Code

The functor to generate a logger.

+Reporter (asai.Asai.Reporter)

Module Asai.Reporter

Generating and handling diagnostics using algebraic effects.

The signature of a logger.

module type Code = sig ... end

The signature of message code. An implementer should specify the message code used in their library or application.

module type S = sig ... end
module Make (Code : Code) : S with module Code := Code

The functor to generate a logger.

diff --git a/asai/Asai/Reporter/module-type-Code/index.html b/asai/Asai/Reporter/module-type-Code/index.html new file mode 100644 index 0000000..599bbb4 --- /dev/null +++ b/asai/Asai/Reporter/module-type-Code/index.html @@ -0,0 +1,2 @@ + +Code (asai.Asai.Reporter.Code)

Module type Reporter.Code

The signature of message code. An implementer should specify the message code used in their library or application.

type t

The type of all message codes.

val default_severity : t -> Diagnostic.severity

The default severity of the code. The severity of a message is about whether the message is an error or a warning, etc. To clarify, it is about how serious the message is to the end user, not whether the program should stop or continue. The severity may be overwritten at the time of issuing a message to the end user.

val to_string : t -> string

A concise, ideally Google-able string representation of each message code. Detailed or long descriptions of code should be avoided. For example, E001 works better than type-checking error. The shorter, the better. It will be assumed that the string representation only uses ASCII printable characters.

diff --git a/asai/Asai/Reporter/module-type-S/index.html b/asai/Asai/Reporter/module-type-S/index.html index 0013f3c..aa8ced5 100644 --- a/asai/Asai/Reporter/module-type-S/index.html +++ b/asai/Asai/Reporter/module-type-S/index.html @@ -1,5 +1,5 @@ -S (asai.Asai.Reporter.S)

Module type Reporter.S

The signature of a logger.

Sending Messages

val emit : +S (asai.Asai.Reporter.S)

Module type Reporter.S

module Code : Code

Sending Messages

val emit : ?severity:Diagnostic.severity -> ?loc:Span.t -> ?backtrace:Diagnostic.backtrace -> diff --git a/asai/Asai/Tty/Make/index.html b/asai/Asai/Tty/Make/index.html index 314cbbb..ae99eba 100644 --- a/asai/Asai/Tty/Make/index.html +++ b/asai/Asai/Tty/Make/index.html @@ -1,5 +1,5 @@ -Make (asai.Asai.Tty.Make)

Module Tty.Make

This module provides functions to display or interact with diagnostics in UNIX terminals.

Parameters

Signature

val display : +Make (asai.Asai.Tty.Make)

Module Tty.Make

This module provides functions to display or interact with diagnostics in UNIX terminals.

Parameters

Signature

val display : ?output:Stdlib.out_channel -> ?show_backtrace:bool -> ?line_breaking:[ `Unicode | `Traditional ] -> diff --git a/asai/Asai/Tty/index.html b/asai/Asai/Tty/index.html index 40333e6..b170f1a 100644 --- a/asai/Asai/Tty/index.html +++ b/asai/Asai/Tty/index.html @@ -1,2 +1,2 @@ -Tty (asai.Asai.Tty)

Module Asai.Tty

Diagnostic display for UNIX terminals.

Display

  • alert unstable The TTY backend will likely change significantly in the future to account for more features.
module Make (Code : Diagnostic.Code) : sig ... end

This module provides functions to display or interact with diagnostics in UNIX terminals.

+Tty (asai.Asai.Tty)

Module Asai.Tty

Diagnostic display for UNIX terminals.

Display

  • alert unstable The TTY backend will likely change significantly in the future to account for more features.
module Make (Code : Reporter.Code) : sig ... end

This module provides functions to display or interact with diagnostics in UNIX terminals.