# Remove initial and terminal lines from Meta files.
# They are used to force us into "comment" mode by default.
s:^.*\?\\>RM.*$:{\\C{}}:
s:^.*RM\\<\?.*$:{\\CE{}}:

# MetaOCaml operators
s:\.\\<:\\Mbegincode{}:g
s:\\>\.:\\Mendcode:g
s:\.\\~:\\Msplice:g

# Server page operators
s:\\<?\(\(\\CE{}\|\\S{}\)*\)\(\(\\~{}\|!\|\\5\|=\)*\):\\Mquote{\3}\1:g
s:\?\\>:\\Munquote:g

# Miscellaneous syntactic niceties
s:\\-\\!\\>:\\ensuremath\\rightarrow:g
s:\\<=:\\codeleq:g
s:\\-:\\codeminus{}:g
s:\\{:\\codelb{}:g
s:\\}:\\coderb{}:g
s:\\<:\\textlt{}:g
s:\\>:\\textgt{}:g
#s:{`}\([A-Za-z0-9_]+\){'}:{\VRfont \1}:g
s:{`}\([a-z\\_]*\){'}:{\\VRfont \1}:g

# Increase spacing
#s:\\Head{}:\\Head{}\\baselineskip=11pt:

# TeX comments
s:^\\L{\\LB{\\Mquote{}\\CE{}\\C{}(\*_\(.*\)}}$:\\lgcommentstart{\\catcode`\\_=\\active\\def_{ } \1:
s:^\\L{\\LB{}\\Tab{[0-9]*}{\*_\(.*\)}}$: \1:
s:^\\L{\\LB{}\\Tab{[0-9]*}{\*)\\CE{}\\C{}\\Munquote}}:}\\lgcommentend:
#s:\([^_]*\)_:%_%\1 :g