<div dir="ltr"><div class="gmail_extra"><div class="gmail_quote"><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Note that inferring the file format also has to be implemented for the emacs-mode and all other front-ends to Agda.  I shortage of (willing) emacs-lisp programmers in our team, I&#39;d like to avoid anything that complicates the emacs-mode.<br></blockquote><div><br></div><div>The procedure to decide which format it is is relatively simple, but I too feel that it shouldn&#39;t be implemented in the agda-mode. Since agda-mode already needs an instance of Agda running in order to highlight files, the procedure could simply be exposed through the interactive mode.</div><div><br></div><div>If the format is decided to be LaTeX, agda-mode could call its (internal?) LaTeX highlighter. If it isn&#39;t, we could rule that the host language is simply <i>not</i> highlighted---or we could try to call an external highlighter. I&#39;m hoping that most highlighters wouldn&#39;t touch a nested code block anyway.</div><div><br></div><div>All in all I don&#39;t think that the changes would be that great. At the moment it already seems to work fine (with the host language not being highlighted if it&#39;s not LaTeX) but I feel this is probably due to the highlighter not finding anything to highlight.</div></div></div></div>