Struct TypesettingData

pub struct TypesettingData {

    pub diagnostics: Vec<(StatementAddress, Diagnostic)>,
    pub latex_defs: HashMap<Token, (Span, GlobalSpan, Token), BuildHasherDefault<FnvHasher>>,
    pub html_defs: HashMap<Token, (Span, GlobalSpan, Token), BuildHasherDefault<FnvHasher>>,
    pub alt_html_defs: HashMap<Token, (Span, GlobalSpan, Token), BuildHasherDefault<FnvHasher>>,
    pub html_var_color: Vec<(GlobalSpan, Token)>,
    pub html_title: Option<(GlobalSpan, Token)>,
    pub html_home: Option<(GlobalSpan, Token)>,
    pub html_dir: Option<(GlobalSpan, Token)>,
    pub alt_html_dir: Option<(GlobalSpan, Token)>,
    pub html_bibliography: Option<(GlobalSpan, Token)>,
    pub html_css: Option<(GlobalSpan, Token)>,
    pub html_font: Option<(GlobalSpan, Token)>,
    pub ext_html_label: Option<(GlobalSpan, Token)>,
    pub ext_html_title: Option<(GlobalSpan, Token)>,
    pub ext_html_home: Option<(GlobalSpan, Token)>,
    pub ext_html_bibliography: Option<(GlobalSpan, Token)>,
    pub html_ext_url: Option<(GlobalSpan, Token)>,
}

The parsed $t comment data.

Fields

diagnostics: Vec<(StatementAddress, Diagnostic)>

Any errors detected while parsing this segment.

latex_defs: HashMap<Token, (Span, GlobalSpan, Token), BuildHasherDefault<FnvHasher>>

LaTeX definitions are used to replace a token with a piece of latex syntax. Each entry has the form (token, replacement).

latexdef "ph" as "\varphi";

html_defs: HashMap<Token, (Span, GlobalSpan, Token), BuildHasherDefault<FnvHasher>>

HTML definitions are used to replace a token with a piece of HTML syntax. This version will generally be used for the GIF rendering version of the web pages. Each entry has the form (token, replacement).

htmldef "ph" as "<IMG SRC='_varphi.gif' WIDTH=11 HEIGHT=19 ALT=' ph' TITLE='ph'>";

alt_html_defs: HashMap<Token, (Span, GlobalSpan, Token), BuildHasherDefault<FnvHasher>>

HTML definitions are used to replace a token with a piece of HTML syntax. This version will generally be used for the unicode rendering version of the web pages. Each entry has the form (token, replacement).

althtmldef "ph" as "<SPAN CLASS=wff STYLE='color:blue'>&#x1D711;</SPAN>";

html_var_color: Vec<(GlobalSpan, Token)>

A piece of HTML to give the variable color key. All htmlvarcolor directives are given separately here, but they are logically concatenated with spaces for rendering.

htmlvarcolor '<SPAN CLASS=wff STYLE="color:blue;font-style:normal">wff</SPAN> '
  + '<SPAN CLASS=setvar STYLE="color:red;font-style:normal">setvar</SPAN> '
  + '<SPAN CLASS=class STYLE="color:#C3C;font-style:normal">class</SPAN>';

html_title: Option<(GlobalSpan, Token)>

The title of the generated HTML page.

htmltitle "Metamath Proof Explorer";

html_home: Option<(GlobalSpan, Token)>

The link to the home page in the generated HTML page.

htmlhome '<A HREF="mmset.html"><FONT SIZE=-2 FACE=sans-serif>' +
    '<IMG SRC="mm.gif" BORDER=0 ALT='  +
    '"Home" HEIGHT=32 WIDTH=32 ALIGN=MIDDLE STYLE="margin-bottom:0px">' +
    'Home</FONT></A>';

html_dir: Option<(GlobalSpan, Token)>

The relative path from the unicode version to the GIF version. Used for cross references. (This is a set.mm specific hack.)

htmldir "../mpegif/";

alt_html_dir: Option<(GlobalSpan, Token)>

The relative path from the GIF version to the unicode version. Used for cross references. (This is a set.mm specific hack.)

althtmldir "../mpeuni/";

html_bibliography: Option<(GlobalSpan, Token)>

Optional file where bibliographic references are kept.

htmlbibliography "mmset.html";

html_css: Option<(GlobalSpan, Token)>

Custom CSS to be placed in the header of generated files. Note that any \n escapes are not yet replaced by newlines in this html_css variable; library consumers are responsible for performing this replacement.

htmlcss '<STYLE TYPE="text/css">\n' +
  '</STYLE>\n' +
  '<LINK href="mmset.css" title="mmset"\n' +
  '    rel="stylesheet" type="text/css">\n';

html_font: Option<(GlobalSpan, Token)>

Tag(s) for the main SPAN surrounding all Unicode math.

htmlfont 'CLASS=math';

ext_html_label: Option<(GlobalSpan, Token)>

A label, such that everything after this label uses the ext_* variables instead of the regular ones. (This is a set.mm specific hack.)

exthtmllabel "chil";

ext_html_title: Option<(GlobalSpan, Token)>

The title of the generated HTML page, for the Hilbert Space extension. (This is a set.mm specific hack.)

exthtmltitle "Hilbert Space Explorer";

ext_html_home: Option<(GlobalSpan, Token)>

The link to the home page in the generated HTML page, for the Hilbert Space extension. (This is a set.mm specific hack.)

exthtmlhome '<A HREF="mmhil.html"><FONT SIZE=-2 FACE=sans-serif>' +
   '<IMG SRC="atomic.gif" BORDER=0 ALT='  +
   '"Home" HEIGHT=32 WIDTH=32 ALIGN=MIDDLE STYLE="margin-bottom:0px">' +
   'Home</FONT></A>';

ext_html_bibliography: Option<(GlobalSpan, Token)>

Optional file where bibliographic references are kept, for the Hilbert Space extension. (This is a set.mm specific hack.)

exthtmlbibliography "mmhil.html";

html_ext_url: Option<(GlobalSpan, Token)>

Optional link(s) to other versions of the theorem page. A “” is replaced with the label of the current theorem. If you need a literal “” as part of the URL, use the alternate URL encoding “%2A”. (Note that * characters are not interpreted in this string; library consumers are responsible for implementing this spec.)

htmlexturl '<A HREF="http://metamath.tirix.org/*.html">'
    + 'Structured version</A>&nbsp;&nbsp; '
    + '<A HREF="https://expln.github.io/metamath/asrt/*.html">'
    + 'Visualization version</A>&nbsp;&nbsp; ';

Implementations

impl TypesettingData

pub fn get_alt_html_def(&self, symbol: TokenPtr<'_>) -> Option<&Token>

Get the unicode rendering for a given symbol

Trait Implementations

impl Clone for TypesettingData

fn clone(&self) -> TypesettingData

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for TypesettingData

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

Formats the value using the given formatter.

impl Default for TypesettingData

fn default() -> TypesettingData

Returns the “default value” for a type.