diff -r 55ef4d0bc250 -r e070a6ab1891 src/Pure/Thy/latex.ML
--- a/src/Pure/Thy/latex.ML	Sat Jul 07 00:15:02 2007 +0200
+++ b/src/Pure/Thy/latex.ML	Sat Jul 07 00:15:02 2007 +0200
@@ -165,14 +165,17 @@
 
 fun latex_output str =
   let val syms = Symbol.explode str
-  in (output_symbols syms, real (Symbol.length syms)) end;
-
-fun latex_keyword cmd =
-  apfst (enclose (if cmd then "\\isacommand{" else "\\isakeyword{") "}") o latex_output;
+  in (output_symbols syms, Symbol.length syms) end;
 
-fun latex_indent "" = ""
-  | latex_indent s = enclose "\\isaindent{" "}" s;
+fun latex_markup (s, _) =
+  if s = Markup.keywordN then ("\\isakeyword{", "}")
+  else if s = Markup.commandN then ("\\isacommand{", "}")
+  else ("", "");
 
-val _ = Output.add_mode latexN (latex_output, latex_keyword, latex_indent o #1, Symbol.encode_raw);
+fun latex_indent "" _ = ""
+  | latex_indent s _ = enclose "\\isaindent{" "}" s;
+
+val _ = Output.add_mode latexN latex_output Symbol.encode_raw;
+val _ = Pretty.add_mode latexN latex_indent latex_markup;
 
 end;