The Specware command to process units is :sw. The user supplies this command in the XEmacs buffer of the Lisp shell, followed by an argument. The argument is a unit identifier.
The command to process a unit is:
:sw <unit-identifier> |
The unit identifier can be SWPATH-based or relative. If it is SWPATH-based, Specware attempts to resolve it as explained in the Section called SWPATH-Based Unit Identifier. If it is relative, Specware attempts to resolve it as explained in the Section called Relative Unit Identifiers, as if the unit identifier occurred in a single-unit file of the current Lisp directory. Either way, if resolution fails an error is signaled by Specware.
If instead resolution succeeds, Specware parses and evaluates the unit term that results from resolution. Parsing and evaluation carry out the computations to construct the unit; they are Specware's "core" functionality. Parsing and evaluation implement the semantics of the Metaslang language.
If the unit term references other units, Specware recursively resolves the unit identifiers and parses and evaluates their unit terms.
The command to process a multiple-unit file is:
:sw <unit-identifier> |
The unit identifier must not contain "#". Specware attempts to resolve the unit identifier. If it is a relative unit identifier, it is resolved as if it occurred inside a single-unit file in the Lisp current directory. However, the file obtained at the third step must be a multi-unit file, and not a single-unit file. If it is indeed a multi-unit file, Specware parses and evaluates all the unit definitions inside the file.