# 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 *)