# HG changeset patch
# User wenzelm
# Date 980103292 -3600
# Node ID a555bfb66c2dcbbdddc309a8022fe1141c828363
# Parent  ea024d0254635c6e99a9bc73e2c41e54679b79ae
setup indent;

diff -r ea024d025463 -r a555bfb66c2d src/Pure/Interface/proof_general.ML
--- a/src/Pure/Interface/proof_general.ML	Sun Jan 21 19:54:05 2001 +0100
+++ b/src/Pure/Interface/proof_general.ML	Sun Jan 21 19:54:52 2001 +0100
@@ -88,7 +88,7 @@
     let val syms = Symbol.explode s
     in (implode (map (fn "\\" => "\\\\" | c => c) syms), real (Symbol.length syms)) end;
 
-fun setup_xsymbols_output () = Symbol.add_mode "xsymbols" xsymbols_output;
+fun setup_xsymbols_output () = Symbol.add_mode "xsymbols" (xsymbols_output, Symbol.default_indent);
 
 
 (* messages *)
@@ -318,6 +318,5 @@
 
 end;
 
-(*this hack avoids problems with escapes in ML commands; required for
-  Proof General 3.2*)
+(*a hack for Proof General 3.2 to avoid problems with escapes in ML commands*)
 infix \\\\ val op \\\\ = op \\;
diff -r ea024d025463 -r a555bfb66c2d src/Pure/Thy/html.ML
--- a/src/Pure/Thy/html.ML	Sun Jan 21 19:54:05 2001 +0100
+++ b/src/Pure/Thy/html.ML	Sun Jan 21 19:54:52 2001 +0100
@@ -115,7 +115,7 @@
 end;
 
 
-val _ = Symbol.add_mode htmlN output_width;
+val _ = Symbol.add_mode htmlN (output_width, Symbol.default_indent);
 
 
 (* token translations *)