# HG changeset patch # User wenzelm # Date 1282768673 -7200 # Node ID ba31936497c2b32313ddddcd3c8d030a298e0af3 # Parent ca8b14fa0d0d22a7f5ee37b6c64b45230f4638a7 organized markup properties via apply/unapply patterns; diff -r ca8b14fa0d0d -r ba31936497c2 src/Pure/General/markup.scala --- a/src/Pure/General/markup.scala Wed Aug 25 21:31:22 2010 +0200 +++ b/src/Pure/General/markup.scala Wed Aug 25 22:37:53 2010 +0200 @@ -9,7 +9,7 @@ object Markup { - /* integers */ + /* plain values */ object Int { def apply(i: scala.Int): String = i.toString @@ -26,25 +26,33 @@ } - /* property values */ - - def get_string(name: String, props: List[(String, String)]): Option[String] = - props.find(p => p._1 == name).map(_._2) + /* named properties */ - def get_long(name: String, props: List[(String, String)]): Option[scala.Long] = + class Property(val name: String) { - get_string(name, props) match { - case None => None - case Some(Long(i)) => Some(i) - } + def apply(value: String): List[(String, String)] = List((name, value)) + def unapply(props: List[(String, String)]): Option[String] = + props.find(_._1 == name).map(_._2) } - def get_int(name: String, props: List[(String, String)]): Option[scala.Int] = + class Int_Property(name: String) { - get_string(name, props) match { - case None => None - case Some(Int(i)) => Some(i) - } + def apply(value: scala.Int): List[(String, String)] = List((name, Int(value))) + def unapply(props: List[(String, String)]): Option[Int] = + props.find(_._1 == name) match { + case None => None + case Some((_, value)) => Int.unapply(value) + } + } + + class Long_Property(name: String) + { + def apply(value: scala.Long): List[(String, String)] = List((name, Long(value))) + def unapply(props: List[(String, String)]): Option[Long] = + props.find(_._1 == name) match { + case None => None + case Some((_, value)) => Long.unapply(value) + } } diff -r ca8b14fa0d0d -r ba31936497c2 src/Pure/General/position.scala --- a/src/Pure/General/position.scala Wed Aug 25 21:31:22 2010 +0200 +++ b/src/Pure/General/position.scala Wed Aug 25 22:37:53 2010 +0200 @@ -11,22 +11,21 @@ { type T = List[(String, String)] - def get_line(pos: T): Option[Int] = Markup.get_int(Markup.LINE, pos) - def get_column(pos: T): Option[Int] = Markup.get_int(Markup.COLUMN, pos) - def get_offset(pos: T): Option[Int] = Markup.get_int(Markup.OFFSET, pos) - def get_end_line(pos: T): Option[Int] = Markup.get_int(Markup.END_LINE, pos) - def get_end_column(pos: T): Option[Int] = Markup.get_int(Markup.END_COLUMN, pos) - def get_end_offset(pos: T): Option[Int] = Markup.get_int(Markup.END_OFFSET, pos) - def get_file(pos: T): Option[String] = Markup.get_string(Markup.FILE, pos) - def get_id(pos: T): Option[Long] = Markup.get_long(Markup.ID, pos) + val Line = new Markup.Int_Property(Markup.LINE) + val End_Line = new Markup.Int_Property(Markup.END_LINE) + val Offset = new Markup.Int_Property(Markup.OFFSET) + val End_Offset = new Markup.Int_Property(Markup.END_OFFSET) + val File = new Markup.Property(Markup.FILE) + val Id = new Markup.Long_Property(Markup.ID) - def get_range(pos: T): Option[Text.Range] = - (get_offset(pos), get_end_offset(pos)) match { - case (Some(start), Some(stop)) if start <= stop => Some(Text.Range(start, stop)) - case (Some(start), None) => Some(Text.Range(start)) - case (_, _) => None - } - - object Id { def unapply(pos: T): Option[Long] = get_id(pos) } - object Range { def unapply(pos: T): Option[Text.Range] = get_range(pos) } + object Range + { + def apply(range: Text.Range): T = Offset(range.start) ++ Offset(range.stop) + def unapply(pos: T): Option[Text.Range] = + (Offset.unapply(pos), End_Offset.unapply(pos)) match { + case (Some(start), Some(stop)) if start <= stop => Some(Text.Range(start, stop)) + case (Some(start), None) => Some(Text.Range(start)) + case _ => None + } + } } diff -r ca8b14fa0d0d -r ba31936497c2 src/Pure/PIDE/command.scala --- a/src/Pure/PIDE/command.scala Wed Aug 25 21:31:22 2010 +0200 +++ b/src/Pure/PIDE/command.scala Wed Aug 25 22:37:53 2010 +0200 @@ -46,12 +46,15 @@ case XML.Elem(Markup(Markup.REPORT, _), msgs) => (this /: msgs)((state, msg) => msg match { - case XML.Elem(Markup(name, atts), args) - if Position.get_id(atts) == Some(command.id) && Position.get_range(atts).isDefined => - val range = command.decode(Position.get_range(atts).get) - val props = atts.filterNot(p => Markup.POSITION_PROPERTIES(p._1)) - val info = Text.Info[Any](range, XML.Elem(Markup(name, props), args)) - state.add_markup(info) + case XML.Elem(Markup(name, atts), args) => + atts match { + case Position.Range(range) if Position.Id.unapply(atts) == Some(command.id) => + val props = atts.filterNot(p => Markup.POSITION_PROPERTIES(p._1)) + val info = + Text.Info[Any](command.decode(range), XML.Elem(Markup(name, props), args)) + state.add_markup(info) + case _ => System.err.println("Ignored report message: " + msg); state + } case _ => System.err.println("Ignored report message: " + msg); state }) case _ => add_result(message) diff -r ca8b14fa0d0d -r ba31936497c2 src/Pure/System/session.scala --- a/src/Pure/System/session.scala Wed Aug 25 21:31:22 2010 +0200 +++ b/src/Pure/System/session.scala Wed Aug 25 22:37:53 2010 +0200 @@ -131,15 +131,15 @@ { raw_protocol.event(result) - Position.get_id(result.properties) match { - case Some(state_id) => + result.properties match { + case Position.Id(state_id) => try { val (st, state) = global_state.accumulate(state_id, result.message) global_state = state indicate_command_change(st.command) } catch { case _: Document.State.Fail => bad_result(result) } - case None => + case _ => if (result.is_status) { result.body match { case List(Isar_Document.Assign(id, edits)) => diff -r ca8b14fa0d0d -r ba31936497c2 src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala --- a/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala Wed Aug 25 21:31:22 2010 +0200 +++ b/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala Wed Aug 25 22:37:53 2010 +0200 @@ -55,11 +55,11 @@ val Text.Range(begin, end) = snapshot.convert(info_range + command_start) val line = buffer.getLineOfOffset(begin) - (Position.get_file(props), Position.get_line(props)) match { + (Position.File.unapply(props), Position.Line.unapply(props)) match { case (Some(ref_file), Some(ref_line)) => new External_Hyperlink(begin, end, line, ref_file, ref_line) case _ => - (Position.get_id(props), Position.get_offset(props)) match { + (Position.Id.unapply(props), Position.Offset.unapply(props)) match { case (Some(ref_id), Some(ref_offset)) => snapshot.lookup_command(ref_id) match { case Some(ref_cmd) =>