author | wenzelm |
Mon, 30 Aug 2010 13:01:32 +0200 | |
changeset 38872 | 26c505765024 |
parent 38722 | ba31936497c2 |
child 38887 | 1261481ef5e5 |
permissions | -rw-r--r-- |
27968 | 1 |
/* Title: Pure/General/position.scala |
2 |
Author: Makarius |
|
3 |
||
4 |
Position properties. |
|
5 |
*/ |
|
6 |
||
7 |
package isabelle |
|
8 |
||
9 |
||
32450 | 10 |
object Position |
11 |
{ |
|
31705 | 12 |
type T = List[(String, String)] |
27968 | 13 |
|
38722
ba31936497c2
organized markup properties via apply/unapply patterns;
wenzelm
parents:
38568
diff
changeset
|
14 |
val Line = new Markup.Int_Property(Markup.LINE) |
ba31936497c2
organized markup properties via apply/unapply patterns;
wenzelm
parents:
38568
diff
changeset
|
15 |
val End_Line = new Markup.Int_Property(Markup.END_LINE) |
ba31936497c2
organized markup properties via apply/unapply patterns;
wenzelm
parents:
38568
diff
changeset
|
16 |
val Offset = new Markup.Int_Property(Markup.OFFSET) |
ba31936497c2
organized markup properties via apply/unapply patterns;
wenzelm
parents:
38568
diff
changeset
|
17 |
val End_Offset = new Markup.Int_Property(Markup.END_OFFSET) |
ba31936497c2
organized markup properties via apply/unapply patterns;
wenzelm
parents:
38568
diff
changeset
|
18 |
val File = new Markup.Property(Markup.FILE) |
ba31936497c2
organized markup properties via apply/unapply patterns;
wenzelm
parents:
38568
diff
changeset
|
19 |
val Id = new Markup.Long_Property(Markup.ID) |
31705 | 20 |
|
38722
ba31936497c2
organized markup properties via apply/unapply patterns;
wenzelm
parents:
38568
diff
changeset
|
21 |
object Range |
ba31936497c2
organized markup properties via apply/unapply patterns;
wenzelm
parents:
38568
diff
changeset
|
22 |
{ |
ba31936497c2
organized markup properties via apply/unapply patterns;
wenzelm
parents:
38568
diff
changeset
|
23 |
def apply(range: Text.Range): T = Offset(range.start) ++ Offset(range.stop) |
ba31936497c2
organized markup properties via apply/unapply patterns;
wenzelm
parents:
38568
diff
changeset
|
24 |
def unapply(pos: T): Option[Text.Range] = |
ba31936497c2
organized markup properties via apply/unapply patterns;
wenzelm
parents:
38568
diff
changeset
|
25 |
(Offset.unapply(pos), End_Offset.unapply(pos)) match { |
ba31936497c2
organized markup properties via apply/unapply patterns;
wenzelm
parents:
38568
diff
changeset
|
26 |
case (Some(start), Some(stop)) if start <= stop => Some(Text.Range(start, stop)) |
ba31936497c2
organized markup properties via apply/unapply patterns;
wenzelm
parents:
38568
diff
changeset
|
27 |
case (Some(start), None) => Some(Text.Range(start)) |
ba31936497c2
organized markup properties via apply/unapply patterns;
wenzelm
parents:
38568
diff
changeset
|
28 |
case _ => None |
ba31936497c2
organized markup properties via apply/unapply patterns;
wenzelm
parents:
38568
diff
changeset
|
29 |
} |
ba31936497c2
organized markup properties via apply/unapply patterns;
wenzelm
parents:
38568
diff
changeset
|
30 |
} |
38872 | 31 |
|
32 |
def purge(props: T): T = props.filterNot(p => Markup.POSITION_PROPERTIES(p._1)) |
|
27968 | 33 |
} |