# HG changeset patch
# User wenzelm
# Date 1184078700 -7200
# Node ID af84f2f13d4dfc6ce7b80327e8322c5e994c6df0
# Parent  63e3b2e383ddf44e574cb87a648d579b1b223fd0
moved print_mode setup for markup to markup.ML;

diff -r 63e3b2e383dd -r af84f2f13d4d src/Pure/General/pretty.ML
--- a/src/Pure/General/pretty.ML	Tue Jul 10 16:45:00 2007 +0200
+++ b/src/Pure/General/pretty.ML	Tue Jul 10 16:45:00 2007 +0200
@@ -26,9 +26,7 @@
 signature PRETTY =
 sig
   val default_indent: string -> int -> output
-  val default_markup: Markup.T -> output * output
-  val mode_markup: Markup.T -> output * output
-  val add_mode: string -> (string -> int -> output) -> (Markup.T -> output * output) -> unit
+  val add_mode: string -> (string -> int -> output) -> unit
   type T
   val raw_str: output * int -> T
   val str: string -> T
@@ -87,28 +85,19 @@
 (** print mode operations **)
 
 fun default_indent (_: string) = Symbol.spaces;
-fun default_markup (_: Markup.T) = ("", "");
 
 local
-  val default = {indent = default_indent, markup = default_markup};
+  val default = {indent = default_indent};
   val modes = ref (Symtab.make [("", default)]);
 in
-  fun add_mode name indent markup =
-    change modes (Symtab.update_new (name, {indent = indent, markup = markup}));
+  fun add_mode name indent =
+    change modes (Symtab.update_new (name, {indent = indent}));
   fun get_mode () =
     the_default default (Library.get_first (Symtab.lookup (! modes)) (! print_mode));
 end;
 
 fun mode_indent x y = #indent (get_mode ()) x y;
 
-fun mode_markup m =
-  if m = Markup.none then ("", "")
-  else #markup (get_mode ()) m;
-
-fun add_markup m add =
-  let val (bg, en) = mode_markup m
-  in Buffer.add bg #> add #> Buffer.add en end;
-
 val output_spaces = Output.output o Symbol.spaces;
 val add_indent = Buffer.add o output_spaces;
 
@@ -281,7 +270,7 @@
             val block' =
               if pos' < emergencypos then (ind |> add_indent indent, pos')
               else (add_indent pos'' Buffer.empty, pos'');
-            val (bg, en) = mode_markup markup;
+            val (bg, en) = Markup.output markup;
             val btext: text = text
               |> control bg
               |> format (bes, block', breakdist (es, after))
@@ -310,6 +299,10 @@
 
 (* special output *)
 
+fun add_markup m add =
+  let val (bg, en) = Markup.output m
+  in Buffer.add bg #> add #> Buffer.add en end;
+
 (*symbolic markup -- no formatting*)
 fun symbolic prt =
   let