diff options
| author | Georg Brandl <georg@python.org> | 2021-01-18 21:24:00 +0100 |
|---|---|---|
| committer | Georg Brandl <georg@python.org> | 2021-01-18 22:08:36 +0100 |
| commit | 2a3d3a7d5b9c60dedf6638d876161d9563faebcf (patch) | |
| tree | 809c0b4a686db98f5954afa1944404cd9652c6b2 /tests/lexers/lagda | |
| parent | f0445be718da83541ea3401aad882f3937147263 (diff) | |
| download | pygments-git-examplefiles.tar.gz | |
Move test_examplefiles to new tests/lexers scheme.examplefiles
Diffstat (limited to 'tests/lexers/lagda')
| -rw-r--r-- | tests/lexers/lagda/example.txt | 126 |
1 files changed, 126 insertions, 0 deletions
diff --git a/tests/lexers/lagda/example.txt b/tests/lexers/lagda/example.txt new file mode 100644 index 00000000..905cdfa0 --- /dev/null +++ b/tests/lexers/lagda/example.txt @@ -0,0 +1,126 @@ +---input--- +\documentclass{article} +% this is a LaTeX comment +\usepackage{agda} + +\begin{document} + +Here's how you can define \emph{RGB} colors in Agda: + +\begin{code} +module example where + +open import Data.Fin +open import Data.Nat + +data Color : Set where + RGB : Fin 256 → Fin 256 → Fin 256 → Color +\end{code} + +\end{document} + +---tokens--- +'\\documentclass' Keyword +'{' Name.Builtin +'article' Text +'}' Name.Builtin +'\n' Text + +'% this is a LaTeX comment\n' Comment + +'\\usepackage' Keyword +'{' Name.Builtin +'agda' Text +'}' Name.Builtin +'\n\n' Text + +'\\begin' Keyword +'{' Name.Builtin +'document' Text +'}' Name.Builtin +"\n\nHere's how you can define " Text +'\\emph' Keyword +'{' Name.Builtin +'RGB' Text +'}' Name.Builtin +' colors in Agda:\n\n' Text + +'\\begin' Keyword +'{' Name.Builtin +'code' Text +'}' Name.Builtin +'\n' Text + +'module' Keyword.Reserved +' ' Text +'example' Name +' ' Text +'where' Keyword.Reserved +'\n' Text + +'\n' Text + +'open' Keyword.Reserved +' ' Text +'import' Keyword.Reserved +' ' Text +'Data.Fin' Name +'\n' Text + +'open' Keyword.Reserved +' ' Text +'import' Keyword.Reserved +' ' Text +'Data.Nat' Name +'\n' Text + +'\n' Text + +'data' Keyword.Reserved +' ' Text +'Color' Text +' ' Text +':' Operator.Word +' ' Text +'Set' Keyword.Type +' ' Text +'where' Keyword.Reserved +'\n' Text + +' ' Text +'RGB' Name.Function +' ' Text +':' Operator.Word +' ' Text +'Fin' Text +' ' Text +'256' Literal.Number.Integer +' ' Text +'→' Operator.Word +' ' Text +'Fin' Text +' ' Text +'256' Literal.Number.Integer +' ' Text +'→' Operator.Word +' ' Text +'Fin' Text +' ' Text +'256' Literal.Number.Integer +' ' Text +'→' Operator.Word +' ' Text +'Color' Text +'\n' Text + +'\\end' Keyword +'{' Name.Builtin +'code' Text +'}' Name.Builtin +'\n\n' Text + +'\\end' Keyword +'{' Name.Builtin +'document' Text +'}' Name.Builtin +'\n' Text |