1.1 --- a/src/Pure/Thy/latex.ML	Sat Jul 07 00:15:02 2007 +0200
     1.2 +++ b/src/Pure/Thy/latex.ML	Sat Jul 07 00:15:02 2007 +0200
     1.3 @@ -165,14 +165,17 @@
     1.4  
     1.5  fun latex_output str =
     1.6    let val syms = Symbol.explode str
     1.7 -  in (output_symbols syms, real (Symbol.length syms)) end;
     1.8 -
     1.9 -fun latex_keyword cmd =
    1.10 -  apfst (enclose (if cmd then "\\isacommand{" else "\\isakeyword{") "}") o latex_output;
    1.11 +  in (output_symbols syms, Symbol.length syms) end;
    1.12  
    1.13 -fun latex_indent "" = ""
    1.14 -  | latex_indent s = enclose "\\isaindent{" "}" s;
    1.15 +fun latex_markup (s, _) =
    1.16 +  if s = Markup.keywordN then ("\\isakeyword{", "}")
    1.17 +  else if s = Markup.commandN then ("\\isacommand{", "}")
    1.18 +  else ("", "");
    1.19  
    1.20 -val _ = Output.add_mode latexN (latex_output, latex_keyword, latex_indent o #1, Symbol.encode_raw);
    1.21 +fun latex_indent "" _ = ""
    1.22 +  | latex_indent s _ = enclose "\\isaindent{" "}" s;
    1.23 +
    1.24 +val _ = Output.add_mode latexN latex_output Symbol.encode_raw;
    1.25 +val _ = Pretty.add_mode latexN latex_indent latex_markup;
    1.26  
    1.27  end;