# HG changeset patch # User wenzelm # Date 1726773206 -7200 # Node ID 47793a46d06c3daf17ebc0f7d896e03be7f52e1b # Parent 05f17df447b6c1deecb9f76256514091ba1b3877 support for Markup.expression properties in pretty-blocks; diff -r 05f17df447b6 -r 47793a46d06c src/Pure/PIDE/markup.ML --- a/src/Pure/PIDE/markup.ML Thu Sep 19 20:56:47 2024 +0200 +++ b/src/Pure/PIDE/markup.ML Thu Sep 19 21:13:26 2024 +0200 @@ -460,7 +460,7 @@ val unbreakableN = "unbreakable"; val indentN = "indent"; -val block_properties = [markupN, consistentN, unbreakableN, indentN]; +val block_properties = [expressionN, markupN, consistentN, unbreakableN, indentN]; val widthN = "width"; diff -r 05f17df447b6 -r 47793a46d06c src/Pure/Syntax/printer.ML --- a/src/Pure/Syntax/printer.ML Thu Sep 19 20:56:47 2024 +0200 +++ b/src/Pure/Syntax/printer.ML Thu Sep 19 21:13:26 2024 +0200 @@ -247,7 +247,7 @@ val (bTs, args') = synT m (bsymbs, args); val (Ts, args'') = synT m (symbs, args'); val T = - Pretty.markup_block {markup = markup, consistent = consistent, indent = indent} bTs + Pretty.markup_blocks {markup = markup, consistent = consistent, indent = indent} bTs |> unbreakable ? Pretty.unbreakable; in (T :: Ts, args'') end | synT m (Break i :: symbs, args) = diff -r 05f17df447b6 -r 47793a46d06c src/Pure/Syntax/syntax_ext.ML --- a/src/Pure/Syntax/syntax_ext.ML Thu Sep 19 20:56:47 2024 +0200 +++ b/src/Pure/Syntax/syntax_ext.ML Thu Sep 19 21:13:26 2024 +0200 @@ -7,7 +7,7 @@ signature SYNTAX_EXT = sig datatype mfix = Mfix of Symbol_Pos.T list * typ * string * int list * int * Position.T - type block = {markup: Markup.T, consistent: bool, unbreakable: bool, indent: int} + type block = {markup: Markup.T list, consistent: bool, unbreakable: bool, indent: int} val block_indent: int -> block datatype xsymb = Delim of string | @@ -60,10 +60,10 @@ Space s: some white space for printing Bg, Brk, En: blocks and breaks for pretty printing*) -type block = {markup: Markup.T, consistent: bool, unbreakable: bool, indent: int}; +type block = {markup: Markup.T list, consistent: bool, unbreakable: bool, indent: int}; fun block_indent indent : block = - {markup = Markup.empty, consistent = false, unbreakable = false, indent = indent}; + {markup = [], consistent = false, unbreakable = false, indent = indent}; datatype xsymb = Delim of string | @@ -171,6 +171,10 @@ val get_bool = get_property false true (Value.parse_bool o #1); val get_nat = get_property 0 1 (Value.parse_nat o #1); +fun get_expression_markup ctxt = + get_property NONE (SOME (Markup.expression "")) (SOME o Markup_Expression.check ctxt) + Markup.expressionN; + end; @@ -211,24 +215,27 @@ else [] | reports_text_of _ = []; -fun read_block_properties ss = +fun read_block_properties ctxt ss = let val props = read_properties ss; + val more_markups = the_list (get_expression_markup ctxt props); + val markup_name = get_string Markup.markupN props; val markup_props = props |> map_filter (fn (a, opt_b) => if member (op =) Markup.block_properties (#1 a) then NONE - else SOME (a, the_default ("", Position.none) opt_b)); - val markup = (markup_name, map (apply2 #1) markup_props); - val _ = - if markup_name = "" andalso not (null markup_props) then - error ("Markup name required for block properties: " ^ show_names (map #1 markup_props)) - else (); + else SOME (a, the_default ("true", Position.none) opt_b)); + val markups = + if markup_name <> "" then [(markup_name, map (apply2 #1) markup_props)] + else if null markup_props then [] + else error ("Markup name required for block properties: " ^ show_names (map #1 markup_props)); - val consistent = get_bool Markup.consistentN props; - val unbreakable = get_bool Markup.unbreakableN props; - val indent = get_nat Markup.indentN props; - in Bg {markup = markup, consistent = consistent, unbreakable = unbreakable, indent = indent} end + val block: block = + {markup = more_markups @ markups, + consistent = get_bool Markup.consistentN props, + unbreakable = get_bool Markup.unbreakableN props, + indent = get_nat Markup.indentN props}; + in Bg block end handle ERROR msg => let val reported_texts = @@ -246,30 +253,31 @@ $$ "'" |-- scan_one ((not o Symbol.is_blank) andf Symbol.not_eof) >> single || scan_one ((not o is_meta) andf (not o Symbol.is_blank) andf Symbol.not_eof) >> single; -val scan_sym = - $$ "_" >> K (Argument ("", 0)) || - $$ "\" >> K index || - $$ "(" |-- - (Symbol_Pos.scan_cartouche_content err_prefix >> read_block_properties || - scan_many Symbol.is_digit >> read_block_indent) || - $$ ")" >> K En || - $$ "/" -- $$ "/" >> K (Brk ~1) || - $$ "/" |-- scan_many Symbol.is_space >> (Brk o length) || - scan_many1 Symbol.is_space >> (Space o Symbol_Pos.content) || - Scan.repeat1 scan_delim >> (Delim o Symbol_Pos.content o flat); +fun scan_symbs ctxt = + let + val scan_sym = + $$ "_" >> K (Argument ("", 0)) || + $$ "\" >> K index || + $$ "(" |-- + (Symbol_Pos.scan_cartouche_content err_prefix >> read_block_properties ctxt || + scan_many Symbol.is_digit >> read_block_indent) || + $$ ")" >> K En || + $$ "/" -- $$ "/" >> K (Brk ~1) || + $$ "/" |-- scan_many Symbol.is_space >> (Brk o length) || + scan_many1 Symbol.is_space >> (Space o Symbol_Pos.content) || + Scan.repeat1 scan_delim >> (Delim o Symbol_Pos.content o flat); -val scan_symb = - Scan.trace scan_sym >> (fn (syms, trace) => SOME (syms, #1 (Symbol_Pos.range trace))) || - $$ "'" -- scan_one Symbol.is_space >> K NONE; - -val scan_symbs = Scan.repeat scan_symb --| Scan.ahead (~$$ "'"); + val scan_symb = + Scan.trace scan_sym >> (fn (syms, trace) => SOME (syms, #1 (Symbol_Pos.range trace))) || + $$ "'" -- scan_one Symbol.is_space >> K NONE; + in Scan.repeat scan_symb --| Scan.ahead (~$$ "'") end; in fun read_mfix ctxt ss = let val xsymbs = - (case Scan.error (Scan.finite Symbol_Pos.stopper scan_symbs) ss of + (case Scan.error (Scan.finite Symbol_Pos.stopper (scan_symbs ctxt)) ss of (res, []) => map_filter I res | (_, (_, pos) :: _) => error (err_prefix ^ "bad input" ^ Position.here pos)); val _ = Context_Position.reports ctxt (maps reports_of xsymbs);