TwelfTag

The TwelfTag system is a way of adding STELF code directly into the STELF Project Wiki. This page gives an introduction to TwelfTag for readers. The page has information about TwelfTag for editors, and the STELF Live system provides a more interactive way of using STELF with on this website.

Syntax highlighting

The most basic function of TwelfTag is to highlight STELF code much the same way that Emacs does. Names are red, and metavariables (free variables) are in blue.

%sort elem %.
%sort list %.
%term nil list %.
%term cons %pi elem %-> list %-> list %.
%sort list-reverse {_ list} {_ list} {_ list} %.
%term lr/nil list-reverse nil L L %.
%term lr/cons %pi (list-reverse (cons E L1) L2 L3) %<- (list-reverse L1 (cons E L2) L3) %.

Showing STELF’s response

When STELF checks a piece of code, it produces some output that represents STELF’s reconstruction of that code and a message (%% OK %% or %% ABORT %%) that signals whether it was successful. Sometimes it is helpful to show STELF’s response in an article, and TwelfTag can do this too, showing STELF’s response in green.

%solve test : {e1} {e2} {e3} {e4} list-reverse (cons e1 (cons e3 (cons e2 (cons e4 nil)))) nil _ %.
%% OK %

Linking to STELF code and STELF output

TwelfTag has the ability to link, inside a page, to the code that has been shown highlighted on that page, and also to link to the response STELF gives when checking that code. *<twelflink>This link</twelflink> shows you the twelf code (the code that is shown with syntax ) for this page. *<twelflink check=true>This link</twelflink> shows you STELF’s response from reading the code on this page.

”Literate STELF”

For some pages, including this one, the page itself is written in valid STELF that is then automatically transformed into an article. Pages written in this way look exactly like other pages, but they have a note at the top of the article that reports on STELF’s status after reading the file - %% OK %% means everything checked out, and %% ABORT %% means that there was a problem - and links to both the code and STELF’s response.