The Twelf Project:Syntax highlighting

From The Twelf Project

Syntax highlighting on this website is enabled by GeSHiCodeTag running on the General Syntax Highlighter. A prototype syntax highlighting extension has been written for the Twelf Wiki that can be enabled by using the <code twelf></code>, but this is depreciated; the syntax highlighter called when using the <twelf> tag of TwelfTag is written in Haskell.

As a result, the GeSHi Twelf extensions has bugs that will not be fixed; however, the GeSHi code extension remains for backward-compatability and for highlighting code in languages besides Twelf.

[edit] Using Syntax Highlighting

A full list of supported languages is below - GeSHi comes with support for the PHP, C, OCaml, and others. The best way to enter code is to use the <code language> tag, where "language" is the language you want to use - GeSHi will print out the list of languages it supports if the one you pick is not one it recognizes. Furthermore, a tag without a language option, i.e. <code>, is a useful way to insert preformatted text into the pages. So this code:

<code twelf>plus_s : plus (s N1) N2 (s N3)
	  <- plus N1 N2 N3.</code>

would appear like this:

plus_s : plus (s N1) N2 (s N3) <- plus N1 N2 N3.

However, to restate the point made above, you shouldn't ever do this for Twelf code, you should use TwelfTag.

[edit] Line numbers

There's also an advaced code tag that adds in line numbers (which do not get taken along for the ride if you copy and paste the text!) It would be nice to make this the common practice for large code snippiets, but because it makes the text so darn small in some browsers that it's not a good idea unless someone can figure out how to make it consistantly bigger. This code:

<code twelf n>nat : type.
z: nat. s: nat -> nat.

plus : nat -> nat -> nat -> type.
%mode plus +N1 +N2 -N3.
plus_z : plus z N N.
plus_s : plus (s N1) N2 (s N3)
	  <- plus N1 N2 N3.
%worlds () (plus _ _ _). %total N (plus N _ _).</code>

will get displayed like this:

nat : type. z: nat. s: nat -> nat.

plus : nat -> nat -> nat -> type. %mode plus +N1 +N2 -N3. plus_z : plus z N N. plus_s : plus (s N1) N2 (s N3) <- plus N1 N2 N3. %worlds () (plus _ _ _). %total N (plus N _ _).

[edit] Supported Languages

You can use the same structure for a wide variety of other languages, which are all listed below.

echo "Hello World"; </php>