# HG changeset patch # User wenzelm # Date 1725914433 -7200 # Node ID 6896736dec386c98a6c4b0842770dbd803565d62 # Parent 2e3e2ec20e87eccd82d06684dfe54f31671a2b5c eliminate print mode "code_presentation" thanks to value-oriented Pretty.T operations; diff -r 2e3e2ec20e87 -r 6896736dec38 src/Tools/Code/code_printer.ML --- a/src/Tools/Code/code_printer.ML Mon Sep 09 22:04:46 2024 +0200 +++ b/src/Tools/Code/code_printer.ML Mon Sep 09 22:40:33 2024 +0200 @@ -115,8 +115,6 @@ val code_presentationN = "code_presentation"; val stmt_nameN = "stmt_name"; -val _ = Markup.add_mode code_presentationN YXML.markup_ops; -val _ = Pretty.add_mode code_presentationN Pretty.markup_ops; (** assembling and printing text pieces **) @@ -125,23 +123,20 @@ infixr 5 @|; fun x @@ y = [x, y]; fun xs @| y = xs @ [y]; -fun with_no_print_mode f = Print_Mode.setmp [] f; -val str = with_no_print_mode Pretty.str; +val str = Pretty.str; val concat = Pretty.block o Pretty.breaks; -val commas = with_no_print_mode Pretty.commas; -fun enclose l r = with_no_print_mode (Pretty.enclose l r); +val commas = Pretty.commas; +val enclose = Pretty.enclose; val brackets = enclose "(" ")" o Pretty.breaks; -fun enum sep l r = with_no_print_mode (Pretty.enum sep l r); +val enum = Pretty.enum; 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 = with_no_print_mode (Pretty.indent i); +val indent = Pretty.indent; -fun with_presentation_marker f = Print_Mode.setmp [code_presentationN] f; - -fun markup_stmt sym = with_presentation_marker - (Pretty.mark (code_presentationN, [(stmt_nameN, Code_Symbol.marker sym)])); +fun markup_stmt sym = + Pretty.mark (code_presentationN, [(stmt_nameN, Code_Symbol.marker sym)]); fun filter_presentation [] xml = Buffer.build (fold XML.add_content xml) @@ -162,7 +157,8 @@ in snd (fold filter xml (true, Buffer.empty)) end; fun format presentation_names width = - with_presentation_marker (Pretty.string_of_margin width) + Pretty.output_buffer (Pretty.markup_output_ops (SOME width)) + #> Buffer.content #> YXML.parse_body #> filter_presentation presentation_names #> Buffer.add "\n"