--- 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);
--- 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";
--- 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)
--- 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 =) ["(", ")", "/", "_", "\<index>"];
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)) ||
$$ "\<index>" >> 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) ||
--- 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