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.

List of supported languages for Geshi 1.0.7.13:
nsis
reg
xml
bash
asp
css
fortran
java
ada
smalltalk
cfdg
python
dos
tsql
lua
asm
sas
java5
html4strict
robots
blitzbasic
pascal
c_mac
applescript
cadlisp
winbatch
smarty
apache
php
perl
c
mysql
vb
idl
inno
groovy
cpp
ocaml-brief
autoit
ruby
sql
eiffel
delphi
lisp
qbasic
cfm
visualfoxpro
oobas
objc
javascript
vhdl
oracle8
mpasm
tcl
diff
ocaml
csharp
scheme
php-brief
ini
freebasic
vbnet
twelf
text
sdlbasic
d
caddcl
matlab
actionscript
gml