# HG changeset patch # User haftmann # Date 1285241001 -7200 # Node ID 6ab9781e6d11638ae0cd56071c1c5a1ddddbf81b # Parent 07549694e2f1267b00fb7b43f681bd4a1b4b2629 reverted cs 07549694e2f1 diff -r 07549694e2f1 -r 6ab9781e6d11 src/Tools/Code/code_printer.ML --- a/src/Tools/Code/code_printer.ML Thu Sep 23 11:29:22 2010 +0200 +++ b/src/Tools/Code/code_printer.ML Thu Sep 23 13:23:21 2010 +0200 @@ -115,19 +115,19 @@ infixr 5 @|; fun x @@ y = [x, y]; fun xs @| y = xs @ [y]; -val str = Print_Mode.with_modes [] Pretty.str; +val str = Print_Mode.setmp [] Pretty.str; val concat = Pretty.block o Pretty.breaks; -val commas = Print_Mode.with_modes [] Pretty.commas; -fun enclose l r = Print_Mode.with_modes [] (Pretty.enclose l r); +val commas = Print_Mode.setmp [] Pretty.commas; +fun enclose l r = Print_Mode.setmp [] (Pretty.enclose l r); val brackets = enclose "(" ")" o Pretty.breaks; -fun enum sep l r = Print_Mode.with_modes [] (Pretty.enum sep l r); +fun enum sep l r = Print_Mode.setmp [] (Pretty.enum sep l r); fun enum_default default sep l r [] = str default | enum_default default sep l r xs = enum sep l r xs; fun semicolon ps = Pretty.block [concat ps, str ";"]; fun doublesemicolon ps = Pretty.block [concat ps, str ";;"]; -fun indent i = Print_Mode.with_modes [] (Pretty.indent i); +fun indent i = Print_Mode.setmp [] (Pretty.indent i); -fun markup_stmt name = Print_Mode.with_modes [code_presentationN] +fun markup_stmt name = Print_Mode.setmp [code_presentationN] (Pretty.mark (code_presentationN, [(stmt_nameN, name)])); fun filter_presentation [] tree = @@ -150,7 +150,7 @@ in snd (fold filter tree (true, Buffer.empty)) end; fun format presentation_names width = - Print_Mode.with_modes [code_presentationN] (Pretty.string_of_margin width) + Print_Mode.setmp [code_presentationN] (Pretty.string_of_margin width) #> YXML.parse_body #> filter_presentation presentation_names #> Buffer.content;