1.1 --- a/src/Pure/General/pretty.ML	Mon Nov 28 20:39:08 2011 +0100
     1.2 +++ b/src/Pure/General/pretty.ML	Mon Nov 28 22:05:32 2011 +0100
     1.3 @@ -133,8 +133,8 @@
     1.4  fun mark_str (m, s) = mark m (str s);
     1.5  fun marks_str (ms, s) = fold_rev mark ms (str s);
     1.6  
     1.7 -fun keyword name = mark_str (Markup.keyword, name);
     1.8 -fun command name = mark_str (Markup.command, name);
     1.9 +fun keyword name = mark_str (Isabelle_Markup.keyword, name);
    1.10 +fun command name = mark_str (Isabelle_Markup.command, name);
    1.11  
    1.12  fun markup_chunks m prts = markup m (fbreaks prts);
    1.13  val chunks = markup_chunks Markup.empty;
    1.14 @@ -276,9 +276,12 @@
    1.15    let
    1.16      fun out (Block ((bg, en), [], _, _)) = Buffer.add bg #> Buffer.add en
    1.17        | out (Block ((bg, en), prts, indent, _)) =
    1.18 -          Buffer.add bg #> Buffer.markup (Markup.block indent) (fold out prts) #> Buffer.add en
    1.19 +          Buffer.add bg #>
    1.20 +          Buffer.markup (Isabelle_Markup.block indent) (fold out prts) #>
    1.21 +          Buffer.add en
    1.22        | out (String (s, _)) = Buffer.add s
    1.23 -      | out (Break (false, wd)) = Buffer.markup (Markup.break wd) (Buffer.add (output_spaces wd))
    1.24 +      | out (Break (false, wd)) =
    1.25 +          Buffer.markup (Isabelle_Markup.break wd) (Buffer.add (output_spaces wd))
    1.26        | out (Break (true, _)) = Buffer.add (Output.output "\n");
    1.27    in out prt Buffer.empty end;
    1.28