# HG changeset patch # User wenzelm # Date 1184078706 -7200 # Node ID 1b6a2c119151fa0dd03b97c4d9f65d55ab25af32 # Parent 58ca991e0702742c5d152251702b1eeb80eecf73 Markup.add_mode; diff -r 58ca991e0702 -r 1b6a2c119151 src/Pure/Thy/html.ML --- a/src/Pure/Thy/html.ML Tue Jul 10 16:45:05 2007 +0200 +++ b/src/Pure/Thy/html.ML Tue Jul 10 16:45:06 2007 +0200 @@ -455,6 +455,6 @@ (* mode output *) val _ = Output.add_mode htmlN output_width Symbol.encode_raw; -val _ = Pretty.add_mode htmlN Pretty.default_indent (span o #1); +val _ = Markup.add_mode htmlN (span o #1); end; diff -r 58ca991e0702 -r 1b6a2c119151 src/Pure/Thy/latex.ML --- a/src/Pure/Thy/latex.ML Tue Jul 10 16:45:05 2007 +0200 +++ b/src/Pure/Thy/latex.ML Tue Jul 10 16:45:06 2007 +0200 @@ -176,6 +176,7 @@ | latex_indent s _ = enclose "\\isaindent{" "}" s; val _ = Output.add_mode latexN latex_output Symbol.encode_raw; -val _ = Pretty.add_mode latexN latex_indent latex_markup; +val _ = Markup.add_mode latexN latex_markup; +val _ = Pretty.add_mode latexN latex_indent; end;