--- 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;