author | wenzelm |
Fri, 08 Jul 2011 17:04:38 +0200 | |
changeset 43710 | 7270ae921cf2 |
parent 42327 | 7c7cc7590eb3 |
child 43780 | 2cb2310d68b6 |
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 Offset = new Markup.Int_Property(Markup.OFFSET) |
ba31936497c2
organized markup properties via apply/unapply patterns;
wenzelm
parents:
38568
diff
changeset
|
16 |
val End_Offset = new Markup.Int_Property(Markup.END_OFFSET) |
ba31936497c2
organized markup properties via apply/unapply patterns;
wenzelm
parents:
38568
diff
changeset
|
17 |
val File = new Markup.Property(Markup.FILE) |
ba31936497c2
organized markup properties via apply/unapply patterns;
wenzelm
parents:
38568
diff
changeset
|
18 |
val Id = new Markup.Long_Property(Markup.ID) |
31705 | 19 |
|
38722
ba31936497c2
organized markup properties via apply/unapply patterns;
wenzelm
parents:
38568
diff
changeset
|
20 |
object Range |
ba31936497c2
organized markup properties via apply/unapply patterns;
wenzelm
parents:
38568
diff
changeset
|
21 |
{ |
ba31936497c2
organized markup properties via apply/unapply patterns;
wenzelm
parents:
38568
diff
changeset
|
22 |
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
|
23 |
def unapply(pos: T): Option[Text.Range] = |
ba31936497c2
organized markup properties via apply/unapply patterns;
wenzelm
parents:
38568
diff
changeset
|
24 |
(Offset.unapply(pos), End_Offset.unapply(pos)) match { |
ba31936497c2
organized markup properties via apply/unapply patterns;
wenzelm
parents:
38568
diff
changeset
|
25 |
case (Some(start), Some(stop)) if start <= stop => Some(Text.Range(start, stop)) |
39041 | 26 |
case (Some(start), None) => Some(Text.Range(start, start + 1)) |
38722
ba31936497c2
organized markup properties via apply/unapply patterns;
wenzelm
parents:
38568
diff
changeset
|
27 |
case _ => None |
ba31936497c2
organized markup properties via apply/unapply patterns;
wenzelm
parents:
38568
diff
changeset
|
28 |
} |
ba31936497c2
organized markup properties via apply/unapply patterns;
wenzelm
parents:
38568
diff
changeset
|
29 |
} |
38872 | 30 |
|
38887
1261481ef5e5
Command.State: add reported positions to markup tree, according main message position or Markup.binding/entity/report occurrences in body;
wenzelm
parents:
38872
diff
changeset
|
31 |
object Id_Range |
1261481ef5e5
Command.State: add reported positions to markup tree, according main message position or Markup.binding/entity/report occurrences in body;
wenzelm
parents:
38872
diff
changeset
|
32 |
{ |
1261481ef5e5
Command.State: add reported positions to markup tree, according main message position or Markup.binding/entity/report occurrences in body;
wenzelm
parents:
38872
diff
changeset
|
33 |
def unapply(pos: T): Option[(Long, Text.Range)] = |
1261481ef5e5
Command.State: add reported positions to markup tree, according main message position or Markup.binding/entity/report occurrences in body;
wenzelm
parents:
38872
diff
changeset
|
34 |
(pos, pos) match { |
1261481ef5e5
Command.State: add reported positions to markup tree, according main message position or Markup.binding/entity/report occurrences in body;
wenzelm
parents:
38872
diff
changeset
|
35 |
case (Id(id), Range(range)) => Some((id, range)) |
1261481ef5e5
Command.State: add reported positions to markup tree, according main message position or Markup.binding/entity/report occurrences in body;
wenzelm
parents:
38872
diff
changeset
|
36 |
case _ => None |
1261481ef5e5
Command.State: add reported positions to markup tree, according main message position or Markup.binding/entity/report occurrences in body;
wenzelm
parents:
38872
diff
changeset
|
37 |
} |
1261481ef5e5
Command.State: add reported positions to markup tree, according main message position or Markup.binding/entity/report occurrences in body;
wenzelm
parents:
38872
diff
changeset
|
38 |
} |
1261481ef5e5
Command.State: add reported positions to markup tree, according main message position or Markup.binding/entity/report occurrences in body;
wenzelm
parents:
38872
diff
changeset
|
39 |
|
42327
7c7cc7590eb3
Name_Space.entry_markup: keep def position as separate properties;
wenzelm
parents:
41483
diff
changeset
|
40 |
private val purge_pos = Map( |
7c7cc7590eb3
Name_Space.entry_markup: keep def position as separate properties;
wenzelm
parents:
41483
diff
changeset
|
41 |
Markup.DEF_LINE -> Markup.LINE, |
7c7cc7590eb3
Name_Space.entry_markup: keep def position as separate properties;
wenzelm
parents:
41483
diff
changeset
|
42 |
Markup.DEF_OFFSET -> Markup.OFFSET, |
7c7cc7590eb3
Name_Space.entry_markup: keep def position as separate properties;
wenzelm
parents:
41483
diff
changeset
|
43 |
Markup.DEF_END_OFFSET -> Markup.END_OFFSET, |
7c7cc7590eb3
Name_Space.entry_markup: keep def position as separate properties;
wenzelm
parents:
41483
diff
changeset
|
44 |
Markup.DEF_FILE -> Markup.FILE, |
7c7cc7590eb3
Name_Space.entry_markup: keep def position as separate properties;
wenzelm
parents:
41483
diff
changeset
|
45 |
Markup.DEF_ID -> Markup.ID) |
7c7cc7590eb3
Name_Space.entry_markup: keep def position as separate properties;
wenzelm
parents:
41483
diff
changeset
|
46 |
|
7c7cc7590eb3
Name_Space.entry_markup: keep def position as separate properties;
wenzelm
parents:
41483
diff
changeset
|
47 |
def purge(props: T): T = |
7c7cc7590eb3
Name_Space.entry_markup: keep def position as separate properties;
wenzelm
parents:
41483
diff
changeset
|
48 |
for ((x, y) <- props if !Markup.POSITION_PROPERTIES(x)) |
7c7cc7590eb3
Name_Space.entry_markup: keep def position as separate properties;
wenzelm
parents:
41483
diff
changeset
|
49 |
yield (if (purge_pos.isDefinedAt(x)) (purge_pos(x), y) else (x, y)) |
27968 | 50 |
} |