When a unit definition is processed, a unit value is produced. For example, a spec is essentially a set of sorts, ops, and axioms. A spec can be constructed by means of various operations in the Metaslang language, but the final result is always a spec, i.e., a set of sorts, ops, and axioms.
The :show command is used to display the value of a unit. Like :sw, it is also supplied in the XEmacs buffer of the Lisp shell and it is followed by a one-line argument. The argument is a unit identifier.
The command to display a unit is:
:show <unit-identifier> |
This command first processes the unit, exactly as if it were :sw <unit-identifier>. In addition, if processing does not yield errors, the value of the unit is displayed on screen. Of course, if the unit has been already processed via a :sw command and its unit term has not been changed after that, the :show command will access the results saved in Specware's internal cache.
The :show command serves to inspect the value of units constructed via the Metaslang operations. This is especially useful for beginning users as an aid to clarify the semantics of such operations.
As already mentioned, Specware maintains an internal cache that associates processing results with unit identifiers.
A list of the units currently present in the cache is displayed on screen via the following command:
:list |
The cache is cleared (i.e., re-initialized) via the following command:
:sw-init |
Normally, there is no need to use these commands.
The value of the SWPATH environment variable is displayed on screen via the following command:
:swpath |
The value of the SWPATH environment variable is changed via the following command:
:swpath <string> |
The <string> must be a semicolon-separated list of absolute directory paths of the underlying operating system. For example, in order to set SWPATH to c:\users\me it is necessary to write :swpath c:\users\me.
Changes to SWPATH only apply to the currently running Specware session. If Specware is quit and then restarted, SWPATH loses the value assigned to it during the previous session, reverting to its default value.
Normally, Lisp code is generated by constructing a Lisp program unit via the Metaslang generate operation and by processing such unit via the :sw command.
Specware provides an additional command to accomplish the same result without actually creating an explicit Lisp program unit. The command is:
:swl <unit-identifier> <string> |
The unit identifier must resolve to a spec, which is processed by Specware. If the spec is successfully processed, Specware generates Lisp code from it (according to the semantics of generate) and deposits the resulting code into the file whose path is given by the string.
The second argument to :swl, i.e. the string, is optional. If it is not given, a file name is inferred as explained in the Section called Generating Lisp Code for generate.
:swll <unit-identifier> |
This is like :swl except it generates code only for the local definitions of the spec given by the unit identifier and not any of the imports. It is intended for incremental development, so it compiles and loads the lisp definitions. Note that if you have not generated code for the imported specs and loaded them, trying to run the code generated by this command will give undefined function errors. Also, if the spec is unqualified but it is imported into a spec that is qualified, the package used will be :SW-USER instead of the package of the qualifier. To avoid this problem qualification can be added to the spec.
When developing a specware application you generate code for your application, compile, load and test it. Then if you make a modification to a single spec you can use the :swll to just load the generated code for the modification. This command is also useful when you just want to see the generated code for a particular spec.
:cl <lisp-file-name> |
Compiles and loads a lisp file.
:sw-help <command-name> |
Prints brief documentation for the specware command command-name. If command-name is omitted it prints documentation for all the specware commands.
:dir <directory> |
Gives directory listing of directory. If directory is omitted it uses the current directory.
:ls <directory> |
Gives directory listing of directory. If directory is omitted it uses the current directory.