@example
value := 00? 00? 00? 00? raw-value
-raw-value := 01 opt-value int32[format] double
- | 02 opt-value int32[format] double string[varname] string[vallab]
- (01 | 02 | 03)
- | 03 string[local] opt-value string[id] string[c] (00 | 01)
+raw-value := 01 opt-value int32[format] double[x]
+ | 02 opt-value int32[format] double[x]
+ string[varname] string[vallab] (01 | 02 | 03)
+ | 03 string[local] opt-value string[id] string[c] (00 | 01)[type]
| 04 opt-value int32[format] string[vallab] string[varname]
(01 | 02 | 03) string[vallab]
| 05 opt-value string[varname] string[varlabel] (01 | 02 | 03)
nested-string := 00 00 count(counted-string (58 | 31 style) 58)
counted-string := count((i0 (58 | 31 string))?)
@end example
+
+A @code{value} boils down to a number or a string. There are several
+possibilities, which one can distinguish by the first nonzero byte in
+the encoding:
+
+@table @code
+@item 01
+The numeric value @code{x}, presented to the user formatted according
+to @code{format}, which is in the format described for system files.
+@xref{System File Output Formats}, for details. Most commonly
+@code{format} has width 40 (the maximum).
+
+An @code{x} with the maximum negative double @code{-DBL_MAX}
+represents the system-missing value SYSMIS. (HIGHEST and LOWEST have
+not been observed.) @xref{System File Format}, for more about these
+special values.
+
+@item 02
+Similar to @code{01}, with the additional information that @code{x} is
+a value of variable @code{varname} and has value label @code{vallab}.
+Both @code{varname} and @code{vallab} can be the empty string, the
+latter very commonly.
+
+The meaning of the final byte is unknown. Possibly it is connected to
+whether the value or the label should be displayed.
+
+@item 03
+A text string that originates from the software program (rather than
+from user data). The string is provided in two forms: @code{c} is in
+English and @code{local} is localized to the user's language
+environment. In an English-language locale, the two strings are often
+the same, and in cases where they differ @code{c} is often abbreviated
+or obscure and @code{local} is more appropriate for a user interface,
+e.g.@: @code{c} of ``Not a PxP table for MCN...'' versus @code{local}
+of ``Computed only for a PxP table, where P must be greater than 1.''
+
+@code{id} is a brief identifying string whose form seems to resemble a
+programming language identifier, e.g.@: @code{cumulative_percent} or
+@code{factor_14}. It is not unique.
+
+@code{type} is 00 for text taken from user input, such as syntax
+fragment, expressions, file names, data set names, and 01 for fixed
+text strings such as names of procedures or statistics.
+
+@item 04