--- 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)
+ }
}
--- 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
+ }
+ }
}
--- 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)
--- 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)) =>
--- 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) =>