Lurch web app user interface

Module

HeadlessLurch

Utilities needed by the command-line interface

This module is a set of auxiliary tools required by the command-line interface. See that module's documentation for how to use the CLI, or this module's documentation for what it provides.

The main purpose here is to launch two invisible background services that the CLI can leverage:

  1. a web server that serves the Lurch app from this repository, so that any browser running on the local machine can access it, and
  2. a headless Chromium browser that runs the Lurch app from that server.

This module provides many functions for interacting with the copy of the Lurch app in the headless Chromium browser, for putting content in, and getting responses back, including the document in various forms, and the results of validation run in the app.

Typically, the CLI will use the functions in this module in this order:

  • Create an invisible, running copy of the Lurch app with openApp().
  • Load a document into the app with openDocument().
  • Validate the document and return the validation results with validationResults().
  • Possibly repeat the above two steps or some subset of them many times.
  • Optionally get the document in PDF form with documentAsPDF().
  • Optionally close the app with closeApp().

Source

Methods

static

closeApp()

Close the headless Chromium that's running the Lurch app. Although this function is provided for completeness, as a twin to openApp(), the CLI does not actually use it, because it just closes the entire CLI when it's complete, which implicitly shuts down this resource.

Source

static

documentAsPDF() → {Promise.<Buffer>}

Get the appearance of the document in the app in the headless browser, represented as a PDF. The return value is the content that belongs in a PDF file, which can then be written to a .pdf file on disk.

Returns

  • Promise.<Buffer>

    a buffer containing the contents of a PDF file

Source

static

documentHTML() → {Promise.<string>}

Get the full contents of the current Lurch app, in the same long-form HTML that would be saved if the user invoked Save from the app's File menu.

Returns

  • Promise.<string>

    the contents of the document (in long-form HTML)

Source

static

isLongForm(html) → {Promise.<boolean>}

Long form HTML is the type of HTML saved by the Lurch app. We call it "long form" because each atom in the document (which has a very small appearance on screen) has a rather large appearance in the HTML content, because that content contains all the atom's internal properties, as well as all of the HTML necessary to represent its typeset form on screen (which can be complex).

There is also a more compact way to represent Lurch documents using HTML tags, as documented in the embed-listener.js module. This function takes a string of HTML as input and detects whether it is an HTML file that was saved from the Lurch app (long form) or not (assumed therefore to be short form).

Parameters

  • html string

    the HTML to test to see whether it is in long form

Returns

  • Promise.<boolean>

    whether the given HTML is in long form

Source

static

openApp()

Open the browser, launch a page, load the Lurch app into that page, and wait until the app is fully loaded. A few meessages will be printed to the console while that happens, so that users of the CLI will know what's going on during the noticeable delay it takes to launch the app.

Source

static

openDocument(filename)

Read a document from the filesystem, recursively obeying any "import" tags inside it (and throwing an error if any circular dependencies are detected), then load the resulting document into the Lurch app in one of three ways:

  • If the file is an HTML file, and it is detected to be in long form (the type saved by the Lurch app) using isLongForm(),then load it directly into the app with no changes.
  • If the file is an HTML file, but it is not detected to be in long form, then assume it contains simplified HTML, and provide it to the app as if the app were an embedded copy of the Lurch app, so that the HTML content will be processed by the embed-listener.js module. This will expand tags of the form <lurch>...</lurch>, <theorem>...</theorem>, and so on into their full internal representations.
  • If the file is a Markdown file, do the same as in the previous bullet point, because the embed-listener.js module supports Markdown as well.

Parameters

  • filename string

    the file to load from the filesystem

Source

static

validationResults() → {Promise.<Array.<Object>>}

Run validation on the document currently in the Lurch app, wait until that validation completes, then find every atom (which includes shells) in the document anbd extract its key information. The result (when the promise resolves) is an array of objects with the following fields.

  • type - the type of atom (e.g., "expression" or "theorem" etc.)
  • result - the validation result (e.g., "valid" or "invalid")
  • depth - the nesting depth of the atom, an integer greater than 0
  • lurch - the meaning of the atom, in Lurch notation, if it is the type of atom that has a meaning in Lurch notation (e.g., an expression written using the intermediate or advanced version of the editor)
  • latex - the LaTeX representation of the atom (which may mean that it is an expository math atom, and thus has no meaning, or it may mean that it is an expression created by the beginner version of the editor, and thus its content was expressed in LaTeX created by MathLive)
  • given - true if the atom is an assumption and was created by the beginner version of the editor
  • contentType - a string representing the type of expression, if it is an expression created by the intermediate version of the editor (which permits content types "Statement", "Assumption", and various forms of declaration)
  • symbol - the symbol being declared, if the atom is a declaration built using the intermediate form of the expression editor

Returns

  • Promise.<Array.<Object>>

Source