# HG changeset patch
# User wenzelm
# Date 980103325 -3600
# Node ID 36741b4fe1091e6ce61d7f0c012ba2f622cdcdb8
# Parent  a555bfb66c2dcbbdddc309a8022fe1141c828363
setuo indent: \isaindent;

diff -r a555bfb66c2d -r 36741b4fe109 src/Pure/Thy/latex.ML
--- a/src/Pure/Thy/latex.ML	Sun Jan 21 19:54:52 2001 +0100
+++ b/src/Pure/Thy/latex.ML	Sun Jan 21 19:55:25 2001 +0100
@@ -144,10 +144,13 @@
   let val syms = Symbol.explode str
   in (output_symbols syms, real (Symbol.length syms)) end;
 
+fun latex_indent "" = ""
+  | latex_indent s = enclose "\\isaindent{" "}" s;
+
 val token_translation =
   map (fn s => (latexN, s, latex_output)) Syntax.standard_token_classes;
 
-val _ = Symbol.add_mode latexN latex_output;
+val _ = Symbol.add_mode latexN (latex_output, latex_indent o #1);
 val setup = [Theory.add_tokentrfuns token_translation];