diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -10,6 +10,7 @@
 - Abc
 - Actionscript
 - Ada
+- Agda
 - Apache
 - Asn1
 - Asp
diff --git a/Text/Highlighting/Kate/Syntax.hs b/Text/Highlighting/Kate/Syntax.hs
--- a/Text/Highlighting/Kate/Syntax.hs
+++ b/Text/Highlighting/Kate/Syntax.hs
@@ -18,6 +18,7 @@
 import qualified Text.Highlighting.Kate.Syntax.Abc as Abc
 import qualified Text.Highlighting.Kate.Syntax.Actionscript as Actionscript
 import qualified Text.Highlighting.Kate.Syntax.Ada as Ada
+import qualified Text.Highlighting.Kate.Syntax.Agda as Agda
 import qualified Text.Highlighting.Kate.Syntax.Alert as Alert
 import qualified Text.Highlighting.Kate.Syntax.Alert_indent as Alert_indent
 import qualified Text.Highlighting.Kate.Syntax.Apache as Apache
@@ -132,11 +133,11 @@
 
 -- | List of supported languages.
 languages :: [String]
-languages = ["Abc","Actionscript","Ada","Alert","Alert_indent","Apache","Asn1","Asp","Awk","Bash","Bibtex","Boo","C","Changelog","Clojure","Cmake","Coffee","Coldfusion","Commonlisp","Cpp","Cs","Css","Curry","D","Diff","Djangotemplate","Dot","Doxygen","Doxygenlua","Dtd","Eiffel","Email","Erlang","Fasm","Fortran","Fsharp","Gcc","Glsl","Gnuassembler","Go","Haskell","Haxe","Html","Ini","Isocpp","Java","Javadoc","Javascript","Json","Jsp","Julia","Latex","Lex","Lilypond","LiterateCurry","LiterateHaskell","Lua","M4","Makefile","Mandoc","Markdown","Mathematica","Matlab","Maxima","Mediawiki","Metafont","Mips","Modelines","Modula2","Modula3","Monobasic","Nasm","Noweb","Objectivec","Objectivecpp","Ocaml","Octave","Opencl","Pascal","Perl","Php","Pike","Postscript","Prolog","Pure","Python","R","Relaxng","Relaxngcompact","Rest","Rhtml","Roff","Ruby","Rust","Scala","Scheme","Sci","Sed","Sgml","Sql","SqlMysql","SqlPostgresql","Tcl","Tcsh","Texinfo","Verilog","Vhdl","Xml","Xorg","Xslt","Xul","Yacc","Yaml","Zsh"]
+languages = ["Abc","Actionscript","Ada","Agda","Alert","Alert_indent","Apache","Asn1","Asp","Awk","Bash","Bibtex","Boo","C","Changelog","Clojure","Cmake","Coffee","Coldfusion","Commonlisp","Cpp","Cs","Css","Curry","D","Diff","Djangotemplate","Dot","Doxygen","Doxygenlua","Dtd","Eiffel","Email","Erlang","Fasm","Fortran","Fsharp","Gcc","Glsl","Gnuassembler","Go","Haskell","Haxe","Html","Ini","Isocpp","Java","Javadoc","Javascript","Json","Jsp","Julia","Latex","Lex","Lilypond","LiterateCurry","LiterateHaskell","Lua","M4","Makefile","Mandoc","Markdown","Mathematica","Matlab","Maxima","Mediawiki","Metafont","Mips","Modelines","Modula2","Modula3","Monobasic","Nasm","Noweb","Objectivec","Objectivecpp","Ocaml","Octave","Opencl","Pascal","Perl","Php","Pike","Postscript","Prolog","Pure","Python","R","Relaxng","Relaxngcompact","Rest","Rhtml","Roff","Ruby","Rust","Scala","Scheme","Sci","Sed","Sgml","Sql","SqlMysql","SqlPostgresql","Tcl","Tcsh","Texinfo","Verilog","Vhdl","Xml","Xorg","Xslt","Xul","Yacc","Yaml","Zsh"]
 
 -- | List of language extensions.
 languageExtensions :: [(String, String)]
-languageExtensions = [("Abc", Abc.syntaxExtensions), ("Actionscript", Actionscript.syntaxExtensions), ("Ada", Ada.syntaxExtensions), ("Alert", Alert.syntaxExtensions), ("Alert_indent", Alert_indent.syntaxExtensions), ("Apache", Apache.syntaxExtensions), ("Asn1", Asn1.syntaxExtensions), ("Asp", Asp.syntaxExtensions), ("Awk", Awk.syntaxExtensions), ("Bash", Bash.syntaxExtensions), ("Bibtex", Bibtex.syntaxExtensions), ("Boo", Boo.syntaxExtensions), ("C", C.syntaxExtensions), ("Changelog", Changelog.syntaxExtensions), ("Clojure", Clojure.syntaxExtensions), ("Cmake", Cmake.syntaxExtensions), ("Coffee", Coffee.syntaxExtensions), ("Coldfusion", Coldfusion.syntaxExtensions), ("Commonlisp", Commonlisp.syntaxExtensions), ("Cpp", Cpp.syntaxExtensions), ("Cs", Cs.syntaxExtensions), ("Css", Css.syntaxExtensions), ("Curry", Curry.syntaxExtensions), ("D", D.syntaxExtensions), ("Diff", Diff.syntaxExtensions), ("Djangotemplate", Djangotemplate.syntaxExtensions), ("Dot", Dot.syntaxExtensions), ("Doxygen", Doxygen.syntaxExtensions), ("Doxygenlua", Doxygenlua.syntaxExtensions), ("Dtd", Dtd.syntaxExtensions), ("Eiffel", Eiffel.syntaxExtensions), ("Email", Email.syntaxExtensions), ("Erlang", Erlang.syntaxExtensions), ("Fasm", Fasm.syntaxExtensions), ("Fortran", Fortran.syntaxExtensions), ("Fsharp", Fsharp.syntaxExtensions), ("Gcc", Gcc.syntaxExtensions), ("Glsl", Glsl.syntaxExtensions), ("Gnuassembler", Gnuassembler.syntaxExtensions), ("Go", Go.syntaxExtensions), ("Haskell", Haskell.syntaxExtensions), ("Haxe", Haxe.syntaxExtensions), ("Html", Html.syntaxExtensions), ("Ini", Ini.syntaxExtensions), ("Isocpp", Isocpp.syntaxExtensions), ("Java", Java.syntaxExtensions), ("Javadoc", Javadoc.syntaxExtensions), ("Javascript", Javascript.syntaxExtensions), ("Json", Json.syntaxExtensions), ("Jsp", Jsp.syntaxExtensions), ("Julia", Julia.syntaxExtensions), ("Latex", Latex.syntaxExtensions), ("Lex", Lex.syntaxExtensions), ("Lilypond", Lilypond.syntaxExtensions), ("LiterateCurry", LiterateCurry.syntaxExtensions), ("LiterateHaskell", LiterateHaskell.syntaxExtensions), ("Lua", Lua.syntaxExtensions), ("M4", M4.syntaxExtensions), ("Makefile", Makefile.syntaxExtensions), ("Mandoc", Mandoc.syntaxExtensions), ("Markdown", Markdown.syntaxExtensions), ("Mathematica", Mathematica.syntaxExtensions), ("Matlab", Matlab.syntaxExtensions), ("Maxima", Maxima.syntaxExtensions), ("Mediawiki", Mediawiki.syntaxExtensions), ("Metafont", Metafont.syntaxExtensions), ("Mips", Mips.syntaxExtensions), ("Modelines", Modelines.syntaxExtensions), ("Modula2", Modula2.syntaxExtensions), ("Modula3", Modula3.syntaxExtensions), ("Monobasic", Monobasic.syntaxExtensions), ("Nasm", Nasm.syntaxExtensions), ("Noweb", Noweb.syntaxExtensions), ("Objectivec", Objectivec.syntaxExtensions), ("Objectivecpp", Objectivecpp.syntaxExtensions), ("Ocaml", Ocaml.syntaxExtensions), ("Octave", Octave.syntaxExtensions), ("Opencl", Opencl.syntaxExtensions), ("Pascal", Pascal.syntaxExtensions), ("Perl", Perl.syntaxExtensions), ("Php", Php.syntaxExtensions), ("Pike", Pike.syntaxExtensions), ("Postscript", Postscript.syntaxExtensions), ("Prolog", Prolog.syntaxExtensions), ("Pure", Pure.syntaxExtensions), ("Python", Python.syntaxExtensions), ("R", R.syntaxExtensions), ("Relaxng", Relaxng.syntaxExtensions), ("Relaxngcompact", Relaxngcompact.syntaxExtensions), ("Rest", Rest.syntaxExtensions), ("Rhtml", Rhtml.syntaxExtensions), ("Roff", Roff.syntaxExtensions), ("Ruby", Ruby.syntaxExtensions), ("Rust", Rust.syntaxExtensions), ("Scala", Scala.syntaxExtensions), ("Scheme", Scheme.syntaxExtensions), ("Sci", Sci.syntaxExtensions), ("Sed", Sed.syntaxExtensions), ("Sgml", Sgml.syntaxExtensions), ("Sql", Sql.syntaxExtensions), ("SqlMysql", SqlMysql.syntaxExtensions), ("SqlPostgresql", SqlPostgresql.syntaxExtensions), ("Tcl", Tcl.syntaxExtensions), ("Tcsh", Tcsh.syntaxExtensions), ("Texinfo", Texinfo.syntaxExtensions), ("Verilog", Verilog.syntaxExtensions), ("Vhdl", Vhdl.syntaxExtensions), ("Xml", Xml.syntaxExtensions), ("Xorg", Xorg.syntaxExtensions), ("Xslt", Xslt.syntaxExtensions), ("Xul", Xul.syntaxExtensions), ("Yacc", Yacc.syntaxExtensions), ("Yaml", Yaml.syntaxExtensions), ("Zsh", Zsh.syntaxExtensions)]
+languageExtensions = [("Abc", Abc.syntaxExtensions), ("Actionscript", Actionscript.syntaxExtensions), ("Ada", Ada.syntaxExtensions), ("Agda", Agda.syntaxExtensions), ("Alert", Alert.syntaxExtensions), ("Alert_indent", Alert_indent.syntaxExtensions), ("Apache", Apache.syntaxExtensions), ("Asn1", Asn1.syntaxExtensions), ("Asp", Asp.syntaxExtensions), ("Awk", Awk.syntaxExtensions), ("Bash", Bash.syntaxExtensions), ("Bibtex", Bibtex.syntaxExtensions), ("Boo", Boo.syntaxExtensions), ("C", C.syntaxExtensions), ("Changelog", Changelog.syntaxExtensions), ("Clojure", Clojure.syntaxExtensions), ("Cmake", Cmake.syntaxExtensions), ("Coffee", Coffee.syntaxExtensions), ("Coldfusion", Coldfusion.syntaxExtensions), ("Commonlisp", Commonlisp.syntaxExtensions), ("Cpp", Cpp.syntaxExtensions), ("Cs", Cs.syntaxExtensions), ("Css", Css.syntaxExtensions), ("Curry", Curry.syntaxExtensions), ("D", D.syntaxExtensions), ("Diff", Diff.syntaxExtensions), ("Djangotemplate", Djangotemplate.syntaxExtensions), ("Dot", Dot.syntaxExtensions), ("Doxygen", Doxygen.syntaxExtensions), ("Doxygenlua", Doxygenlua.syntaxExtensions), ("Dtd", Dtd.syntaxExtensions), ("Eiffel", Eiffel.syntaxExtensions), ("Email", Email.syntaxExtensions), ("Erlang", Erlang.syntaxExtensions), ("Fasm", Fasm.syntaxExtensions), ("Fortran", Fortran.syntaxExtensions), ("Fsharp", Fsharp.syntaxExtensions), ("Gcc", Gcc.syntaxExtensions), ("Glsl", Glsl.syntaxExtensions), ("Gnuassembler", Gnuassembler.syntaxExtensions), ("Go", Go.syntaxExtensions), ("Haskell", Haskell.syntaxExtensions), ("Haxe", Haxe.syntaxExtensions), ("Html", Html.syntaxExtensions), ("Ini", Ini.syntaxExtensions), ("Isocpp", Isocpp.syntaxExtensions), ("Java", Java.syntaxExtensions), ("Javadoc", Javadoc.syntaxExtensions), ("Javascript", Javascript.syntaxExtensions), ("Json", Json.syntaxExtensions), ("Jsp", Jsp.syntaxExtensions), ("Julia", Julia.syntaxExtensions), ("Latex", Latex.syntaxExtensions), ("Lex", Lex.syntaxExtensions), ("Lilypond", Lilypond.syntaxExtensions), ("LiterateCurry", LiterateCurry.syntaxExtensions), ("LiterateHaskell", LiterateHaskell.syntaxExtensions), ("Lua", Lua.syntaxExtensions), ("M4", M4.syntaxExtensions), ("Makefile", Makefile.syntaxExtensions), ("Mandoc", Mandoc.syntaxExtensions), ("Markdown", Markdown.syntaxExtensions), ("Mathematica", Mathematica.syntaxExtensions), ("Matlab", Matlab.syntaxExtensions), ("Maxima", Maxima.syntaxExtensions), ("Mediawiki", Mediawiki.syntaxExtensions), ("Metafont", Metafont.syntaxExtensions), ("Mips", Mips.syntaxExtensions), ("Modelines", Modelines.syntaxExtensions), ("Modula2", Modula2.syntaxExtensions), ("Modula3", Modula3.syntaxExtensions), ("Monobasic", Monobasic.syntaxExtensions), ("Nasm", Nasm.syntaxExtensions), ("Noweb", Noweb.syntaxExtensions), ("Objectivec", Objectivec.syntaxExtensions), ("Objectivecpp", Objectivecpp.syntaxExtensions), ("Ocaml", Ocaml.syntaxExtensions), ("Octave", Octave.syntaxExtensions), ("Opencl", Opencl.syntaxExtensions), ("Pascal", Pascal.syntaxExtensions), ("Perl", Perl.syntaxExtensions), ("Php", Php.syntaxExtensions), ("Pike", Pike.syntaxExtensions), ("Postscript", Postscript.syntaxExtensions), ("Prolog", Prolog.syntaxExtensions), ("Pure", Pure.syntaxExtensions), ("Python", Python.syntaxExtensions), ("R", R.syntaxExtensions), ("Relaxng", Relaxng.syntaxExtensions), ("Relaxngcompact", Relaxngcompact.syntaxExtensions), ("Rest", Rest.syntaxExtensions), ("Rhtml", Rhtml.syntaxExtensions), ("Roff", Roff.syntaxExtensions), ("Ruby", Ruby.syntaxExtensions), ("Rust", Rust.syntaxExtensions), ("Scala", Scala.syntaxExtensions), ("Scheme", Scheme.syntaxExtensions), ("Sci", Sci.syntaxExtensions), ("Sed", Sed.syntaxExtensions), ("Sgml", Sgml.syntaxExtensions), ("Sql", Sql.syntaxExtensions), ("SqlMysql", SqlMysql.syntaxExtensions), ("SqlPostgresql", SqlPostgresql.syntaxExtensions), ("Tcl", Tcl.syntaxExtensions), ("Tcsh", Tcsh.syntaxExtensions), ("Texinfo", Texinfo.syntaxExtensions), ("Verilog", Verilog.syntaxExtensions), ("Vhdl", Vhdl.syntaxExtensions), ("Xml", Xml.syntaxExtensions), ("Xorg", Xorg.syntaxExtensions), ("Xslt", Xslt.syntaxExtensions), ("Xul", Xul.syntaxExtensions), ("Yacc", Yacc.syntaxExtensions), ("Yaml", Yaml.syntaxExtensions), ("Zsh", Zsh.syntaxExtensions)]
 
 -- | Returns a list of languages appropriate for the given file extension.
 languagesByExtension :: String -> [String]
@@ -152,7 +153,7 @@
 -- extension (if unique).
 -- The parsers read the input lazily and parse line by line;
 -- results are returned immediately.
--- Supported languages: @abc@, @actionscript@, @ada@, @alert@, @alert_indent@, @apache@, @asn1@, @asp@, @awk@, @bash@, @bibtex@, @boo@, @c@, @changelog@, @clojure@, @cmake@, @coffee@, @coldfusion@, @commonlisp@, @cpp@, @cs@, @css@, @curry@, @d@, @diff@, @djangotemplate@, @dot@, @doxygen@, @doxygenlua@, @dtd@, @eiffel@, @email@, @erlang@, @fasm@, @fortran@, @fsharp@, @gcc@, @glsl@, @gnuassembler@, @go@, @haskell@, @haxe@, @html@, @ini@, @isocpp@, @java@, @javadoc@, @javascript@, @json@, @jsp@, @julia@, @latex@, @lex@, @lilypond@, @literatecurry@, @literatehaskell@, @lua@, @m4@, @makefile@, @mandoc@, @markdown@, @mathematica@, @matlab@, @maxima@, @mediawiki@, @metafont@, @mips@, @modelines@, @modula2@, @modula3@, @monobasic@, @nasm@, @noweb@, @objectivec@, @objectivecpp@, @ocaml@, @octave@, @opencl@, @pascal@, @perl@, @php@, @pike@, @postscript@, @prolog@, @pure@, @python@, @r@, @relaxng@, @relaxngcompact@, @rest@, @rhtml@, @roff@, @ruby@, @rust@, @scala@, @scheme@, @sci@, @sed@, @sgml@, @sql@, @sqlmysql@, @sqlpostgresql@, @tcl@, @tcsh@, @texinfo@, @verilog@, @vhdl@, @xml@, @xorg@, @xslt@, @xul@, @yacc@, @yaml@, @zsh@.
+-- Supported languages: @abc@, @actionscript@, @ada@, @agda@, @alert@, @alert_indent@, @apache@, @asn1@, @asp@, @awk@, @bash@, @bibtex@, @boo@, @c@, @changelog@, @clojure@, @cmake@, @coffee@, @coldfusion@, @commonlisp@, @cpp@, @cs@, @css@, @curry@, @d@, @diff@, @djangotemplate@, @dot@, @doxygen@, @doxygenlua@, @dtd@, @eiffel@, @email@, @erlang@, @fasm@, @fortran@, @fsharp@, @gcc@, @glsl@, @gnuassembler@, @go@, @haskell@, @haxe@, @html@, @ini@, @isocpp@, @java@, @javadoc@, @javascript@, @json@, @jsp@, @julia@, @latex@, @lex@, @lilypond@, @literatecurry@, @literatehaskell@, @lua@, @m4@, @makefile@, @mandoc@, @markdown@, @mathematica@, @matlab@, @maxima@, @mediawiki@, @metafont@, @mips@, @modelines@, @modula2@, @modula3@, @monobasic@, @nasm@, @noweb@, @objectivec@, @objectivecpp@, @ocaml@, @octave@, @opencl@, @pascal@, @perl@, @php@, @pike@, @postscript@, @prolog@, @pure@, @python@, @r@, @relaxng@, @relaxngcompact@, @rest@, @rhtml@, @roff@, @ruby@, @rust@, @scala@, @scheme@, @sci@, @sed@, @sgml@, @sql@, @sqlmysql@, @sqlpostgresql@, @tcl@, @tcsh@, @texinfo@, @verilog@, @vhdl@, @xml@, @xorg@, @xslt@, @xul@, @yacc@, @yaml@, @zsh@.
 highlightAs :: String         -- ^ Language syntax (e.g. "haskell") or extension (e.g. "hs").
             -> String         -- ^ Source code to highlight
             -> [SourceLine]   -- ^ List of highlighted source lines
@@ -167,6 +168,7 @@
         "abc" -> Abc.highlight
         "actionscript" -> Actionscript.highlight
         "ada" -> Ada.highlight
+        "agda" -> Agda.highlight
         "alert" -> Alert.highlight
         "alert_indent" -> Alert_indent.highlight
         "apache" -> Apache.highlight
diff --git a/Text/Highlighting/Kate/Syntax/Agda.hs b/Text/Highlighting/Kate/Syntax/Agda.hs
new file mode 100644
--- /dev/null
+++ b/Text/Highlighting/Kate/Syntax/Agda.hs
@@ -0,0 +1,131 @@
+{- This module was generated from data in the Kate syntax
+   highlighting file agda.xml, version 1.0, by Matthias C. M. Troffaes -}
+
+module Text.Highlighting.Kate.Syntax.Agda
+          (highlight, parseExpression, syntaxName, syntaxExtensions)
+where
+import Text.Highlighting.Kate.Types
+import Text.Highlighting.Kate.Common
+import Text.ParserCombinators.Parsec hiding (State)
+import Control.Monad.State
+import Data.Char (isSpace)
+import qualified Data.Set as Set
+
+-- | Full name of language.
+syntaxName :: String
+syntaxName = "Agda"
+
+-- | Filename extensions for this language.
+syntaxExtensions :: String
+syntaxExtensions = "*.agda"
+
+-- | Highlight source code using this syntax definition.
+highlight :: String -> [SourceLine]
+highlight input = evalState (mapM parseSourceLine $ lines input) startingState
+
+parseSourceLine :: String -> State SyntaxState SourceLine
+parseSourceLine = mkParseSourceLine (parseExpression Nothing)
+
+-- | Parse an expression using appropriate local context.
+parseExpression :: Maybe (String,String)
+                -> KateParser Token
+parseExpression mbcontext = do
+  (lang,cont) <- maybe currentContext return mbcontext
+  result <- parseRules (lang,cont)
+  optional $ do eof
+                updateState $ \st -> st{ synStPrevChar = '\n' }
+                pEndLine
+  return result
+
+startingState = SyntaxState {synStContexts = [("Agda","code")], synStLineNumber = 0, synStPrevChar = '\n', synStPrevNonspace = False, synStCaseSensitive = True, synStKeywordCaseSensitive = True, synStCaptures = []}
+
+pEndLine = do
+  updateState $ \st -> st{ synStPrevNonspace = False }
+  context <- currentContext
+  contexts <- synStContexts `fmap` getState
+  if length contexts >= 2
+    then case context of
+      ("Agda","code") -> return ()
+      ("Agda","comment") -> (popContext) >> pEndLine
+      ("Agda","comments") -> return ()
+      ("Agda","hole") -> return ()
+      ("Agda","char") -> (popContext) >> pEndLine
+      ("Agda","string") -> return ()
+      _ -> return ()
+    else return ()
+
+withAttribute attr txt = do
+  when (null txt) $ fail "Parser matched no text"
+  updateState $ \st -> st { synStPrevChar = last txt
+                          , synStPrevNonspace = synStPrevNonspace st || not (all isSpace txt) }
+  return (attr, txt)
+
+list_reserved_keywords = Set.fromList $ words $ "abstract codata coinductive constructor data field forall hiding import in inductive infix infixl infixr let open pattern postulate primitive private public module mutual quote quoteGoal quoteTerm record renaming rewrite syntax to unquote using where with"
+
+regex_'5c'7b'2d'23'2e'2a'23'2d'5c'7d = compileRegex True "\\{-#.*#-\\}"
+regex_'28Prop'7cSet'5b₀'2d₉'5d'2b'7cSet'5b0'2d9'5d'2a'29'28'3f'3d'28'5b'5f'3b'2e'22'28'29'7b'7d'40'5d'7c'5cs'7c'24'29'29 = compileRegex True "(Prop|Set[\8320-\8329]+|Set[0-9]*)(?=([_;.\"(){}@]|\\s|$))"
+regex_'28'2d'3e'7c'2192'7c'2200'7cλ'7c'3a'7c'3d'7c'5c'7c'29'28'3f'3d'28'5b'5f'3b'2e'22'28'29'7b'7d'40'5d'7c'5cs'7c'24'29'29 = compileRegex True "(->|\8594|\8704|\955|:|=|\\|)(?=([_;.\"(){}@]|\\s|$))"
+regex_'5cd'2b'5c'2e'5cd'2b'28'3f'3d'28'5b'5f'3b'2e'22'28'29'7b'7d'40'5d'7c'5cs'7c'24'29'29 = compileRegex True "\\d+\\.\\d+(?=([_;.\"(){}@]|\\s|$))"
+regex_'5b0'2d9'5d'2b'28'3f'3d'28'5b'5f'3b'2e'22'28'29'7b'7d'40'5d'7c'5cs'7c'24'29'29 = compileRegex True "[0-9]+(?=([_;.\"(){}@]|\\s|$))"
+regex_'5b'5e'5f'3b'2e'22'28'29'7b'7d'40'5cs'5d'2b = compileRegex True "[^_;.\"(){}@\\s]+"
+
+parseRules ("Agda","code") =
+  (((pRegExpr regex_'5c'7b'2d'23'2e'2a'23'2d'5c'7d >>= withAttribute OtherTok))
+   <|>
+   ((pKeyword " \n\t.();{}_;.\"(){}@" list_reserved_keywords >>= withAttribute KeywordTok))
+   <|>
+   ((pRegExpr regex_'28Prop'7cSet'5b₀'2d₉'5d'2b'7cSet'5b0'2d9'5d'2a'29'28'3f'3d'28'5b'5f'3b'2e'22'28'29'7b'7d'40'5d'7c'5cs'7c'24'29'29 >>= withAttribute DataTypeTok))
+   <|>
+   ((pRegExpr regex_'28'2d'3e'7c'2192'7c'2200'7cλ'7c'3a'7c'3d'7c'5c'7c'29'28'3f'3d'28'5b'5f'3b'2e'22'28'29'7b'7d'40'5d'7c'5cs'7c'24'29'29 >>= withAttribute OtherTok))
+   <|>
+   ((pRegExpr regex_'5cd'2b'5c'2e'5cd'2b'28'3f'3d'28'5b'5f'3b'2e'22'28'29'7b'7d'40'5d'7c'5cs'7c'24'29'29 >>= withAttribute FloatTok))
+   <|>
+   ((pRegExpr regex_'5b0'2d9'5d'2b'28'3f'3d'28'5b'5f'3b'2e'22'28'29'7b'7d'40'5d'7c'5cs'7c'24'29'29 >>= withAttribute DecValTok))
+   <|>
+   ((pDetectChar False '\'' >>= withAttribute CharTok) >>~ pushContext ("Agda","char"))
+   <|>
+   ((pDetectChar False '"' >>= withAttribute StringTok) >>~ pushContext ("Agda","string"))
+   <|>
+   ((pDetect2Chars False '-' '-' >>= withAttribute CommentTok) >>~ pushContext ("Agda","comment"))
+   <|>
+   ((pDetect2Chars False '{' '-' >>= withAttribute CommentTok) >>~ pushContext ("Agda","comments"))
+   <|>
+   ((pDetect2Chars False '{' '!' >>= withAttribute OtherTok) >>~ pushContext ("Agda","hole"))
+   <|>
+   ((pAnyChar "_;.\"(){}@\\\\" >>= withAttribute OtherTok))
+   <|>
+   ((pRegExpr regex_'5b'5e'5f'3b'2e'22'28'29'7b'7d'40'5cs'5d'2b >>= withAttribute NormalTok))
+   <|>
+   (currentContext >>= \x -> guard (x == ("Agda","code")) >> pDefault >>= withAttribute NormalTok))
+
+parseRules ("Agda","comment") =
+  (currentContext >>= \x -> guard (x == ("Agda","comment")) >> pDefault >>= withAttribute CommentTok)
+
+parseRules ("Agda","comments") =
+  (((pDetect2Chars False '{' '-' >>= withAttribute CommentTok) >>~ pushContext ("Agda","comments"))
+   <|>
+   ((pDetect2Chars False '-' '}' >>= withAttribute CommentTok) >>~ (popContext))
+   <|>
+   (currentContext >>= \x -> guard (x == ("Agda","comments")) >> pDefault >>= withAttribute CommentTok))
+
+parseRules ("Agda","hole") =
+  (((pDetect2Chars False '!' '}' >>= withAttribute OtherTok) >>~ (popContext))
+   <|>
+   (currentContext >>= \x -> guard (x == ("Agda","hole")) >> pDefault >>= withAttribute OtherTok))
+
+parseRules ("Agda","char") =
+  (((pDetect2Chars False '\\' '\'' >>= withAttribute CharTok))
+   <|>
+   ((pDetectChar False '\'' >>= withAttribute CharTok) >>~ (popContext))
+   <|>
+   (currentContext >>= \x -> guard (x == ("Agda","char")) >> pDefault >>= withAttribute CharTok))
+
+parseRules ("Agda","string") =
+  (((pDetect2Chars False '\\' '"' >>= withAttribute StringTok))
+   <|>
+   ((pDetectChar False '"' >>= withAttribute StringTok) >>~ (popContext))
+   <|>
+   (currentContext >>= \x -> guard (x == ("Agda","string")) >> pDefault >>= withAttribute StringTok))
+
+
+parseRules x = parseRules ("Agda","code") <|> fail ("Unknown context" ++ show x)
diff --git a/changelog b/changelog
--- a/changelog
+++ b/changelog
@@ -1,3 +1,8 @@
+highlighting-kate 0.5.10 (09 Nov 2014)
+
+  * Added support for Agda (Matthias C. M. Troffaes).
+  * Made doctype case-insensitive in HTML 5 (Ondřej Žára).
+
 highlighting-kate 0.5.9 (24 Aug 2014)
 
   * Added cabal test suite.
diff --git a/highlighting-kate.cabal b/highlighting-kate.cabal
--- a/highlighting-kate.cabal
+++ b/highlighting-kate.cabal
@@ -1,5 +1,5 @@
 Name:                highlighting-kate
-Version:             0.5.9
+Version:             0.5.10
 Cabal-Version:       >= 1.10
 Build-Type:          Simple
 Category:            Text
@@ -117,6 +117,7 @@
                      Text.Highlighting.Kate.Syntax.Abc
                      Text.Highlighting.Kate.Syntax.Actionscript
                      Text.Highlighting.Kate.Syntax.Ada
+                     Text.Highlighting.Kate.Syntax.Agda
                      Text.Highlighting.Kate.Syntax.Alert
                      Text.Highlighting.Kate.Syntax.Alert_indent
                      Text.Highlighting.Kate.Syntax.Apache
diff --git a/xml/agda.xml b/xml/agda.xml
new file mode 100644
--- /dev/null
+++ b/xml/agda.xml
@@ -0,0 +1,107 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<!DOCTYPE language SYSTEM "language.dtd"[
+  <!ENTITY charsdelim "_;.&#34;(){}@">
+  <!ENTITY wordsep "(?=([&charsdelim;]|\s|$))">
+]>
+<language name="Agda" version="1.0" kateversion="3.4" section="Sources" extensions="*.agda" mimetype="text/x-agda" author="Matthias C. M. Troffaes" license="LGPL">
+  <highlighting>
+    <list name="reserved keywords">
+      <item> abstract </item>
+      <item> codata </item>
+      <item> coinductive </item>
+      <item> constructor </item>
+      <item> data </item>
+      <item> field </item>
+      <item> forall </item>
+      <item> hiding </item>
+      <item> import </item>
+      <item> in </item>
+      <item> inductive </item>
+      <item> infix </item>
+      <item> infixl  </item>
+      <item> infixr </item>
+      <item> let </item>
+      <item> open </item>
+      <item> pattern </item>
+      <item> postulate </item>
+      <item> primitive </item>
+      <item> private </item>
+      <item> public </item>
+      <item> module </item>
+      <item> mutual </item>
+      <item> quote </item>
+      <item> quoteGoal </item>
+      <item> quoteTerm </item>
+      <item> record </item>
+      <item> renaming </item>
+      <item> rewrite </item>
+      <item> syntax </item>
+      <item> to </item>
+      <item> unquote </item>
+      <item> using </item>
+      <item> where </item>
+      <item> with </item>
+    </list>
+    <contexts>
+      <context attribute="Normal" lineEndContext="#stay" name="code">
+        <RegExpr attribute="Pragma"  context="#stay" String="\{-#.*#-\}" />
+        <keyword attribute="Keyword" context="#stay" String="reserved keywords" />
+        <RegExpr attribute="Type"    context="#stay" String="(Prop|Set[₀-₉]+|Set[0-9]*)&wordsep;" />
+        <RegExpr attribute="Special" context="#stay" String="(-&gt;|→|∀|λ|:|=|\|)&wordsep;" />
+        <RegExpr attribute="Float"   context="#stay" String="\d+\.\d+&wordsep;" />
+        <RegExpr attribute="Decimal" context="#stay" String="[0-9]+&wordsep;" />
+        <DetectChar attribute="Char"   context="char"   char="'" />
+        <DetectChar attribute="String" context="string" char="&quot;" />
+        <Detect2Chars attribute="Comment" context="comment"  char="-"  char1="-" />
+        <Detect2Chars attribute="Comment" context="comments" char="{" char1="-" />
+        <Detect2Chars attribute="Hole"    context="hole"     char="{" char1="!" />
+        <!-- delimiters which cannot be part of an identifier, or
+             backslash which starts a lambda expression -->
+        <AnyChar      attribute="Special" context="#stay" String="&charsdelim;\\" />
+        <!-- any other identifier (can contain backslash and single
+             quote anywhere except at start, but these two special
+             cases are already taken care off above) -->
+        <RegExpr attribute="Normal" context="#stay" String="[^&charsdelim;\s]+" />
+      </context>
+      <context attribute="Comment" lineEndContext="#pop" name="comment" />
+      <context attribute="Comment" lineEndContext="#stay" name="comments">
+        <Detect2Chars attribute="Comment" context="comments" char="{" char1="-" /> <!-- for nested comments -->
+        <Detect2Chars attribute="Comment" context="#pop" char="-" char1="}" />
+      </context>
+      <context attribute="Hole" lineEndContext="#stay" name="hole">
+        <Detect2Chars attribute="Hole" context="#pop" char="!" char1="}" />
+      </context>
+      <context attribute="Char" lineEndContext="#pop" name="char">
+        <Detect2Chars attribute="Char" context="#stay" char="\\" char1="'" />
+        <DetectChar   attribute="Char" context="#pop"  char="'" />
+      </context>
+      <context attribute="String" lineEndContext="#stay" name="string">
+        <Detect2Chars attribute="String" context="#stay" char="\\" char1="&quot;" />
+        <DetectChar   attribute="String" context="#pop"  char="&quot;" />
+      </context>
+    </contexts>
+    <itemDatas>
+      <itemData name="Normal"   defStyleNum="dsNormal"   spellChecking="false" />
+      <itemData name="Comment"  defStyleNum="dsComment"  />
+      <itemData name="Pragma"   defStyleNum="dsOthers"   spellChecking="false" />
+      <itemData name="Hole"     defStyleNum="dsOthers"   spellChecking="false" />
+      <itemData name="Keyword"  defStyleNum="dsKeyword"  spellChecking="false" />
+      <itemData name="Type"     defStyleNum="dsDataType" spellChecking="false" />
+      <itemData name="Special"  defStyleNum="dsOthers"   spellChecking="false" />
+      <itemData name="Decimal"  defStyleNum="dsDecVal"   spellChecking="false" />
+      <itemData name="Float"    defStyleNum="dsFloat"    spellChecking="false" />
+      <itemData name="Char"     defStyleNum="dsChar"     spellChecking="false" />
+      <itemData name="String"   defStyleNum="dsString" />
+    </itemDatas>
+  </highlighting>
+  <general>
+    <folding indentationsensitive="1"/>
+    <comments>
+      <comment name="singleLine" start="--" />
+      <comment name="multiLine" start="{-" end="-}" />
+    </comments>
+    <keywords casesensitive="1"
+              weakDeliminator=":!+,-&lt;=&gt;%&amp;*/?[]^|~\\"
+              additionalDeliminator="&charsdelim;" />
+  </general>
+</language>
diff --git a/xml/html.xml b/xml/html.xml
--- a/xml/html.xml
+++ b/xml/html.xml
@@ -17,7 +17,8 @@
     <DetectIdentifier/>
     <StringDetect attribute="Comment" context="Comment" String="&lt;!--" beginRegion="comment" />
     <StringDetect attribute="CDATA" context="CDATA" String="&lt;![CDATA[" beginRegion="cdata" />
-    <RegExpr attribute="Doctype" context="Doctype" String="&lt;!DOCTYPE\s+" insensitive="true" beginRegion="doctype"  />
+    <!-- NOTE: the kate source had insensitive="true", but "false" is correct -->
+    <RegExpr attribute="Doctype" context="Doctype" String="&lt;!DOCTYPE\s+" insensitive="false" beginRegion="doctype"  />
     <RegExpr attribute="Processing Instruction" context="PI" String="&lt;\?[\w:-]*" beginRegion="pi" />
     <RegExpr attribute="Element" context="CSS" String="&lt;style\b" insensitive="true" beginRegion="style" />
     <RegExpr attribute="Element" context="JS" String="&lt;script\b" insensitive="true" beginRegion="script" />