organized markup properties via apply/unapply patterns;
authorwenzelm
Wed Aug 25 22:37:53 2010 +0200 (2010-08-25)
changeset 38722ba31936497c2
parent 38721 ca8b14fa0d0d
child 38723 6a55b8978a56
organized markup properties via apply/unapply patterns;
src/Pure/General/markup.scala
src/Pure/General/position.scala
src/Pure/PIDE/command.scala
src/Pure/System/session.scala
src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala
     1.1 --- a/src/Pure/General/markup.scala	Wed Aug 25 21:31:22 2010 +0200
     1.2 +++ b/src/Pure/General/markup.scala	Wed Aug 25 22:37:53 2010 +0200
     1.3 @@ -9,7 +9,7 @@
     1.4  
     1.5  object Markup
     1.6  {
     1.7 -  /* integers */
     1.8 +  /* plain values */
     1.9  
    1.10    object Int {
    1.11      def apply(i: scala.Int): String = i.toString
    1.12 @@ -26,25 +26,33 @@
    1.13    }
    1.14  
    1.15  
    1.16 -  /* property values */
    1.17 -
    1.18 -  def get_string(name: String, props: List[(String, String)]): Option[String] =
    1.19 -    props.find(p => p._1 == name).map(_._2)
    1.20 +  /* named properties */
    1.21  
    1.22 -  def get_long(name: String, props: List[(String, String)]): Option[scala.Long] =
    1.23 +  class Property(val name: String)
    1.24    {
    1.25 -    get_string(name, props) match {
    1.26 -      case None => None
    1.27 -      case Some(Long(i)) => Some(i)
    1.28 -    }
    1.29 +    def apply(value: String): List[(String, String)] = List((name, value))
    1.30 +    def unapply(props: List[(String, String)]): Option[String] =
    1.31 +      props.find(_._1 == name).map(_._2)
    1.32    }
    1.33  
    1.34 -  def get_int(name: String, props: List[(String, String)]): Option[scala.Int] =
    1.35 +  class Int_Property(name: String)
    1.36    {
    1.37 -    get_string(name, props) match {
    1.38 -      case None => None
    1.39 -      case Some(Int(i)) => Some(i)
    1.40 -    }
    1.41 +    def apply(value: scala.Int): List[(String, String)] = List((name, Int(value)))
    1.42 +    def unapply(props: List[(String, String)]): Option[Int] =
    1.43 +      props.find(_._1 == name) match {
    1.44 +        case None => None
    1.45 +        case Some((_, value)) => Int.unapply(value)
    1.46 +      }
    1.47 +  }
    1.48 +
    1.49 +  class Long_Property(name: String)
    1.50 +  {
    1.51 +    def apply(value: scala.Long): List[(String, String)] = List((name, Long(value)))
    1.52 +    def unapply(props: List[(String, String)]): Option[Long] =
    1.53 +      props.find(_._1 == name) match {
    1.54 +        case None => None
    1.55 +        case Some((_, value)) => Long.unapply(value)
    1.56 +      }
    1.57    }
    1.58  
    1.59  
     2.1 --- a/src/Pure/General/position.scala	Wed Aug 25 21:31:22 2010 +0200
     2.2 +++ b/src/Pure/General/position.scala	Wed Aug 25 22:37:53 2010 +0200
     2.3 @@ -11,22 +11,21 @@
     2.4  {
     2.5    type T = List[(String, String)]
     2.6  
     2.7 -  def get_line(pos: T): Option[Int] = Markup.get_int(Markup.LINE, pos)
     2.8 -  def get_column(pos: T): Option[Int] = Markup.get_int(Markup.COLUMN, pos)
     2.9 -  def get_offset(pos: T): Option[Int] = Markup.get_int(Markup.OFFSET, pos)
    2.10 -  def get_end_line(pos: T): Option[Int] = Markup.get_int(Markup.END_LINE, pos)
    2.11 -  def get_end_column(pos: T): Option[Int] = Markup.get_int(Markup.END_COLUMN, pos)
    2.12 -  def get_end_offset(pos: T): Option[Int] = Markup.get_int(Markup.END_OFFSET, pos)
    2.13 -  def get_file(pos: T): Option[String] = Markup.get_string(Markup.FILE, pos)
    2.14 -  def get_id(pos: T): Option[Long] = Markup.get_long(Markup.ID, pos)
    2.15 +  val Line = new Markup.Int_Property(Markup.LINE)
    2.16 +  val End_Line = new Markup.Int_Property(Markup.END_LINE)
    2.17 +  val Offset = new Markup.Int_Property(Markup.OFFSET)
    2.18 +  val End_Offset = new Markup.Int_Property(Markup.END_OFFSET)
    2.19 +  val File = new Markup.Property(Markup.FILE)
    2.20 +  val Id = new Markup.Long_Property(Markup.ID)
    2.21  
    2.22 -  def get_range(pos: T): Option[Text.Range] =
    2.23 -    (get_offset(pos), get_end_offset(pos)) match {
    2.24 -      case (Some(start), Some(stop)) if start <= stop => Some(Text.Range(start, stop))
    2.25 -      case (Some(start), None) => Some(Text.Range(start))
    2.26 -      case (_, _) => None
    2.27 -    }
    2.28 -
    2.29 -  object Id { def unapply(pos: T): Option[Long] = get_id(pos) }
    2.30 -  object Range { def unapply(pos: T): Option[Text.Range] = get_range(pos) }
    2.31 +  object Range
    2.32 +  {
    2.33 +    def apply(range: Text.Range): T = Offset(range.start) ++ Offset(range.stop)
    2.34 +    def unapply(pos: T): Option[Text.Range] =
    2.35 +      (Offset.unapply(pos), End_Offset.unapply(pos)) match {
    2.36 +        case (Some(start), Some(stop)) if start <= stop => Some(Text.Range(start, stop))
    2.37 +        case (Some(start), None) => Some(Text.Range(start))
    2.38 +        case _ => None
    2.39 +      }
    2.40 +  }
    2.41  }
     3.1 --- a/src/Pure/PIDE/command.scala	Wed Aug 25 21:31:22 2010 +0200
     3.2 +++ b/src/Pure/PIDE/command.scala	Wed Aug 25 22:37:53 2010 +0200
     3.3 @@ -46,12 +46,15 @@
     3.4          case XML.Elem(Markup(Markup.REPORT, _), msgs) =>
     3.5            (this /: msgs)((state, msg) =>
     3.6              msg match {
     3.7 -              case XML.Elem(Markup(name, atts), args)
     3.8 -              if Position.get_id(atts) == Some(command.id) && Position.get_range(atts).isDefined =>
     3.9 -                val range = command.decode(Position.get_range(atts).get)
    3.10 -                val props = atts.filterNot(p => Markup.POSITION_PROPERTIES(p._1))
    3.11 -                val info = Text.Info[Any](range, XML.Elem(Markup(name, props), args))
    3.12 -                state.add_markup(info)
    3.13 +              case XML.Elem(Markup(name, atts), args) =>
    3.14 +                atts match {
    3.15 +                  case Position.Range(range) if Position.Id.unapply(atts) == Some(command.id) =>
    3.16 +                    val props = atts.filterNot(p => Markup.POSITION_PROPERTIES(p._1))
    3.17 +                    val info =
    3.18 +                      Text.Info[Any](command.decode(range), XML.Elem(Markup(name, props), args))
    3.19 +                    state.add_markup(info)
    3.20 +                  case _ => System.err.println("Ignored report message: " + msg); state
    3.21 +                }
    3.22                case _ => System.err.println("Ignored report message: " + msg); state
    3.23              })
    3.24          case _ => add_result(message)
     4.1 --- a/src/Pure/System/session.scala	Wed Aug 25 21:31:22 2010 +0200
     4.2 +++ b/src/Pure/System/session.scala	Wed Aug 25 22:37:53 2010 +0200
     4.3 @@ -131,15 +131,15 @@
     4.4      {
     4.5        raw_protocol.event(result)
     4.6  
     4.7 -      Position.get_id(result.properties) match {
     4.8 -        case Some(state_id) =>
     4.9 +      result.properties match {
    4.10 +        case Position.Id(state_id) =>
    4.11            try {
    4.12              val (st, state) = global_state.accumulate(state_id, result.message)
    4.13              global_state = state
    4.14              indicate_command_change(st.command)
    4.15            }
    4.16            catch { case _: Document.State.Fail => bad_result(result) }
    4.17 -        case None =>
    4.18 +        case _ =>
    4.19            if (result.is_status) {
    4.20              result.body match {
    4.21                case List(Isar_Document.Assign(id, edits)) =>
     5.1 --- a/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala	Wed Aug 25 21:31:22 2010 +0200
     5.2 +++ b/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala	Wed Aug 25 22:37:53 2010 +0200
     5.3 @@ -55,11 +55,11 @@
     5.4                  val Text.Range(begin, end) = snapshot.convert(info_range + command_start)
     5.5                  val line = buffer.getLineOfOffset(begin)
     5.6  
     5.7 -                (Position.get_file(props), Position.get_line(props)) match {
     5.8 +                (Position.File.unapply(props), Position.Line.unapply(props)) match {
     5.9                    case (Some(ref_file), Some(ref_line)) =>
    5.10                      new External_Hyperlink(begin, end, line, ref_file, ref_line)
    5.11                    case _ =>
    5.12 -                    (Position.get_id(props), Position.get_offset(props)) match {
    5.13 +                    (Position.Id.unapply(props), Position.Offset.unapply(props)) match {
    5.14                        case (Some(ref_id), Some(ref_offset)) =>
    5.15                          snapshot.lookup_command(ref_id) match {
    5.16                            case Some(ref_cmd) =>