mdtablefix 0.6.1

`mdtablefix` unb0rks and reflows Markdown tables so that each column has a uniform width. When the `--wrap` option is used, it also wraps paragraphs and list items to 80 columns.
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46

//! Production consumer decisions derived from the verified classifier.

#[cfg(verus_keep_ghost)]
use vstd::prelude::*;

use super::{ClassifyCtxKernel, LineClass, classify_seq};

verified_kernel_function! {
/// Accepts Setext text only when the shared classifier sees paragraph text.
#[must_use]
pub(crate) fn is_setext_text_seq(chars: &[char], ctx: &ClassifyCtxKernel) -> bool;
ensures(result => result == (crate::spec_classify(chars@, ctx@) == LineClass::ParagraphText));
{
    matches!(classify_seq(chars, ctx).class, LineClass::ParagraphText)
}
}

verified_kernel_function! {
/// Accepts a Setext underline only under its preceding-paragraph context.
#[must_use]
pub(crate) fn is_setext_underline_seq(chars: &[char], ctx: &ClassifyCtxKernel) -> bool;
ensures(result => result == (crate::spec_classify(chars@, ctx@) == LineClass::SetextUnderline));
{
    matches!(classify_seq(chars, ctx).class, LineClass::SetextUnderline)
}
}

verified_kernel_function! {
/// Selects only structural thematic breaks for canonicalization.
#[must_use]
pub(crate) fn is_canonical_break_seq(chars: &[char], ctx: &ClassifyCtxKernel) -> bool;
ensures(result => result == (crate::spec_classify(chars@, ctx@) == LineClass::ThematicBreak));
{
    matches!(classify_seq(chars, ctx).class, LineClass::ThematicBreak)
}
}

verified_kernel_function! {
/// Confirms that emitted Setext replacement is structurally an ATX heading.
#[must_use]
pub(crate) fn is_atx_heading_seq(chars: &[char], ctx: &ClassifyCtxKernel) -> bool;
ensures(result => result == (crate::spec_classify(chars@, ctx@) == LineClass::AtxHeading));
{
    matches!(classify_seq(chars, ctx).class, LineClass::AtxHeading)
}
}