treat wrapped markup elements as raw markup delimiters;
authorwenzelm
Sat Sep 29 16:15:18 2012 +0200 (2012-09-29 ago)
changeset 496567ff712de5747
parent 49655 6642e559f165
child 49657 40e4feac2921
treat wrapped markup elements as raw markup delimiters;
src/Pure/General/pretty.ML
src/Pure/PIDE/yxml.ML
     1.1 --- a/src/Pure/General/pretty.ML	Sat Sep 29 13:43:23 2012 +0200
     1.2 +++ b/src/Pure/General/pretty.ML	Sat Sep 29 16:15:18 2012 +0200
     1.3 @@ -33,6 +33,7 @@
     1.4    val blk: int * T list -> T
     1.5    val block: T list -> T
     1.6    val strs: string list -> T
     1.7 +  val raw_markup: Output.output * Output.output -> int * T list -> T
     1.8    val markup: Markup.T -> T list -> T
     1.9    val mark: Markup.T -> T -> T
    1.10    val mark_str: Markup.T * string -> T
    1.11 @@ -61,9 +62,10 @@
    1.12    val output: int option -> T -> Output.output
    1.13    val string_of_margin: int -> T -> string
    1.14    val string_of: T -> string
    1.15 +  val writeln: T -> unit
    1.16 +  val symbolic_output: T -> Output.output
    1.17    val symbolic_string_of: T -> string
    1.18    val str_of: T -> string
    1.19 -  val writeln: T -> unit
    1.20    val to_ML: T -> ML_Pretty.pretty
    1.21    val from_ML: ML_Pretty.pretty -> T
    1.22  end;
    1.23 @@ -134,13 +136,13 @@
    1.24  fun breaks prts = Library.separate (brk 1) prts;
    1.25  fun fbreaks prts = Library.separate fbrk prts;
    1.26  
    1.27 -fun block_markup m (indent, es) =
    1.28 +fun raw_markup m (indent, es) =
    1.29    let
    1.30      fun sum [] k = k
    1.31        | sum (e :: es) k = sum es (length e + k);
    1.32    in Block (m, es, indent, sum es 0) end;
    1.33  
    1.34 -fun markup_block m arg = block_markup (Markup.output m) arg;
    1.35 +fun markup_block m arg = raw_markup (Markup.output m) arg;
    1.36  
    1.37  val blk = markup_block Markup.empty;
    1.38  fun block prts = blk (2, prts);
    1.39 @@ -325,9 +327,12 @@
    1.40  val output = Buffer.content oo output_buffer;
    1.41  fun string_of_margin margin = Output.escape o output (SOME margin);
    1.42  val string_of = Output.escape o output NONE;
    1.43 -val symbolic_string_of = Output.escape o Buffer.content o symbolic;
    1.44 +val writeln = Output.writeln o string_of;
    1.45 +
    1.46 +val symbolic_output = Buffer.content o symbolic;
    1.47 +val symbolic_string_of = Output.escape o symbolic_output;
    1.48 +
    1.49  val str_of = Output.escape o Buffer.content o unformatted;
    1.50 -val writeln = Output.writeln o string_of;
    1.51  
    1.52  
    1.53  
    1.54 @@ -337,7 +342,7 @@
    1.55    | to_ML (String s) = ML_Pretty.String s
    1.56    | to_ML (Break b) = ML_Pretty.Break b;
    1.57  
    1.58 -fun from_ML (ML_Pretty.Block (m, prts, ind)) = block_markup m (ind, map from_ML prts)
    1.59 +fun from_ML (ML_Pretty.Block (m, prts, ind)) = raw_markup m (ind, map from_ML prts)
    1.60    | from_ML (ML_Pretty.String s) = String s
    1.61    | from_ML (ML_Pretty.Break b) = Break b;
    1.62  
     2.1 --- a/src/Pure/PIDE/yxml.ML	Sat Sep 29 13:43:23 2012 +0200
     2.2 +++ b/src/Pure/PIDE/yxml.ML	Sat Sep 29 16:15:18 2012 +0200
     2.3 @@ -23,6 +23,7 @@
     2.4    val output_markup: Markup.T -> string * string
     2.5    val string_of_body: XML.body -> string
     2.6    val string_of: XML.tree -> string
     2.7 +  val output_markup_elem: Markup.T -> (string * string) * string
     2.8    val parse_body: string -> XML.body
     2.9    val parse: string -> XML.tree
    2.10  end;
    2.11 @@ -75,6 +76,16 @@
    2.12  val string_of = string_of_body o single;
    2.13  
    2.14  
    2.15 +(* wrapped elements *)
    2.16 +
    2.17 +val Z = chr 0;
    2.18 +val Z_text = [XML.Text Z];
    2.19 +
    2.20 +fun output_markup_elem markup =
    2.21 +  let val [bg1, bg2, en] = space_explode Z (string_of (XML.wrap_elem ((markup, Z_text), Z_text)))
    2.22 +  in ((bg1, bg2), en) end;
    2.23 +
    2.24 +
    2.25  
    2.26  (** efficient YXML parsing **)
    2.27