moved print_mode setup for markup to markup.ML;
authorwenzelm
Tue Jul 10 16:45:00 2007 +0200 (2007-07-10)
changeset 23698af84f2f13d4d
parent 23697 63e3b2e383dd
child 23699 5a4527f3ac79
moved print_mode setup for markup to markup.ML;
src/Pure/General/pretty.ML
     1.1 --- a/src/Pure/General/pretty.ML	Tue Jul 10 16:45:00 2007 +0200
     1.2 +++ b/src/Pure/General/pretty.ML	Tue Jul 10 16:45:00 2007 +0200
     1.3 @@ -26,9 +26,7 @@
     1.4  signature PRETTY =
     1.5  sig
     1.6    val default_indent: string -> int -> output
     1.7 -  val default_markup: Markup.T -> output * output
     1.8 -  val mode_markup: Markup.T -> output * output
     1.9 -  val add_mode: string -> (string -> int -> output) -> (Markup.T -> output * output) -> unit
    1.10 +  val add_mode: string -> (string -> int -> output) -> unit
    1.11    type T
    1.12    val raw_str: output * int -> T
    1.13    val str: string -> T
    1.14 @@ -87,28 +85,19 @@
    1.15  (** print mode operations **)
    1.16  
    1.17  fun default_indent (_: string) = Symbol.spaces;
    1.18 -fun default_markup (_: Markup.T) = ("", "");
    1.19  
    1.20  local
    1.21 -  val default = {indent = default_indent, markup = default_markup};
    1.22 +  val default = {indent = default_indent};
    1.23    val modes = ref (Symtab.make [("", default)]);
    1.24  in
    1.25 -  fun add_mode name indent markup =
    1.26 -    change modes (Symtab.update_new (name, {indent = indent, markup = markup}));
    1.27 +  fun add_mode name indent =
    1.28 +    change modes (Symtab.update_new (name, {indent = indent}));
    1.29    fun get_mode () =
    1.30      the_default default (Library.get_first (Symtab.lookup (! modes)) (! print_mode));
    1.31  end;
    1.32  
    1.33  fun mode_indent x y = #indent (get_mode ()) x y;
    1.34  
    1.35 -fun mode_markup m =
    1.36 -  if m = Markup.none then ("", "")
    1.37 -  else #markup (get_mode ()) m;
    1.38 -
    1.39 -fun add_markup m add =
    1.40 -  let val (bg, en) = mode_markup m
    1.41 -  in Buffer.add bg #> add #> Buffer.add en end;
    1.42 -
    1.43  val output_spaces = Output.output o Symbol.spaces;
    1.44  val add_indent = Buffer.add o output_spaces;
    1.45  
    1.46 @@ -281,7 +270,7 @@
    1.47              val block' =
    1.48                if pos' < emergencypos then (ind |> add_indent indent, pos')
    1.49                else (add_indent pos'' Buffer.empty, pos'');
    1.50 -            val (bg, en) = mode_markup markup;
    1.51 +            val (bg, en) = Markup.output markup;
    1.52              val btext: text = text
    1.53                |> control bg
    1.54                |> format (bes, block', breakdist (es, after))
    1.55 @@ -310,6 +299,10 @@
    1.56  
    1.57  (* special output *)
    1.58  
    1.59 +fun add_markup m add =
    1.60 +  let val (bg, en) = Markup.output m
    1.61 +  in Buffer.add bg #> add #> Buffer.add en end;
    1.62 +
    1.63  (*symbolic markup -- no formatting*)
    1.64  fun symbolic prt =
    1.65    let