--- a/src/Pure/General/pretty.scala Mon Nov 28 20:39:08 2011 +0100
+++ b/src/Pure/General/pretty.scala Mon Nov 28 22:05:32 2011 +0100
@@ -19,11 +19,12 @@
object Block
{
def apply(i: Int, body: XML.Body): XML.Tree =
- XML.Elem(Markup(Markup.BLOCK, Markup.Indent(i)), body)
+ XML.Elem(Markup(Isabelle_Markup.BLOCK, Isabelle_Markup.Indent(i)), body)
def unapply(tree: XML.Tree): Option[(Int, XML.Body)] =
tree match {
- case XML.Elem(Markup(Markup.BLOCK, Markup.Indent(i)), body) => Some((i, body))
+ case XML.Elem(Markup(Isabelle_Markup.BLOCK, Isabelle_Markup.Indent(i)), body) =>
+ Some((i, body))
case _ => None
}
}
@@ -31,11 +32,12 @@
object Break
{
def apply(w: Int): XML.Tree =
- XML.Elem(Markup(Markup.BREAK, Markup.Width(w)), List(XML.Text(Symbol.spaces(w))))
+ XML.Elem(Markup(Isabelle_Markup.BREAK, Isabelle_Markup.Width(w)),
+ List(XML.Text(Symbol.spaces(w))))
def unapply(tree: XML.Tree): Option[Int] =
tree match {
- case XML.Elem(Markup(Markup.BREAK, Markup.Width(w)), _) => Some(w)
+ case XML.Elem(Markup(Isabelle_Markup.BREAK, Isabelle_Markup.Width(w)), _) => Some(w)
case _ => None
}
}