tuned signature;
authorwenzelm
Tue Feb 18 17:03:12 2014 +0100 (2014-02-18 ago)
changeset 555534a5f65df29fa
parent 55552 bcc643ac071a
child 55554 e4907b74a347
tuned signature;
src/Pure/General/pretty.scala
src/Pure/PIDE/markup.ML
src/Pure/PIDE/markup.scala
src/Pure/PIDE/yxml.scala
     1.1 --- a/src/Pure/General/pretty.scala	Tue Feb 18 16:34:02 2014 +0100
     1.2 +++ b/src/Pure/General/pretty.scala	Tue Feb 18 17:03:12 2014 +0100
     1.3 @@ -45,12 +45,11 @@
     1.4    object Block
     1.5    {
     1.6      def apply(i: Int, body: XML.Body): XML.Tree =
     1.7 -      XML.Elem(Markup(Markup.BLOCK, Markup.Indent(i)), body)
     1.8 +      XML.Elem(Markup.Block(i), body)
     1.9  
    1.10      def unapply(tree: XML.Tree): Option[(Int, XML.Body)] =
    1.11        tree match {
    1.12 -        case XML.Elem(Markup(Markup.BLOCK, Markup.Indent(i)), body) =>
    1.13 -          Some((i, body))
    1.14 +        case XML.Elem(Markup.Block(i), body) => Some((i, body))
    1.15          case _ => None
    1.16        }
    1.17    }
    1.18 @@ -58,12 +57,11 @@
    1.19    object Break
    1.20    {
    1.21      def apply(w: Int): XML.Tree =
    1.22 -      XML.Elem(Markup(Markup.BREAK, Markup.Width(w)),
    1.23 -        List(XML.Text(spaces(w))))
    1.24 +      XML.Elem(Markup.Break(w), List(XML.Text(spaces(w))))
    1.25  
    1.26      def unapply(tree: XML.Tree): Option[Int] =
    1.27        tree match {
    1.28 -        case XML.Elem(Markup(Markup.BREAK, Markup.Width(w)), _) => Some(w)
    1.29 +        case XML.Elem(Markup.Break(w), _) => Some(w)
    1.30          case _ => None
    1.31        }
    1.32    }
     2.1 --- a/src/Pure/PIDE/markup.ML	Tue Feb 18 16:34:02 2014 +0100
     2.2 +++ b/src/Pure/PIDE/markup.ML	Tue Feb 18 17:03:12 2014 +0100
     2.3 @@ -221,9 +221,9 @@
     2.4  fun properties more_props ((elem, props): T) =
     2.5    (elem, fold_rev Properties.put more_props props);
     2.6  
     2.7 -fun markup_elem elem = (elem, (elem, []): T);
     2.8 -fun markup_string elem prop = (elem, fn s => (elem, [(prop, s)]): T);
     2.9 -fun markup_int elem prop = (elem, fn i => (elem, [(prop, print_int i)]): T);
    2.10 +fun markup_elem name = (name, (name, []): T);
    2.11 +fun markup_string name prop = (name, fn s => (name, [(prop, s)]): T);
    2.12 +fun markup_int name prop = (name, fn i => (name, [(prop, print_int i)]): T);
    2.13  
    2.14  
    2.15  (* misc properties *)
     3.1 --- a/src/Pure/PIDE/markup.scala	Tue Feb 18 16:34:02 2014 +0100
     3.2 +++ b/src/Pure/PIDE/markup.scala	Tue Feb 18 17:03:12 2014 +0100
     3.3 @@ -27,6 +27,24 @@
     3.4    val Empty = Markup("", Nil)
     3.5    val Broken = Markup("broken", Nil)
     3.6  
     3.7 +  class Markup_String(val name: String, prop: String)
     3.8 +  {
     3.9 +    private val Prop = new Properties.String(prop)
    3.10 +
    3.11 +    def apply(s: String): Markup = Markup(name, Prop(s))
    3.12 +    def unapply(markup: Markup): Option[String] =
    3.13 +      if (markup.name == name) Prop.unapply(markup.properties) else None
    3.14 +  }
    3.15 +
    3.16 +  class Markup_Int(val name: String, prop: String)
    3.17 +  {
    3.18 +    private val Prop = new Properties.Int(prop)
    3.19 +
    3.20 +    def apply(i: Int): Markup = Markup(name, Prop(i))
    3.21 +    def unapply(markup: Markup): Option[Int] =
    3.22 +      if (markup.name == name) Prop.unapply(markup.properties) else None
    3.23 +  }
    3.24 +
    3.25  
    3.26    /* formal entities */
    3.27  
    3.28 @@ -39,9 +57,9 @@
    3.29    {
    3.30      def unapply(markup: Markup): Option[(String, String)] =
    3.31        markup match {
    3.32 -        case Markup(ENTITY, props @ Kind(kind)) =>
    3.33 -          props match {
    3.34 -            case Name(name) => Some(kind, name)
    3.35 +        case Markup(ENTITY, props) =>
    3.36 +          (props, props) match {
    3.37 +            case (Kind(kind), Name(name)) => Some(kind, name)
    3.38              case _ => None
    3.39            }
    3.40          case _ => None
    3.41 @@ -70,49 +88,22 @@
    3.42    /* embedded languages */
    3.43  
    3.44    val LANGUAGE = "language"
    3.45 -
    3.46 -  object Language
    3.47 -  {
    3.48 -    def unapply(markup: Markup): Option[String] =
    3.49 -      markup match {
    3.50 -        case Markup(LANGUAGE, Name(name)) => Some(name)
    3.51 -        case _ => None
    3.52 -      }
    3.53 -  }
    3.54 +  val Language = new Markup_String(LANGUAGE, NAME)
    3.55  
    3.56  
    3.57    /* external resources */
    3.58  
    3.59    val PATH = "path"
    3.60 -
    3.61 -  object Path
    3.62 -  {
    3.63 -    def unapply(markup: Markup): Option[String] =
    3.64 -      markup match {
    3.65 -        case Markup(PATH, Name(name)) => Some(name)
    3.66 -        case _ => None
    3.67 -      }
    3.68 -  }
    3.69 +  val Path = new Markup_String(PATH, NAME)
    3.70  
    3.71    val URL = "url"
    3.72 -
    3.73 -  object Url
    3.74 -  {
    3.75 -    def unapply(markup: Markup): Option[String] =
    3.76 -      markup match {
    3.77 -        case Markup(URL, Name(name)) => Some(name)
    3.78 -        case _ => None
    3.79 -      }
    3.80 -  }
    3.81 +  val Url = new Markup_String(URL, NAME)
    3.82  
    3.83  
    3.84    /* pretty printing */
    3.85  
    3.86 -  val Indent = new Properties.Int("indent")
    3.87 -  val BLOCK = "block"
    3.88 -
    3.89 -  val Width = new Properties.Int("width")
    3.90 -  val BREAK = "break"
    3.91 +  val Block = new Markup_Int("block", "indent")
    3.92 +  val Break = new Markup_Int("break", "width")
    3.93  
    3.94    val ITEM = "item"
    3.95    val BULLET = "bullet"
     4.1 --- a/src/Pure/PIDE/yxml.scala	Tue Feb 18 16:34:02 2014 +0100
     4.2 +++ b/src/Pure/PIDE/yxml.scala	Tue Feb 18 17:03:12 2014 +0100
     4.3 @@ -120,7 +120,7 @@
     4.4    /* failsafe parsing */
     4.5  
     4.6    private def markup_broken(source: CharSequence) =
     4.7 -    XML.elem(Markup.Broken.name, List(XML.Text(source.toString)))
     4.8 +    XML.Elem(Markup.Broken, List(XML.Text(source.toString)))
     4.9  
    4.10    def parse_body_failsafe(source: CharSequence): XML.Body =
    4.11    {