Struct SourcePosition 

pub struct SourcePosition { /* private fields */ }

The transparent carrier’s payload: a binder’s kind, or where a subterm came from. A position in a source text, in Lean’s convention: the LINE is 1-based and the COLUMN is 0-based and counted in Unicode scalar values. Held in its canonical spelling, the one Lean prints a diagnostic’s position in — file:line:column — so a position IS its text: two positions are equal exactly when they print the same, and reading one back needs no rendering.

Implementations

impl SourcePosition

pub fn new(file: impl Into<String>, line: u32, column: u32) -> SourcePosition

The position file:line:column.

pub fn parse(text: &str) -> Option<SourcePosition>

Read a position in its canonical spelling, file:line:column. The LAST two :-separated fields are the line and the column, so a file name may itself contain :; the file is not empty, the line is at least 1, and both numbers are written in canonical decimal (no sign, no leading zero) so that reading and printing are inverse.

pub fn file(&self) -> &str

The file (or other source unit) the subterm was written in.

pub fn line(&self) -> u32

The 1-based line.

pub fn column(&self) -> u32

The 0-based column, in Unicode scalar values.

pub fn as_str(&self) -> &str

The canonical spelling, file:line:column.

Trait Implementations

impl Clone for SourcePosition

fn clone(&self) -> SourcePosition

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for SourcePosition

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

Formats the value using the given formatter.

impl Display for SourcePosition

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

Formats the value using the given formatter.

impl PartialEq for SourcePosition

fn eq(&self, other: &SourcePosition) -> 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 Eq for SourcePosition

impl StructuralPartialEq for SourcePosition