src/Pure/Thy/latex.ML
changeset 19265 cae36e16f3c0
parent 17218 64242b791c19
child 22648 8c6b4f7548e3
     1.1 --- a/src/Pure/Thy/latex.ML	Tue Mar 14 22:06:31 2006 +0100
     1.2 +++ b/src/Pure/Thy/latex.ML	Tue Mar 14 22:06:33 2006 +0100
     1.3 @@ -160,10 +160,12 @@
     1.4    let val syms = Symbol.explode str
     1.5    in (output_symbols syms, real (Symbol.length syms)) end;
     1.6  
     1.7 +fun latex_keyword cmd =
     1.8 +  apfst (enclose (if cmd then "\\isacommand{" else "\\isakeyword{") "}") o latex_output;
     1.9 +
    1.10  fun latex_indent "" = ""
    1.11    | latex_indent s = enclose "\\isaindent{" "}" s;
    1.12  
    1.13 -val _ = Output.add_mode latexN (latex_output, latex_indent o #1, Symbol.encode_raw);
    1.14 -
    1.15 +val _ = Output.add_mode latexN (latex_output, latex_keyword, latex_indent o #1, Symbol.encode_raw);
    1.16  
    1.17  end;