# HG changeset patch # User wenzelm # Date 1459460193 -7200 # Node ID 75ee05386b9038071eb96e3ead70db2c530a9d19 # Parent 057e8dbe4326be5f553a5ae7a1dadff5f719195e explicit mixfix block properties; diff -r 057e8dbe4326 -r 75ee05386b90 src/Pure/General/pretty.ML --- a/src/Pure/General/pretty.ML Thu Mar 31 16:23:25 2016 +0200 +++ b/src/Pure/General/pretty.ML Thu Mar 31 23:36:33 2016 +0200 @@ -23,7 +23,9 @@ val default_indent: string -> int -> Output.output val add_mode: string -> (string -> int -> Output.output) -> unit type T - val make_block: Output.output * Output.output -> bool -> int -> T list -> T + val make_block: {markup: Output.output * Output.output, consistent: bool, indent: int} -> + T list -> T + val markup_block: {markup: Markup.T, consistent: bool, indent: int} -> T list -> T val str: string -> T val brk: int -> T val brk_indent: int -> int -> T @@ -119,7 +121,7 @@ | length (Break (_, wd, _)) = wd | length (Str (_, len)) = len; -fun make_block markup consistent indent body = +fun make_block {markup, consistent, indent} body = let fun body_length prts len = let @@ -133,8 +135,8 @@ end; in Block (markup, consistent, indent, body, body_length body 0) end; -fun markup_block markup indent es = - make_block (Markup.output markup) false indent es; +fun markup_block {markup, consistent, indent} es = + make_block {markup = Markup.output markup, consistent = consistent, indent = indent} es; @@ -149,11 +151,13 @@ fun breaks prts = Library.separate (brk 1) prts; fun fbreaks prts = Library.separate fbrk prts; -fun blk (ind, es) = markup_block Markup.empty ind es; +fun blk (indent, es) = + markup_block {markup = Markup.empty, consistent = false, indent = indent} es; + fun block prts = blk (2, prts); val strs = block o breaks o map str; -fun markup m = markup_block m 0; +fun markup m = markup_block {markup = m, consistent = false, indent = 0}; fun mark m prt = if m = Markup.empty then prt else markup m [prt]; fun mark_str (m, s) = mark m (str s); fun marks_str (ms, s) = fold_rev mark ms (str s); @@ -384,7 +388,8 @@ | to_ML _ (Str (s, len)) = ML_Pretty.String (s, FixedInt.fromInt len); fun from_ML (ML_Pretty.Block (m, consistent, indent, prts)) = - make_block m consistent (FixedInt.toInt indent) (map from_ML prts) + make_block {markup = m, consistent = consistent, indent = FixedInt.toInt indent} + (map from_ML prts) | from_ML (ML_Pretty.Break (force, wd, ind)) = Break (force, FixedInt.toInt wd, FixedInt.toInt ind) | from_ML (ML_Pretty.String (s, len)) = Str (s, FixedInt.toInt len); diff -r 057e8dbe4326 -r 75ee05386b90 src/Pure/PIDE/markup.ML --- a/src/Pure/PIDE/markup.ML Thu Mar 31 16:23:25 2016 +0200 +++ b/src/Pure/PIDE/markup.ML Thu Mar 31 23:36:33 2016 +0200 @@ -65,7 +65,9 @@ val pathN: string val path: string -> T val urlN: string val url: string -> T val docN: string val doc: string -> T - val indentN: string + val markupN: string val get_markup: Properties.T -> string + val consistentN: string val get_consistent: Properties.T -> bool + val indentN: string val get_indent: Properties.T -> int val widthN: string val blockN: string val block: bool -> int -> T val breakN: string val break: int -> int -> T @@ -382,8 +384,17 @@ (* pretty printing *) +val markupN = "markup"; +fun get_markup props = the_default "" (Properties.get props markupN); + val consistentN = "consistent"; +fun get_consistent props = + the_default false (Option.map parse_bool (Properties.get props consistentN)); + val indentN = "indent"; +fun get_indent props = + the_default 0 (Option.map parse_int (Properties.get props indentN)); + val widthN = "width"; val blockN = "block"; diff -r 057e8dbe4326 -r 75ee05386b90 src/Pure/Syntax/printer.ML --- a/src/Pure/Syntax/printer.ML Thu Mar 31 16:23:25 2016 +0200 +++ b/src/Pure/Syntax/printer.ML Thu Mar 31 23:36:33 2016 +0200 @@ -86,7 +86,7 @@ TypArg of int | String of bool * string | Break of int | - Block of int * symb list; + Block of {markup: Markup.T, consistent: bool, indent: int} * symb list; type prtabs = (string * ((symb list * int * int) list) Symtab.table) list; @@ -110,12 +110,12 @@ apfst (cons (arg s_p)) (xsyms_to_syms xsyms) | xsyms_to_syms (Syntax_Ext.Space s :: xsyms) = apfst (cons (String (false, s))) (xsyms_to_syms xsyms) - | xsyms_to_syms (Syntax_Ext.Bg i :: xsyms) = + | xsyms_to_syms (Syntax_Ext.Bg info :: xsyms) = let val (bsyms, xsyms') = xsyms_to_syms xsyms; val (syms, xsyms'') = xsyms_to_syms xsyms'; in - (Block (i, bsyms) :: syms, xsyms'') + (Block (info, bsyms) :: syms, xsyms'') end | xsyms_to_syms (Syntax_Ext.Brk i :: xsyms) = apfst (cons (Break i)) (xsyms_to_syms xsyms) @@ -202,13 +202,11 @@ then Pretty.marks_str (m @ [Lexicon.literal_markup s], s) else Pretty.str s; in (T :: Ts, args') end - | synT m (Block (i, bsymbs) :: symbs, args) = + | synT m (Block (info, bsymbs) :: symbs, args) = let val (bTs, args') = synT m (bsymbs, args); val (Ts, args'') = synT m (symbs, args'); - val T = - if i < 0 then Pretty.unbreakable (Pretty.block bTs) - else Pretty.blk (i, bTs); + val T = Pretty.markup_block info bTs |> #indent info < 0 ? Pretty.unbreakable; in (T :: Ts, args'') end | synT m (Break i :: symbs, args) = let @@ -217,8 +215,8 @@ in (T :: Ts, args') end and parT m (pr, args, p, p': int) = #1 (synT m - (if p > p' orelse (show_brackets andalso p' <> 1000 andalso not (is_chain pr)) - then [Block (1, String (false, "(") :: pr @ [String (false, ")")])] + (if p > p' orelse (show_brackets andalso p' <> 1000 andalso not (is_chain pr)) then + [Block (Syntax_Ext.block_indent 1, String (false, "(") :: pr @ [String (false, ")")])] else pr, args)) and atomT a = Pretty.marks_str (markup_extern a) diff -r 057e8dbe4326 -r 75ee05386b90 src/Pure/Syntax/syntax_ext.ML --- a/src/Pure/Syntax/syntax_ext.ML Thu Mar 31 16:23:25 2016 +0200 +++ b/src/Pure/Syntax/syntax_ext.ML Thu Mar 31 23:36:33 2016 +0200 @@ -8,11 +8,15 @@ sig datatype mfix = Mfix of Symbol_Pos.T list * typ * string * int list * int * Position.T val typ_to_nonterm: typ -> string + type block_info = {markup: Markup.T, consistent: bool, indent: int} + val block_indent: int -> block_info datatype xsymb = Delim of string | Argument of string * int | Space of string | - Bg of int | Brk of int | En + Bg of block_info | + Brk of int | + En datatype xprod = XProd of string * xsymb list * string * int val chain_pri: int val delims_of: xprod list -> string list list @@ -62,11 +66,16 @@ Space s: some white space for printing Bg, Brk, En: blocks and breaks for pretty printing*) +type block_info = {markup: Markup.T, consistent: bool, indent: int}; +fun block_indent indent = {markup = Markup.empty, consistent = false, indent = indent}; + datatype xsymb = Delim of string | Argument of string * int | Space of string | - Bg of int | Brk of int | En; + Bg of block_info | + Brk of int | + En; fun is_delim (Delim _) = true | is_delim _ = false; @@ -144,19 +153,57 @@ fun scan_many pred = Scan.many (pred o Symbol_Pos.symbol); fun scan_many1 pred = Scan.many1 (pred o Symbol_Pos.symbol); +(*block properties*) +local + val err_prefix = "Error in mixfix block properties: "; + val !!! = Symbol_Pos.!!! (fn () => err_prefix ^ "expected identifier or numeral or cartouche"); + + val scan_atom = + Symbol_Pos.scan_ident || + ($$$ "-" @@@ (Symbol_Pos.scan_float || Symbol_Pos.scan_nat)) || + Symbol_Pos.scan_float || Symbol_Pos.scan_nat || + Symbol_Pos.scan_cartouche_content err_prefix; + + val scan_blanks = scan_many Symbol.is_blank; + val scan_item = scan_blanks |-- scan_atom --| scan_blanks >> Symbol_Pos.content; + + val scan_prop = scan_item -- Scan.optional ($$ "=" |-- !!! scan_item) "true"; + val scan_end = Scan.ahead (Scan.one Symbol_Pos.is_eof) >> K "" || !!! Scan.fail; +in + fun read_block_properties ss = + let + fun err msg = error (msg ^ Position.here (#1 (Symbol_Pos.range ss))); + val props = the (Scan.read Symbol_Pos.stopper (Scan.repeat1 scan_prop --| scan_end) ss); + + val markup_name = Markup.get_markup props; + val markup_props = + fold Properties.remove [Markup.markupN, Markup.consistentN, Markup.indentN] props; + val _ = + if markup_name = "" andalso not (null markup_props) then + err ("Markup name required for block properties: " ^ commas_quote (map #1 markup_props)) + else (); + + val consistent = Markup.get_consistent props handle Fail msg => err msg; + val indent = Markup.get_indent props handle Fail msg => err msg; + in Bg {markup = (markup_name, markup_props), consistent = consistent, indent = indent} end; +end; + +val read_block_indent = + map Symbol_Pos.symbol #> (fn ss => + Bg (block_indent (if ss = ["0", "0"] then ~1 else #1 (Library.read_int ss)))); + val is_meta = member (op =) ["(", ")", "/", "_", "\"]; val scan_delim_char = $$ "'" |-- scan_one ((not o Symbol.is_blank) andf Symbol.not_eof) || scan_one ((not o is_meta) andf (not o Symbol.is_blank) andf Symbol.not_eof); -fun read_int ["0", "0"] = ~1 - | read_int cs = #1 (Library.read_int cs); - val scan_sym = $$ "_" >> K (Argument ("", 0)) || $$ "\" >> K index || - $$ "(" |-- scan_many Symbol.is_digit >> (Bg o read_int o map Symbol_Pos.symbol) || + $$ "(" |-- + (Symbol_Pos.scan_cartouche_content "Error in mixfix annotation: " >> read_block_properties || + scan_many Symbol.is_digit >> read_block_indent) || $$ ")" >> K En || $$ "/" -- $$ "/" >> K (Brk ~1) || $$ "/" |-- scan_many Symbol.is_blank >> (Brk o length) || diff -r 057e8dbe4326 -r 75ee05386b90 src/Pure/Syntax/syntax_phases.ML --- a/src/Pure/Syntax/syntax_phases.ML Thu Mar 31 16:23:25 2016 +0200 +++ b/src/Pure/Syntax/syntax_phases.ML Thu Mar 31 23:36:33 2016 +0200 @@ -750,7 +750,8 @@ let val ((bg1, bg2), en) = typing_elem; val bg = bg1 ^ Pretty.symbolic_output (pretty_typ_ast Markup.empty ty) ^ bg2; - in SOME (Pretty.make_block (bg, en) false 0 [pretty_ast Markup.empty t]) end + val info = {markup = (bg, en), consistent = false, indent = 0}; + in SOME (Pretty.make_block info [pretty_ast Markup.empty t]) end else NONE and ofsort_trans ty s = @@ -758,7 +759,8 @@ let val ((bg1, bg2), en) = sorting_elem; val bg = bg1 ^ Pretty.symbolic_output (pretty_typ_ast Markup.empty s) ^ bg2; - in SOME (Pretty.make_block (bg, en) false 0 [pretty_typ_ast Markup.empty ty]) end + val info = {markup = (bg, en), consistent = false, indent = 0}; + in SOME (Pretty.make_block info [pretty_typ_ast Markup.empty ty]) end else NONE and pretty_typ_ast m ast = ast