src/Pure/PIDE/markup.scala
changeset 55553 4a5f65df29fa
parent 55552 bcc643ac071a
child 55555 99409ccbe04a
     1.1 --- a/src/Pure/PIDE/markup.scala	Tue Feb 18 16:34:02 2014 +0100
     1.2 +++ b/src/Pure/PIDE/markup.scala	Tue Feb 18 17:03:12 2014 +0100
     1.3 @@ -27,6 +27,24 @@
     1.4    val Empty = Markup("", Nil)
     1.5    val Broken = Markup("broken", Nil)
     1.6  
     1.7 +  class Markup_String(val name: String, prop: String)
     1.8 +  {
     1.9 +    private val Prop = new Properties.String(prop)
    1.10 +
    1.11 +    def apply(s: String): Markup = Markup(name, Prop(s))
    1.12 +    def unapply(markup: Markup): Option[String] =
    1.13 +      if (markup.name == name) Prop.unapply(markup.properties) else None
    1.14 +  }
    1.15 +
    1.16 +  class Markup_Int(val name: String, prop: String)
    1.17 +  {
    1.18 +    private val Prop = new Properties.Int(prop)
    1.19 +
    1.20 +    def apply(i: Int): Markup = Markup(name, Prop(i))
    1.21 +    def unapply(markup: Markup): Option[Int] =
    1.22 +      if (markup.name == name) Prop.unapply(markup.properties) else None
    1.23 +  }
    1.24 +
    1.25  
    1.26    /* formal entities */
    1.27  
    1.28 @@ -39,9 +57,9 @@
    1.29    {
    1.30      def unapply(markup: Markup): Option[(String, String)] =
    1.31        markup match {
    1.32 -        case Markup(ENTITY, props @ Kind(kind)) =>
    1.33 -          props match {
    1.34 -            case Name(name) => Some(kind, name)
    1.35 +        case Markup(ENTITY, props) =>
    1.36 +          (props, props) match {
    1.37 +            case (Kind(kind), Name(name)) => Some(kind, name)
    1.38              case _ => None
    1.39            }
    1.40          case _ => None
    1.41 @@ -70,49 +88,22 @@
    1.42    /* embedded languages */
    1.43  
    1.44    val LANGUAGE = "language"
    1.45 -
    1.46 -  object Language
    1.47 -  {
    1.48 -    def unapply(markup: Markup): Option[String] =
    1.49 -      markup match {
    1.50 -        case Markup(LANGUAGE, Name(name)) => Some(name)
    1.51 -        case _ => None
    1.52 -      }
    1.53 -  }
    1.54 +  val Language = new Markup_String(LANGUAGE, NAME)
    1.55  
    1.56  
    1.57    /* external resources */
    1.58  
    1.59    val PATH = "path"
    1.60 -
    1.61 -  object Path
    1.62 -  {
    1.63 -    def unapply(markup: Markup): Option[String] =
    1.64 -      markup match {
    1.65 -        case Markup(PATH, Name(name)) => Some(name)
    1.66 -        case _ => None
    1.67 -      }
    1.68 -  }
    1.69 +  val Path = new Markup_String(PATH, NAME)
    1.70  
    1.71    val URL = "url"
    1.72 -
    1.73 -  object Url
    1.74 -  {
    1.75 -    def unapply(markup: Markup): Option[String] =
    1.76 -      markup match {
    1.77 -        case Markup(URL, Name(name)) => Some(name)
    1.78 -        case _ => None
    1.79 -      }
    1.80 -  }
    1.81 +  val Url = new Markup_String(URL, NAME)
    1.82  
    1.83  
    1.84    /* pretty printing */
    1.85  
    1.86 -  val Indent = new Properties.Int("indent")
    1.87 -  val BLOCK = "block"
    1.88 -
    1.89 -  val Width = new Properties.Int("width")
    1.90 -  val BREAK = "break"
    1.91 +  val Block = new Markup_Int("block", "indent")
    1.92 +  val Break = new Markup_Int("break", "width")
    1.93  
    1.94    val ITEM = "item"
    1.95    val BULLET = "bullet"