Struct ContextRequest 

pub struct ContextRequest {
    pub file: LeanFile,
    pub line: u32,
    pub before: usize,
    pub after: usize,
}

Where to center a context bundle and how much surrounding source to include.

Fields

file: LeanFile

Target Lean source file.

line: u32

One-based line the bundle is centered on.

before: usize

Source lines to include before the target line.

after: usize

Source lines to include after the target line.

Implementations

impl ContextRequest

pub const fn new(file: LeanFile, line: u32) -> Self

Build a request with the default eight-line window on each side.

Trait Implementations

impl Clone for ContextRequest

fn clone(&self) -> ContextRequest

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for ContextRequest

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl Eq for ContextRequest

impl PartialEq for ContextRequest

fn eq(&self, other: &ContextRequest) -> bool

Tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Rhs) -> bool

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl StructuralPartialEq for ContextRequest