src/Pure/Thy/latex.ML
changeset 23703 1b6a2c119151
parent 23621 e070a6ab1891
child 27344 d44490b06190
equal deleted inserted replaced
23702:58ca991e0702 23703:1b6a2c119151
   174 
   174 
   175 fun latex_indent "" _ = ""
   175 fun latex_indent "" _ = ""
   176   | latex_indent s _ = enclose "\\isaindent{" "}" s;
   176   | latex_indent s _ = enclose "\\isaindent{" "}" s;
   177 
   177 
   178 val _ = Output.add_mode latexN latex_output Symbol.encode_raw;
   178 val _ = Output.add_mode latexN latex_output Symbol.encode_raw;
   179 val _ = Pretty.add_mode latexN latex_indent latex_markup;
   179 val _ = Markup.add_mode latexN latex_markup;
       
   180 val _ = Pretty.add_mode latexN latex_indent;
   180 
   181 
   181 end;
   182 end;