Whitespace
One or more of the whitespace tokens
Documentation out of dateLearn more
Lexical Syntax of STELF
The STELF lexical syntax varies largely from the original Twelf. In particular, STELF’s lexical syntax is designed to use as few classes as possible, and for those classes to be as unobtrusive as possible.
Requirements
Section titled “Requirements”All input to STELF is assumed to be valid UTF-8, and to follow the conventions. It is not a requirement that the input be normalized, or orthographically correct. Characters are not normalized.
Conventions
Section titled “Conventions”Whitespace is defined as the unicode charecters with the property White_Space=yes
The “newline” charecters are any of those whose charecters 0x000A, 0x000B, 0x000C, 0x000D, 0x0085, 0x2028, and 0x2029.
The following charecters have the following unicode values
| Charecter | Unicode (Hex) |
|---|---|
% | 25 |
_ | 5F |
( | 28 |
) | 29 |
{ | 7B |
} | 7D |
[ | 5B |
] | 5D |
Lexical Classes
Section titled “Lexical Classes”Terms fall into one of a couple lexical classes
Tokens
Special charecters which are not whitespace.
Some of the time do not behave differently.
These are (, ), {, }, [, ]
Commands
This is the most important part of the syntax.
In most cases, commands are any token preeced by whitespace or a special token starting with %, then followed by a list of any other charecters, and followed by whitespace or, if not containing special charecters, a special charecter.
Special Syntax
Strings, comments, escape charecters,
Names
Any sequence of non-whitespace, non-special charecters.
Names are equivalent up to equality, except for names which start with _, which are treated specially1
By equivalent up to equality, we mean that +αֶ and foo can be swapped for each other, and so long as they are swapped whenever they are referenced, are equivalent
Special Lexical Syntax
Section titled “Special Lexical Syntax”There are three things that are lexed completely differently from everything else. In addition, in the order they are presented, they take precednence over every other rule in the grammar
Escaping
There is a special command, %%.
Unlike every other construct, %% takes one and only one arguement, which is exactly one charecter long.
In addition, this takes precedence over every other command.
The only effect of this command is to remove any special meaning that a symbol has, wherever it occurs.
This is the only command that can occur anywhere.
If the charecter following this is not special, this just becomes a no-op.
2
Strings
Strings begin with the command %[.
While many of the commands have mutiple forms, strings are the only one with infinite, as you can also use %[[, %[[[, %[[[[, and so on.
Strings are terminated with %], %]], and %]]].
The number of ]s must match the number of [ used to begin a string.
Strings may not nest.
Strings are valid anywhere in the grammar, except inside other strings and when preceeded by an unescaped % (in which case it becomes %% then [[[[) which isn’t a command
Currently, strings aren’t used anywhere, and only serve the purpose of making outer markup nicer to work with
Inline comments
Inline comments stay the same as in Twelf.
A comment is begun by the empty command (% followed by whitespace), and ends with a newline, as defined above.