Jose.Headertype t = {alg : Jwa.alg;jwk : Jwk.public Jwk.t option;kid : string option;x5t : string option;x5t256 : string option;typ : string option;cty : string option;enc : Jwa.enc option;extra : (string * Yojson.Safe.t) list;}The header has the following properties:
alg Jwa.algjwk JSON Web Keykid Key ID - We currently always expect this to be there, this can change in the futurex5t X.509 Certificate SHA-1 Thumbprint -x5t#S256 X.509 Certificate SHA-256 Thumbprinttyp Typecty Content Type Not implementedval make_header :
+Header (jose.Jose.Header) Module Jose.Header
type t = {alg : Jwa.alg;jwk : Jwk.public Jwk.t option;kid : string option;x5t : string option;x5t256 : string option;typ : string option;cty : string option;enc : Jwa.enc option;extra : (string * Yojson.Safe.t) list;
}The header has the following properties:
alg Jwa.algjwk JSON Web Keykid Key ID - We currently always expect this to be there, this can change in the futurex5t X.509 Certificate SHA-1 Thumbprint -x5t#S256 X.509 Certificate SHA-256 Thumbprinttyp Typecty Content Type Not implemented
val make_header :
?typ:string ->
?alg:Jwa.alg ->
?enc:Jwa.enc ->
diff --git a/jose/Jose/Jwa/index.html b/jose/Jose/Jwa/index.html
index ff2980f..7905f66 100644
--- a/jose/Jose/Jwa/index.html
+++ b/jose/Jose/Jwa/index.html
@@ -1,2 +1,2 @@
-Jwa (jose.Jose.Jwa) Module Jose.Jwa
JSON Web Algorithm
type alg = [ | `RS256(*HMAC using SHA-256
*)| `HS256(*RSASSA-PKCS1-v1_5 using SHA-256
*)| `ES256(*ECDSA using P-256 and SHA-256
*)| `ES384(*ECDSA using P-384 and SHA-384
*)| `ES512(*ECDSA using P-521 and SHA-512
*)| `EdDSA| `RSA_OAEP(*RSAES OAEP using default parameters
*)| `RSA1_5(*RSA PKCS 1
*)| `None| `Unsupported of string
]RS256 and HS256 and none is currently the only supported algs for signature - RSA_OAEP is currently the only supported alg for encryption
val alg_to_string : alg -> stringval alg_of_string : string -> algval alg_to_json : alg -> Yojson.Safe.tval alg_of_json : Yojson.Safe.t -> algval kty_to_string : kty -> stringval kty_of_string : string -> ktytype enc = [ | `A128CBC_HS256(*AES_128_CBC_HMAC_SHA_256 authenticated encryption algorithm, https://tools.ietf.org/html/rfc7518#section-5.2.3
*)| `A256GCM(*AES GCM using 256-bit key
*)
]https://tools.ietf.org/html/rfc7518#section-5
val enc_to_string : enc -> stringval enc_of_string : string -> enc
+Jwa (jose.Jose.Jwa) Module Jose.Jwa
JSON Web Algorithm
type alg = [ | `RS256(*HMAC using SHA-256
*)| `HS256(*RSASSA-PKCS1-v1_5 using SHA-256
*)| `ES256(*ECDSA using P-256 and SHA-256
*)| `ES384(*ECDSA using P-384 and SHA-384
*)| `ES512(*ECDSA using P-521 and SHA-512
*)| `EdDSA| `RSA_OAEP(*RSAES OAEP using default parameters
*)| `RSA1_5(*RSA PKCS 1
*)| `None| `Unsupported of string
]RS256 and HS256 and none is currently the only supported algs for signature - RSA_OAEP is currently the only supported alg for encryption
val alg_to_string : alg -> stringval alg_of_string : string -> algval alg_to_json : alg -> Yojson.Safe.tval alg_of_json : Yojson.Safe.t -> algval kty_to_string : kty -> stringval kty_of_string : string -> ktytype enc = [ | `A128CBC_HS256(*AES_128_CBC_HMAC_SHA_256 authenticated encryption algorithm, https://tools.ietf.org/html/rfc7518#section-5.2.3
*)| `A256GCM(*AES GCM using 256-bit key
*)
]https://tools.ietf.org/html/rfc7518#section-5
val enc_to_string : enc -> stringval enc_of_string : string -> enc
diff --git a/jose/Jose/Jwe/index.html b/jose/Jose/Jwe/index.html
index 3df58de..09f6ebc 100644
--- a/jose/Jose/Jwe/index.html
+++ b/jose/Jose/Jwe/index.html
@@ -1,5 +1,5 @@
-Jwe (jose.Jose.Jwe) Module Jose.Jwe
type t = {header : Header.t;cek : string;(*Content Encryption Key
*)iv : string;(*Initialization Vector
*)payload : string;(*plaintext to be encrypted
*)aad : string option;(*Additional Authentication Data, for future use
*)
}A JWE ready for encryption
val make :
+Jwe (jose.Jose.Jwe) Module Jose.Jwe
type t = {header : Header.t;cek : string;(*Content Encryption Key
*)iv : string;(*Initialization Vector
*)payload : string;(*plaintext to be encrypted
*)aad : string option;(*Additional Authentication Data, for future use
*)
}A JWE ready for encryption
make header payload creates a JWE from a Header.t and the plaintext that you want to encrypt
val encrypt :
diff --git a/jose/Jose/Jwk/index.html b/jose/Jose/Jwk/index.html
index e105c61..32aac0f 100644
--- a/jose/Jose/Jwk/index.html
+++ b/jose/Jose/Jwk/index.html
@@ -1,5 +1,5 @@
-Jwk (jose.Jose.Jwk) Module Jose.Jwk
JSON Web Key
use will default to `Sig in all functions unless supplied
type pub_rsa = Mirage_crypto_pk.Rsa.pub jwkrsa represents a public JWK with kty `RSA and a Rsa.pub key
type priv_rsa = Mirage_crypto_pk.Rsa.priv jwkrsa represents a private JWK with kty `RSA and a Rsa.priv key
type oct = string jwkoct represents a JWK with kty `OCT and a string key.
oct will in most cases be a private key but there are some cases where it will be considered public, eg. if you parse a public JSON
type priv_es256 = Mirage_crypto_ec.P256.Dsa.priv jwkes256 represents a public JWK with kty `EC and a P256.pub key
type pub_es256 = Mirage_crypto_ec.P256.Dsa.pub jwkes256 represents a private JWK with kty `EC and a P256.priv key
type priv_es384 = Mirage_crypto_ec.P384.Dsa.priv jwkes384 represents a public JWK with kty `EC and a P384.pub key
type pub_es384 = Mirage_crypto_ec.P384.Dsa.pub jwkes384 represents a private JWK with kty `EC and a P384.priv key
type priv_es512 = Mirage_crypto_ec.P521.Dsa.priv jwkes512 represents a public JWK with kty `EC and a P512.pub key
type pub_es512 = Mirage_crypto_ec.P521.Dsa.pub jwkes512 represents a private JWK with kty `EC and a P512.priv key
type priv_ed25519 = Mirage_crypto_ec.Ed25519.priv jwked25519 represents a public JWK with kty `OKP and a Ed25519.pub key
type pub_ed25519 = Mirage_crypto_ec.Ed25519.pub jwked25519 represents a private JWK with kty `OKP and a Ed25519.priv key
type 'a t = | Oct : oct -> 'a t| Rsa_priv : priv_rsa -> priv t| Rsa_pub : pub_rsa -> public t| Es256_priv : priv_es256 -> priv t| Es256_pub : pub_es256 -> public t| Es384_priv : priv_es384 -> priv t| Es384_pub : pub_es384 -> public t| Es512_priv : priv_es512 -> priv t| Es512_pub : pub_es512 -> public t| Ed25519_priv : priv_ed25519 -> priv t| Ed25519_pub : pub_ed25519 -> public t
t describes a JSON Web Key which can be either public or private
Public keys
These keys are safe to show and should be used to verify signed content.
rsa_of_pub use pub takes a public key generated by Nocrypto and returns a result t or a message of what went wrong.
val of_pub_pem :
+Jwk (jose.Jose.Jwk) Module Jose.Jwk
JSON Web Key
use will default to `Sig in all functions unless supplied
type pub_rsa = Mirage_crypto_pk.Rsa.pub jwkrsa represents a public JWK with kty `RSA and a Rsa.pub key
type priv_rsa = Mirage_crypto_pk.Rsa.priv jwkrsa represents a private JWK with kty `RSA and a Rsa.priv key
type oct = string jwkoct represents a JWK with kty `OCT and a string key.
oct will in most cases be a private key but there are some cases where it will be considered public, eg. if you parse a public JSON
type priv_es256 = Mirage_crypto_ec.P256.Dsa.priv jwkes256 represents a public JWK with kty `EC and a P256.pub key
type pub_es256 = Mirage_crypto_ec.P256.Dsa.pub jwkes256 represents a private JWK with kty `EC and a P256.priv key
type priv_es384 = Mirage_crypto_ec.P384.Dsa.priv jwkes384 represents a public JWK with kty `EC and a P384.pub key
type pub_es384 = Mirage_crypto_ec.P384.Dsa.pub jwkes384 represents a private JWK with kty `EC and a P384.priv key
type priv_es512 = Mirage_crypto_ec.P521.Dsa.priv jwkes512 represents a public JWK with kty `EC and a P512.pub key
type pub_es512 = Mirage_crypto_ec.P521.Dsa.pub jwkes512 represents a private JWK with kty `EC and a P512.priv key
type priv_ed25519 = Mirage_crypto_ec.Ed25519.priv jwked25519 represents a public JWK with kty `OKP and a Ed25519.pub key
type pub_ed25519 = Mirage_crypto_ec.Ed25519.pub jwked25519 represents a private JWK with kty `OKP and a Ed25519.priv key
type 'a t = | Oct : oct -> 'a t| Rsa_priv : priv_rsa -> priv t| Rsa_pub : pub_rsa -> public t| Es256_priv : priv_es256 -> priv t| Es256_pub : pub_es256 -> public t| Es384_priv : priv_es384 -> priv t| Es384_pub : pub_es384 -> public t| Es512_priv : priv_es512 -> priv t| Es512_pub : pub_es512 -> public t| Ed25519_priv : priv_ed25519 -> priv t| Ed25519_pub : pub_ed25519 -> public t
t describes a JSON Web Key which can be either public or private
Public keys
These keys are safe to show and should be used to verify signed content.
rsa_of_pub use pub takes a public key generated by Nocrypto and returns a result t or a message of what went wrong.
val of_pub_pem :
?use:use ->
string ->
(public t, [> `Msg of string | `Unsupported_kty ]) Stdlib.resultof_pub_pem use pem takes a PEM as a string and returns a public t or a message of what went wrong.
val to_pub_pem :
diff --git a/jose/Jose/Jwks/index.html b/jose/Jose/Jwks/index.html
index 997dbf1..f83b099 100644
--- a/jose/Jose/Jwks/index.html
+++ b/jose/Jose/Jwks/index.html
@@ -1,2 +1,2 @@
-Jwks (jose.Jose.Jwks) Module Jose.Jwks
JSON Web Key Set
t describes a Private JSON Web Key Set
val to_json : t -> Yojson.Safe.tto_json t takes a t and returns a Yojson.Safe.t
val of_json : Yojson.Safe.t -> tof_json json takes a Yojson.Safe.t and returns a t. Keys that can not be serialized safely will be removed from the list
val of_string : string -> tof_string json_string takes a JSON string representation and returns a t. Keys that can not be serialized safely will be removed from the list
val to_string : t -> stringto_string t takes a t and returns a JSON string representation
val find_key : t -> string -> Jwk.public Jwk.t option
+Jwks (jose.Jose.Jwks) Module Jose.Jwks
JSON Web Key Set
t describes a Private JSON Web Key Set
val to_json : t -> Yojson.Safe.tto_json t takes a t and returns a Yojson.Safe.t
val of_json : Yojson.Safe.t -> tof_json json takes a Yojson.Safe.t and returns a t. Keys that can not be serialized safely will be removed from the list
val of_string : string -> tof_string json_string takes a JSON string representation and returns a t. Keys that can not be serialized safely will be removed from the list
val to_string : t -> stringto_string t takes a t and returns a JSON string representation
val find_key : t -> string -> Jwk.public Jwk.t option
diff --git a/jose/Jose/Jws/index.html b/jose/Jose/Jws/index.html
index 0f1b310..bea44af 100644
--- a/jose/Jose/Jws/index.html
+++ b/jose/Jose/Jws/index.html
@@ -1,5 +1,5 @@
-Jws (jose.Jose.Jws) Module Jose.Jws
JSON Web Signature
val of_string :
+Jws (jose.Jose.Jws) Module Jose.Jws
JSON Web Signature
val of_string :
string ->
(t, [> `Msg of string | `Not_json | `Not_supported ]) Stdlib.resultval to_string : ?serialization:serialization -> t -> stringval validate :
jwk:'a Jwk.t ->
diff --git a/jose/Jose/Jwt/index.html b/jose/Jose/Jwt/index.html
index a0a8669..7774193 100644
--- a/jose/Jose/Jwt/index.html
+++ b/jose/Jose/Jwt/index.html
@@ -1,5 +1,5 @@
-Jwt (jose.Jose.Jwt) Module Jose.Jwt
JSON Web Token
val empty_payload : payloadtype t = {header : Header.t;raw_header : string;payload : payload;raw_payload : string;signature : Jws.signature;
}val get_yojson_claim : t -> string -> Yojson.Safe.t optionval get_string_claim : t -> string -> string optionval get_int_claim : t -> string -> int optionval to_string : ?serialization:Jws.serialization -> t -> stringval of_string :
+Jwt (jose.Jose.Jwt) Module Jose.Jwt
JSON Web Token
val empty_payload : payloadtype t = {header : Header.t;raw_header : string;payload : payload;raw_payload : string;signature : Jws.signature;
}val get_yojson_claim : t -> string -> Yojson.Safe.t optionval get_string_claim : t -> string -> string optionval get_int_claim : t -> string -> int optionval to_string : ?serialization:Jws.serialization -> t -> stringval of_string :
jwk:'a Jwk.t ->
now:Ptime.t ->
string ->
diff --git a/jose/Jose/index.html b/jose/Jose/index.html
index 13b5cbf..cd11be6 100644
--- a/jose/Jose/index.html
+++ b/jose/Jose/index.html
@@ -1,2 +1,2 @@
-Jose (jose.Jose) Module Jose
module Jwa : sig ... endmodule Jwk : sig ... endmodule Jwks : sig ... endmodule Header : sig ... endmodule Jws : sig ... endmodule Jwt : sig ... endmodule Jwe : sig ... end
+Jose (jose.Jose) Module Jose
module Jwa : sig ... endmodule Jwk : sig ... endmodule Jwks : sig ... endmodule Header : sig ... endmodule Jws : sig ... endmodule Jwt : sig ... endmodule Jwe : sig ... end
diff --git a/jose/index.html b/jose/index.html
index d1df89a..196535b 100644
--- a/jose/index.html
+++ b/jose/index.html
@@ -1,2 +1,2 @@
-index (jose.index) jose index
Library jose
The entry point of this library is the module: Jose.
+index (jose.index) jose index
Library jose
The entry point of this library is the module: Jose.
diff --git a/odoc.support/odoc.css b/odoc.support/odoc.css
index f0f22a1..1b0bb98 100644
--- a/odoc.support/odoc.css
+++ b/odoc.support/odoc.css
@@ -1,7 +1,7 @@
@charset "UTF-8";
/* Copyright (c) 2016 The odoc contributors. All rights reserved.
Distributed under the ISC license, see terms at the end of the file.
- odoc 2.4.4 */
+ odoc 3.0.0_beta1 */
/* Fonts */
/* noticia-text-regular - latin */
@@ -98,138 +98,163 @@
scroll-padding-top: calc(var(--search-bar-height) + var(--search-padding-top) + 1em);
- --main-background: #FFFFFF;
-
- --color: #333333;
- --link-color: #2C94BD;
- --source-color: grey;
- --anchor-hover: #555;
- --anchor-color: #d5d5d5;
- --xref-shadow: #cc6666;
- --header-shadow: #ddd;
- --by-name-version-color: #aaa;
- --by-name-nav-link-color: #222;
- --target-background: rgba(187, 239, 253, 0.3);
- --target-shadow: rgba(187, 239, 253, 0.8);
- --pre-border-color: #eee;
- --code-background: #f6f8fa;
-
- --li-code-background: #f6f8fa;
- --li-code-color: #0d2b3e;
- --toc-color: #1F2D3D;
- --toc-before-color: #777;
- --toc-background: #f6f8fa;
- --toc-background-emph: #ecf0f5;
- --toc-list-border: #ccc;
-
- --spec-summary-border-color: #5c9cf5;
- --spec-label-color: green;
- --spec-summary-background: var(--code-background);
- --spec-summary-hover-background: #ebeff2;
- --spec-details-after-background: rgba(0, 4, 15, 0.05);
- --spec-details-after-shadow: rgba(204, 204, 204, 0.53);
-
- --search-results-border: #bbb;
- --search-results-shadow: #bbb;
-
- --search-snake: #82aaff;
+ /* light gruvbox theme colors */
+ --bg_h: #f9f5d7;
+ --bg: #f6f8fa; /*#fbf1c7;*/
+ --bg_s: #f2e5bc;
+ --bg1: #ebdbb2;
+ --bg2: #d5c4a1;
+ --bg3: #bdae93;
+ --bg4: #a89984;
+
+ --fg: #282828;
+ --fg1: #3c3836;
+ --fg2: #504945;
+ --fg3: #665c54;
+ --fg4: #7c6f64;
+
+ --red: #9d0006;
+ --green: #79740e;
+ --yellow: #b57614;
+ --blue: #076678;
+ --purple: #8f3f71;
+ --aqua: #427b58;
+ --orange: #af3a03;
+ --gray: #928374;
+
+ --red-dim: #cc2412;
+ --green-dim: #98971a;
+ --yellow-dim: #d79921;
+ --blue-dim: #458598;
+ --purple-dim: #b16286;
+ --aqua-dim: #689d6a;
+ --orange-dim: #d65d0e;
+ --gray-dim: #7c6f64;
+
+ /* odoc colors */
+ --odoc-blue: #5c9cf5;
+ --odoc-bg: #FFFFFF;
+ --odoc-bg1: #f6f8fa;
+ --odoc-fg: #333333;
+ --odoc-fg1: #1F2D3D;
}
-.dark:root {
- --main-background: #202020;
- --code-background: #222;
- --line-numbers-background: rgba(0, 0, 0, 0.125);
- --navbar-background: #202020;
-
- --color: #bebebe;
- --dirname-color: #666;
- --underline-color: #444;
- --visited-color: #002800;
- --visited-number-color: #252;
- --unvisited-color: #380000;
- --unvisited-number-color: #622;
- --somevisited-color: #303000;
- --highlight-color: #303e3f;
- --line-number-color: rgba(230, 230, 230, 0.3);
- --unvisited-margin-color: #622;
- --border: #333;
- --navbar-border: #333;
- --code-color: #ccc;
-
- --li-code-background: #373737;
- --li-code-color: #999;
- --toc-color: #777;
- --toc-background: #252525;
- --toc-background-emph: #2a2a2a;
-
- --hljs-link: #999;
- --hljs-keyword: #cda869;
- --hljs-regexp: #f9ee98;
- --hljs-title: #dcdcaa;
- --hljs-type: #ac885b;
- --hljs-meta: #82aaff;
- --hljs-variable: #cf6a4c;
-
- --spec-label-color: lightgreen;
+@media (prefers-color-scheme: dark) {
+ :root {
+ /* dark gruvbox theme colors */
+ --bg_h: #1d2021;
+ --bg: #282828;
+ --bg_s: #32302f;
+ --bg1: #3c3836;
+ --bg2: #504945;
+ --bg3: #665c54;
+ --bg4: #7c6f64;
+
+ --fg: #fbf1c7;
+ --fg1: #ebdbb2;
+ --fg2: #d5c4a1;
+ --fg3: #bdae93;
+ --fg4: #a89984;
+
+ --red: #fb4934;
+ --green: #b8bb26;
+ --yellow: #fabd2f;
+ --blue: #83a598;
+ --purple: #d3869b;
+ --aqua: #8ec07c;
+ --gray: #928374;
+ --orange: #fe8019;
+
+ --red-dim: #cc2412;
+ --green-dim: #98971a;
+ --yellow-dim: #d79921;
+ --blue-dim: #458588;
+ --purple-dim: #b16286;
+ --aqua-dim: #689d6a;
+ --gray-dim: #a89984;
+ --orange-dim: #d65d0e;
+
+ /* odoc colors */
+ --odoc-blue: #5c9cf5;
+ --odoc-bg: #202020;
+ --odoc-bg1: #252525;
+ --odoc-fg: #bebebe;
+ --odoc-fg1: #777;
+ }
+}
- --search-results-border: #505050;
- --search-results-shadow: #404040;
+:root {
+ --main-background: var(--odoc-bg);
+ --color: var(--odoc-fg);
+ --anchor-hover: var(--fg1);
+ --anchor-color: var(--bg2);
+ --xref-shadow: var(--red-dim);
+ --xref-unresolved: var(--blue-dim);
+ --header-shadow: var(--bg3);
+ --by-name-version-color: var(--bg4);
+ --by-name-nav-link-color: var(--fg2);
+ --target-background: color-mix(in srgb, var(--main-background) 70%, var(--odoc-blue) 30%);
+ --target-border: var(--odoc-blue);
+ --pre-border-color: var(--fg4);
+ --link-color: var(--odoc-blue);
+ --source-link-color: var(--fg4);
+
+
+ --toc-color: var(--fg);
+ --toc-before-color: var(--odoc-fg1);
+ --toc-background: var(--odoc-bg1);
+ --toc-list-border: var(--fg1);
+
+ --hljs-bg: var(--code-background);
+ --hljs-link: var(--fg2);
+ --source-code-keyword: var(--orange);
+ --hljs-regexp: var(--yellow);
+ --hljs-title: var(--yellow-dim);
+
+ --spec-label-color: var(--aqua);
+ --spec-summary-background: var(--code-background);
+ --spec-summary-border-color: var(--odoc-blue);
+ --spec-summary-hover-background: var(--odoc-bg1);
+ --spec-details-after-background: var(--odoc-bg1);
+ --spec-details-after-border: var(--fg3);
+ --search-results-border: var(--fg1);
+ --search-results-shadow: var(--bg3);
+ --search-highlight-color: var(--odoc-blue);
+ --search-snake-color: var(--odoc-blue);
+ /* code colors */
+ --code-color: var(--fg);
+ --code-background: var(--bg);
+ --li-code-background: var(--bg);
+ --li-code-color: var(--fg);
+
+
+ --source-line-column: var(--fg3);
+ --source-line-column-bg: var(--bg_h);
+
+ --source-code-comment: var(--gray);
+ --source-code-docstring: var(--green-dim);
+ --source-code-lident: var(--fg1);
+ --source-code-uident: var(--blue);
+ --source-code-literal: var(--yellow);
+ --source-code-keyword: var(--red);
+ --source-code-underscore: var(--fg3);
+ --source-code-operator: var(--purple);
+ --source-code-parens: var(--orange-dim);
+ --source-code-separator: var(--orange-dim);
+
+ --hljs-variable: var(--yellow);
+ --hljs-literal: var(--red);
+ --hljs-name: var(--green-dim);
+ --hljs-tag: var(--fg4);
+ --hljs-attr: var(--purple);
+ --hljs-addition: var(--green-dim);
+ --hljs-addition-bg: color-mix(in srgb, var(--hljs-addition) 10%, var(--hljs-bg) 90%);
+ --hljs-deletion: var(--red-dim);
+ --hljs-deletion-bg: color-mix(in srgb, var(--hljs-deletion) 10%, var(--hljs-bg) 90%);
-}
-@media (prefers-color-scheme: dark) {
- :root {
- --main-background: #202020;
- --code-background: #333;
- --line-numbers-background: rgba(0, 0, 0, 0.125);
- --navbar-background: #202020;
-
- --meter-unvisited-color: #622;
- --meter-visited-color: #252;
- --meter-separator-color: black;
-
- --color: #bebebe;
- --dirname-color: #666;
- --underline-color: #444;
- --visited-color: #002800;
- --visited-number-color: #252;
- --unvisited-color: #380000;
- --unvisited-number-color: #622;
- --somevisited-color: #303000;
- --highlight-color: #303e3f;
- --line-number-color: rgba(230, 230, 230, 0.3);
- --unvisited-margin-color: #622;
- --border: #333;
- --navbar-border: #333;
- --code-color: #ccc;
- --by-name-nav-link-color: var(--color);
-
- --li-code-background: #373737;
- --li-code-color: #999;
- --toc-color: #777;
- --toc-before-color: #777;
- --toc-background: #252525;
- --toc-background-emph: #2a2a2a;
- --toc-list-border: #ccc;
- --spec-summary-hover-background: #ebeff2;
- --spec-details-after-background: rgba(0, 4, 15, 0.05);
- --spec-details-after-shadow: rgba(204, 204, 204, 0.53);
-
- --hljs-link: #999;
- --hljs-keyword: #cda869;
- --hljs-regexp: #f9ee98;
- --hljs-title: #dcdcaa;
- --hljs-type: #ac885b;
- --hljs-meta: #82aaff;
- --hljs-variable: #cf6a4c;
-
- --spec-label-color: lightgreen;
-
- --search-results-border: #505050;
- --search-results-shadow: #404040;
- }
}
/* Reset a few things. */
@@ -258,7 +283,6 @@ html {
body {
text-align: left;
- background: #FFFFFF;
color: var(--color);
background-color: var(--main-background);
font-family: "Noticia Text", Georgia, serif;
@@ -269,23 +293,69 @@ body {
margin-left: auto;
margin-right: auto;
padding: 0 4ex;
+ margin-top: 0;
}
body.odoc {
- max-width: 132ex;
+ max-width: 181ex;
display: grid;
- grid-template-columns: min-content 1fr;
+ grid-template-columns: min-content 1fr min-content;
+ grid-template-areas:
+ "search-bar nav ."
+ "toc-global preamble toc-local"
+ "toc-global content toc-local";
column-gap: 4ex;
- row-gap: 2ex;
+ grid-template-rows: auto auto 1fr;
+}
+
+body.odoc:has(> .odoc-search:focus-within) {
+ grid-template-areas:
+ "search-bar search-bar search-bar"
+ ". nav ."
+ "toc-global preamble toc-local"
+ "toc-global content toc-local";
+}
+
+body.odoc:not(:has(> .odoc-tocs .odoc-global-toc)) {
+ grid-template-areas:
+ "search-bar search-bar"
+ "nav ."
+ "preamble toc-local"
+ "content toc-local";
+ grid-template-columns: 1fr min-content;
+}
+
+/* When there is no global sidebar */
+body.odoc:not(:has(> .odoc-tocs .odoc-global-toc)) nav.odoc-nav {
+ padding-top: 0;
+}
+
+/* When there is no global sidebbar and the searchbar is focused */
+body.odoc:not(:has(> .odoc-tocs .odoc-global-toc)) nav.odoc-nav:has(+ .odoc-search:focus-within) {
+ padding-top: var(--search-padding-top);
+}
+
+nav.odoc-nav:has(+ .odoc-search:focus-within) {
+ padding-top: 0;
}
body.odoc-src {
- margin-right: calc(10vw + 20ex);
+ display: grid;
+ grid-template-columns: min-content 1fr;
+ grid-template-areas:
+ "search-bar nav "
+ "toc-global preamble"
+ "toc-global content ";
+ column-gap: 4ex;
+ grid-template-rows: auto auto 1fr;
}
.odoc-content {
- grid-row: 4;
- grid-column: 2;
+ grid-area: content;
+}
+
+.odoc-content > *:first-child {
+ margin-top: 0;
}
.odoc-preamble > *:first-child {
@@ -294,13 +364,13 @@ body.odoc-src {
margin-top: 0;
}
-header {
+/* Add margin after the preamble if it contains more than one element. */
+header.odoc-preamble:has(> :nth-child(2)) {
margin-bottom: 30px;
}
header.odoc-preamble {
- grid-column: 2;
- grid-row: 3;
+ grid-area: preamble;
}
nav {
@@ -308,8 +378,9 @@ nav {
}
nav.odoc-nav {
- grid-column: 2;
- grid-row: 2;
+ grid-area: nav;
+ padding-top: var(--search-padding-top);
+ padding-bottom: var(--search-padding-top);
}
/* Basic markup elements */
@@ -385,15 +456,15 @@ a {
color: inherit;
}
-a:hover {
+a:hover:not(.img-link) {
box-shadow: 0 1px 0 0 var(--link-color);
}
/* Linked highlight */
-*:target {
+*:target, .current_unit {
background-color: var(--target-background) !important;
- box-shadow: 0 0px 0 1px var(--target-shadow) !important;
border-radius: 1px;
+ border: var(--target-border) 1px solid !important;
}
*:hover > a.anchor {
@@ -430,7 +501,7 @@ a.anchor {
}
.xref-unresolved {
- color: #2C94BD;
+ color: var(--xref-unresolved);
}
.xref-unresolved:hover {
box-shadow: 0 1px 0 0 var(--xref-shadow);
@@ -439,7 +510,7 @@ a.anchor {
/* Source links float inside preformated text or headings. */
a.source_link {
float: right;
- color: var(--source-color);
+ color: var(--source-link-color);
font-family: "Fira Sans", sans-serif;
font-size: initial;
}
@@ -652,7 +723,7 @@ div.def-doc>*:first-child {
bottom: 1px;
width: 15px;
background: var(--spec-details-after-background, rgba(0, 4, 15, 0.05));
- box-shadow: 0 0px 0 1px var(--spec-details-after-shadow, rgba(204, 204, 204, 0.53));
+ box-shadow: 0 0px 0 1px var(--spec-details-after-border, rgba(204, 204, 204, 0.53));
}
.odoc-include summary {
@@ -668,7 +739,7 @@ div.def-doc>*:first-child {
/* FIXME: Does not work in Firefox. */
.odoc-include summary::-webkit-details-marker {
- color: #888;
+ color: #888; /* todo : use color from palette */
transform: scaleX(-1);
position: absolute;
top: calc(50% - 5px);
@@ -701,7 +772,13 @@ td.def-doc *:first-child {
/* Alert emoji */
.alert::before, .deprecated::before {
- content: '⚠️ ';
+ content: '⚠️ ' / '';
+}
+
+/* Since emoji */
+
+.since::before {
+ content: '🕚 ' / '';
}
/* Lists of modules */
@@ -786,26 +863,43 @@ td.def-doc *:first-child {
line-height: 1.2;
}
+.odoc-toc.odoc-local-toc:before {
+ content: "Local content";
+
+}
+.odoc-toc.odoc-global-toc:before {
+ content: "Global content";
+}
+
/* When a search bar is present, we need the sticky sidebar to be a bit lower,
so `top` is higher */
-.odoc-search + * + .odoc-toc {
- --toc-top: calc(var(--search-bar-height) + var(--search-padding-top) + 20px);
+body.odoc:has( .odoc-search) .odoc-toc {
+ --toc-top: calc(var(--search-bar-height) + 2 * var(--search-padding-top));
max-height: calc(100vh - 2 * var(--toc-top));
top: var(--toc-top)
}
+.odoc-tocs {
+ display: contents;
+}
+
+.odoc-local-toc {
+ grid-area: toc-local;
+}
+
+.odoc-global-toc {
+ grid-area: toc-global;
+}
+
.odoc-toc {
--toc-top: 20px;
- width: 28ex;
+ width: 42ex;
background: var(--toc-background);
overflow: auto;
color: var(--toc-color);
padding-left: 2ex;
padding-right: 2ex;
- grid-row-start: 3;
- grid-row-end: 5;
- grid-column: 1;
height: fit-content;
border: solid 1px var(--border);
border-radius: 5px;
@@ -823,9 +917,29 @@ td.def-doc *:first-child {
display: block;
}
-.odoc-sidebar ul li a:hover {
- box-shadow: none;
- text-decoration: underline;
+.odoc-toc.odoc-global-toc > ul > li {
+ margin-left:0;
+}
+
+.odoc-toc.odoc-global-toc > ul > li > ul > li {
+ margin-left:0;
+ padding-left:0;
+ border: 0;
+ margin-top: 10px;
+ margin-bottom: 10px;
+}
+
+.odoc-toc.odoc-global-toc > ul > li > ul > li {
+ font-weight: 500;
+}
+
+.odoc-toc.odoc-global-toc > ul > li > ul > li > a {
+ font-weight: inherit;
+ font-size: inherit;
+}
+
+.odoc-toc.odoc-global-toc > ul > li > a {
+ font-size: 1.2em;
}
:root {
@@ -840,13 +954,13 @@ td.def-doc *:first-child {
/* This amounts to fit-content when the search is not active, but when you
have the search results displayed, you do not want the height of the search
container to change. */
- height: calc(var(--search-bar-height) + var(--search-padding-top));
+ height: calc(var(--search-bar-height) + 2 * var(--search-padding-top));
width: 100%;
padding-top: var(--search-padding-top);
+ padding-bottom: var(--search-padding-top);
z-index: 1;
- grid-row: 1;
- grid-column-start: 1;
- grid-column-end: 3;
+ grid-area: search-bar;
+
}
@@ -870,10 +984,30 @@ td.def-doc *:first-child {
transition: font-size 0.3s;
box-shadow: 0px 0px 0.2rem 0.3em var(--main-background);
height: var(--search-bar-height);
+ border: 1px solid var(--fg4);
+ /* inputs are of fixed size by default, even if you display:block them */
+ width: 100%;
+ color: var(--odoc-fg);
+ background: var(--odoc-bg1);
+ border-radius: 5px;
+ outline: none;
+}
+
+.odoc-search:focus-within {
+ width: 100%;
}
.odoc-search:focus-within .search-bar {
font-size: 1.1em;
+ border-color: var(--search-highlight-color);
+}
+
+.search-bar:focus-visible {
+ outline: 2px solid var(--search-highlight-color);
+}
+
+.search-bar::placeholder {
+ color: var(--fg3);
}
.odoc-search:not(:focus-within) .search-result {
@@ -900,11 +1034,6 @@ td.def-doc *:first-child {
overflow-y: auto;
}
-.search-bar {
- /* inputs are of fixed size by default, even if you display:block them */
- width: 100%;
-}
-
.odoc-search .search-no-result {
color: var(--color);
@@ -949,7 +1078,7 @@ td.def-doc *:first-child {
margin-right: 4px;
border-radius: 50%;
border: 3px solid #aaa;
- border-color: var(--search-snake) transparent var(--search-snake) transparent;
+ border-color: var(--search-snake-color) transparent var(--search-snake-color) transparent;
animation: search-snake 1.2s linear infinite;
position: absolute;
right: 0;
@@ -993,14 +1122,14 @@ td.def-doc *:first-child {
white-space: nowrap;
}
-.odoc-search .search-entry:focus-visible {
+.odoc-search .search-result .search-entry:focus-visible {
box-shadow: none;
background-color: var(--target-background);
}
.odoc-search .search-entry:hover {
box-shadow: none;
- background-color: var(--toc-background-emph);
+ background-color: var(--main-background);
}
.odoc-search .search-entry .entry-kind {
@@ -1021,8 +1150,8 @@ td.def-doc *:first-child {
.odoc-search .search-entry pre code {
font-size: 1em;
- background-color: var(--li-code-background);
- color: var(--li-code-color);
+ background-color: var(--code-background);
+ color: var(--code-color);
border-radius: 3px;
padding: 0 0.3ex;
}
@@ -1106,7 +1235,7 @@ td.def-doc *:first-child {
font-weight: 500;
}
-.odoc-toc li ul {
+.odoc-toc ul li ul {
margin: 0px;
padding-top: 0.25em;
}
@@ -1120,6 +1249,7 @@ td.def-doc *:first-child {
}
.odoc-toc>ul>li {
+ margin-left: 0;
margin-bottom: 0.3em;
}
@@ -1148,21 +1278,75 @@ td.def-doc *:first-child {
/* Mobile adjustements. */
+@media only screen and (max-width: 210ex) {
+ body.odoc {
+ max-width: 132ex;
+ grid-template-areas:
+ "search-bar nav"
+ "sidebar preamble"
+ "sidebar content";
+ }
+ body.odoc .odoc-tocs {
+ display: flex;
+ grid-area: sidebar;
+ flex-direction : column;
+ gap: 20px;
+ }
+ body.odoc .odoc-tocs .odoc-toc {
+ position: unset;
+ max-height: unset;
+ }
+ body.odoc:has(.odoc-search:focus-within) {
+ grid-template-areas:
+ "search-bar search-bar"
+ ". nav"
+ "sidebar preamble"
+ "sidebar content";
+ }
+}
+
@media only screen and (max-width: 110ex) {
- body {
+ body.odoc {
margin: 2em;
padding: 0;
+ grid-template-areas:
+ "search-bar"
+ "nav"
+ "preamble"
+ "toc-local"
+ "content"
+ "toc-global";
+ grid-template-columns: 1fr;
}
-
- body.odoc {
- display: block;
+ body.odoc:has(> .odoc-search:focus-within) {
+ /* This is the same as when there is no focus on the search bar, this is
+ just to prevent the default "wide layout" rule from changing anything. */
+ grid-template-areas:
+ "search-bar"
+ "nav"
+ "preamble"
+ "toc-local"
+ "content"
+ "toc-global";
+ grid-template-columns: 1fr;
}
-
- .odoc-toc {
+ body.odoc .odoc-search {
+ position: relative;
+ height: calc(var(--search-bar-height) + 2 * var(--search-padding-top));
+ }
+ body.odoc nav.odoc-nav {
+ padding-top: 0;
+ padding-bottom: var(--search-padding-top);
+ }
+ body.odoc .odoc-tocs {
+ display: contents;
+ }
+ body.odoc .odoc-tocs .odoc-toc {
position: static;
width: auto;
min-width: unset;
max-width: unset;
+ max-height: unset;
border: none;
padding: 0.2em 1em;
border-radius: 5px;
@@ -1187,12 +1371,15 @@ td.def-doc *:first-child {
.source_container {
display: flex;
+ grid-area: content;
+ margin-top: 0;
}
.source_line_column {
padding-right: 0.5em;
text-align: right;
- background: #eee8d5;
+ color: var(--source-line-column);
+ background: var(--source-line-column-bg);
}
.source_line {
@@ -1201,9 +1388,9 @@ td.def-doc *:first-child {
.source_code {
flex-grow: 1;
- background: #fdf6e3;
+ background: var(--code-background);
padding: 0 0.3em;
- color: #657b83;
+ color: var(--code-color);
}
/* Source directories */
@@ -1236,7 +1423,7 @@ td.def-doc *:first-child {
.hljs-comment,
.hljs-meta {
- color: #969896;
+ color: var(--source-code-comment);
}
.hljs-string,
@@ -1244,35 +1431,35 @@ td.def-doc *:first-child {
.hljs-template-variable,
.hljs-strong,
.hljs-emphasis,
-.hljs-quote {
- color: #df5000;
+.hljs-quote,
+.hljs-literal {
+ color: var(--source-code-literal);
}
.hljs-keyword,
.hljs-selector-tag {
- color: #a71d5d;
+ color: var(--source-code-keyword);
}
.hljs-type,
.hljs-class .hljs-title {
- color: #458;
+ color: var(--source-code-uident);
font-weight: 500;
}
-.hljs-literal,
.hljs-symbol,
.hljs-bullet,
.hljs-attribute {
- color: #0086b3;
+ color: var(--hljs-literal);
}
.hljs-section,
.hljs-name {
- color: #63a35c;
+ color: var(--hljs-name);
}
.hljs-tag {
- color: #333333;
+ color: var(--hljs-tag);
}
.hljs-attr,
@@ -1280,100 +1467,129 @@ td.def-doc *:first-child {
.hljs-selector-class,
.hljs-selector-attr,
.hljs-selector-pseudo {
- color: #795da3;
+ color: var(--hljs-attr);
}
.hljs-addition {
- color: #55a532;
- background-color: #eaffea;
+ color: var(--hljs-addition);
+ background-color: var(--hljs-addition-bg);
}
.hljs-deletion {
- color: #bd2c00;
- background-color: #ffecec;
+ color: var(--hljs-deletion);
+ background-color: var(--hljs-deletion-bg);
}
.hljs-link {
text-decoration: underline;
}
-.VAL,
-.TYPE,
-.LET,
+/* Keywords */
+.AND, .ANDOP, .AS, .ASSERT,
+.BAR, .BEGIN,
+.CLASS, .CONSTRAINT,
+.DO, .DONE, .DOWNTO,
+.ELSE, .END, .EXCEPTION, .EXTERNAL,
+.FOR, .FUN, .FUNCTION, .FUNCTOR,
+.IF, .IN, .INCLUDE, .INHERIT, .INITIALIZER,
+.LAZY, .LESSMINUS, .LET, .LETOP,
+.MATCH, .METHOD, .MINUSGREATER, .MODULE, .MUTABLE,
+.NEW, .NONREC,
+.OBJECT, .OF, .OPEN,
+.PERCENT, .PRIVATE,
.REC,
-.IN,
-.OPEN,
-.NONREC,
-.MODULE,
-.METHOD,
-.LETOP,
-.INHERIT,
-.INCLUDE,
-.FUNCTOR,
-.EXTERNAL,
-.CONSTRAINT,
-.ASSERT,
-.AND,
-.END,
-.CLASS,
-.STRUCT,
-.SIG {
- color: #859900;
- ;
-}
-
-.WITH,
-.WHILE,
-.WHEN,
-.VIRTUAL,
-.TRY,
-.TO,
-.THEN,
-.PRIVATE,
-.OF,
-.NEW,
-.MUTABLE,
-.MATCH,
-.LAZY,
-.IF,
-.FUNCTION,
-.FUN,
-.FOR,
-.EXCEPTION,
-.ELSE,
-.TO,
-.DOWNTO,
-.DO,
-.DONE,
-.BEGIN,
-.AS {
- color: #cb4b16;
-}
-
-.TRUE,
-.FALSE {
- color: #b58900;
-}
-
-.failwith,
-.INT,
-.SEMISEMI,
-.LIDENT {
- color: #2aa198;
-}
-
-.STRING,
-.CHAR,
-.UIDENT {
- color: #b58900;
+.SEMISEMI, .SIG, .STRUCT,
+.THEN, .TO, .TRY, .TYPE,
+.VAL, .VIRTUAL,
+.WHEN, .WITH, .WHILE
+{
+ color: var(--source-code-keyword);;
+}
+
+/* Separators */
+.COMMA, .COLON, .COLONGREATER, .SEMI {
+ color: var(--source-code-separator);
+}
+
+/* Parens
+ `begin` and `end ` are excluded because `end` is used in other, more
+ keyword-y contexts*/
+.BARRBRACKET,
+.LBRACE,
+.LBRACELESS,
+.LBRACKET,
+.LBRACKETAT,
+.LBRACKETATAT,
+.LBRACKETATATAT,
+.LBRACKETBAR,
+.LBRACKETGREATER,
+.LBRACKETLESS,
+.LBRACKETPERCENT,
+.LBRACKETPERCENTPERCENT,
+.LPAREN,
+.RBRACE,
+.RBRACKET,
+.RPAREN
+{
+ color: var(--source-code-parens);
+}
+
+/* Prefix operators */
+.ASSERT, .BANG, .PREFIXOP,
+/* Infix operators.
+ A choice had to be made for equal `=` which is both a keyword and an operator.
+ It looked better having it as an operator, because when it is a keyword,
+ there are already loads of keyword around.
+ It would look even nicer if there was a way to distinguish between these
+ two cases.*/
+.INFIXOP0, .INFIXOP1, .INFIXOP2, .INFIXOP3, .INFIXOP4,
+.BARBAR, .PLUS, .STAR, .AMPERAMPER, .AMPERAND, .COLONEQUAL, .GREATER, .LESS,
+.MINUS, .MINUSDOT, .MINUSGREATER, .OR, .PLUSDOT, .PLUSEQ, .EQUAL
+{
+ color: var(--source-code-operator);
+}
+
+/* Upper case ident
+ `true` and `false` are considered uident here, because you can bind them in a
+ constructor defintion :
+ ```ocaml
+ type my_bool =
+ | true of string
+ | false
+ | Other of int
+ ```
+*/
+.UIDENT, .COLONCOLON, .TRUE, .FALSE {
+ color: var(--source-code-uident);
+
+}
+
+/* Lower case idents.
+ Quotes are here because of `type 'a t = 'a list`,
+ and question mark and tildes because of
+ ```ocaml
+ let f ~a ?b () = Option.map a b
+ ```
+*/
+.LIDENT, .QUESTION, .QUOTE, .TILDE {
+ color: var(--source-code-lident);
+}
+
+/* Litterals */
+ .STRING, .CHAR, .INT, .FLOAT, .QUOTED_STRING_EXPR, .QUOTED_STRING_ITEM {
+ color: var(--source-code-literal);
+}
+
+.UNDERSCORE {
+ color: var(--source-code-underscore);
}
.DOCSTRING {
- color: #268bd2;
+ color: var(--source-code-docstring);
}
.COMMENT {
- color: #93a1a1;
+ color: var(--source-code-comment);
}
/*---------------------------------------------------------------------------
@@ -1390,4 +1606,4 @@ td.def-doc *:first-child {
WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
- ---------------------------------------------------------------------------*/
\ No newline at end of file
+ ---------------------------------------------------------------------------*/
diff --git a/odoc.support/odoc_search.js b/odoc.support/odoc_search.js
index 0dc659d..79b86bd 100644
--- a/odoc.support/odoc_search.js
+++ b/odoc.support/odoc_search.js
@@ -64,3 +64,87 @@ document.querySelector(".search-bar").addEventListener("input", (ev) => {
wait();
worker.postMessage(ev.target.value);
});
+
+
+/** Navigation */
+
+let search_result_elt = document.querySelector(".search-result")
+
+function search_results() {
+ return search_result_elt.children;
+}
+
+function enter_search() {
+ document.querySelector(".search-bar").focus();
+}
+
+function escape_search() {
+ document.activeElement.blur()
+}
+
+function focus_previous_result() {
+ let results = Array.from(search_results());
+ let current_focus = results.findIndex((elt) => (document.activeElement === elt));
+ if (current_focus === -1)
+ return;
+ else if (current_focus === 0)
+ enter_search();
+ else
+ results[current_focus - 1].focus();
+}
+
+function focus_next_result() {
+ let results = Array.from(search_results());
+ if (results.length === 0) return;
+ let current_focus = results.findIndex((elt) => (document.activeElement === elt));
+ if (current_focus === -1)
+ results[0].focus();
+ else if (current_focus + 1 === results.length)
+ return;
+ else
+ results[current_focus + 1].focus();
+}
+
+
+function is_searching() {
+ return (document.querySelectorAll(".odoc-search:focus-within").length > 0);
+}
+
+function is_typing() {
+ return (document.activeElement === document.querySelector(".search-bar"));
+}
+
+function handle_key_down(event) {
+ if (is_searching()) {
+ if (event.key === "ArrowUp") {
+ event.preventDefault();
+ focus_previous_result();
+ }
+ if (event.key === "ArrowDown") {
+ event.preventDefault();
+ focus_next_result();
+ }
+ if (event.key === "Escape") {
+ event.preventDefault();
+ escape_search();
+ }
+ }
+ if (!(is_typing())) {
+ let ascii = event.key.charCodeAt(0);
+ if (event.key === "/") {
+ event.preventDefault();
+ enter_search();
+ }
+ else if ( is_searching()
+ && event.key.length === 1
+ && ( (ascii >= 65 && ascii <= 90) // lowercase letter
+ || (ascii >= 97 && ascii <= 122) // uppercase letter
+ || (ascii >= 48 && ascii <= 57) // numbers
+ || (ascii >= 32 && ascii <= 46) // ` ` to `.`
+ || (ascii >= 58 && ascii <= 64)) // `:` to `@`
+ )
+ // We do not prevent default because we want the char to be added to the input
+ enter_search ();
+ }
+}
+document.addEventListener("keydown", handle_key_down);