author | wenzelm |
Fri, 27 Jul 2012 14:09:59 +0200 | |
changeset 48548 | 49afe0e92163 |
parent 48409 | 0d2114eb412a |
child 48920 | 9f84d872feba |
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 |
||
48409 | 10 |
import java.io.{File => JFile} |
11 |
||
12 |
||
32450 | 13 |
object Position |
14 |
{ |
|
43780 | 15 |
type T = Properties.T |
27968 | 16 |
|
45666 | 17 |
val Line = new Properties.Int(Isabelle_Markup.LINE) |
18 |
val Offset = new Properties.Int(Isabelle_Markup.OFFSET) |
|
19 |
val End_Offset = new Properties.Int(Isabelle_Markup.END_OFFSET) |
|
20 |
val File = new Properties.String(Isabelle_Markup.FILE) |
|
21 |
val Id = new Properties.Long(Isabelle_Markup.ID) |
|
31705 | 22 |
|
38722
ba31936497c2
organized markup properties via apply/unapply patterns;
wenzelm
parents:
38568
diff
changeset
|
23 |
object Range |
ba31936497c2
organized markup properties via apply/unapply patterns;
wenzelm
parents:
38568
diff
changeset
|
24 |
{ |
ba31936497c2
organized markup properties via apply/unapply patterns;
wenzelm
parents:
38568
diff
changeset
|
25 |
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
|
26 |
def unapply(pos: T): Option[Text.Range] = |
ba31936497c2
organized markup properties via apply/unapply patterns;
wenzelm
parents:
38568
diff
changeset
|
27 |
(Offset.unapply(pos), End_Offset.unapply(pos)) match { |
ba31936497c2
organized markup properties via apply/unapply patterns;
wenzelm
parents:
38568
diff
changeset
|
28 |
case (Some(start), Some(stop)) if start <= stop => Some(Text.Range(start, stop)) |
39041 | 29 |
case (Some(start), None) => Some(Text.Range(start, start + 1)) |
38722
ba31936497c2
organized markup properties via apply/unapply patterns;
wenzelm
parents:
38568
diff
changeset
|
30 |
case _ => None |
ba31936497c2
organized markup properties via apply/unapply patterns;
wenzelm
parents:
38568
diff
changeset
|
31 |
} |
ba31936497c2
organized markup properties via apply/unapply patterns;
wenzelm
parents:
38568
diff
changeset
|
32 |
} |
38872 | 33 |
|
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
|
34 |
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
|
35 |
{ |
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 |
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
|
37 |
(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
|
38 |
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
|
39 |
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
|
40 |
} |
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
|
41 |
} |
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
|
42 |
|
42327
7c7cc7590eb3
Name_Space.entry_markup: keep def position as separate properties;
wenzelm
parents:
41483
diff
changeset
|
43 |
private val purge_pos = Map( |
45666 | 44 |
Isabelle_Markup.DEF_LINE -> Isabelle_Markup.LINE, |
45 |
Isabelle_Markup.DEF_OFFSET -> Isabelle_Markup.OFFSET, |
|
46 |
Isabelle_Markup.DEF_END_OFFSET -> Isabelle_Markup.END_OFFSET, |
|
47 |
Isabelle_Markup.DEF_FILE -> Isabelle_Markup.FILE, |
|
48 |
Isabelle_Markup.DEF_ID -> Isabelle_Markup.ID) |
|
42327
7c7cc7590eb3
Name_Space.entry_markup: keep def position as separate properties;
wenzelm
parents:
41483
diff
changeset
|
49 |
|
7c7cc7590eb3
Name_Space.entry_markup: keep def position as separate properties;
wenzelm
parents:
41483
diff
changeset
|
50 |
def purge(props: T): T = |
45666 | 51 |
for ((x, y) <- props if !Isabelle_Markup.POSITION_PROPERTIES(x)) |
42327
7c7cc7590eb3
Name_Space.entry_markup: keep def position as separate properties;
wenzelm
parents:
41483
diff
changeset
|
52 |
yield (if (purge_pos.isDefinedAt(x)) (purge_pos(x), y) else (x, y)) |
48370 | 53 |
|
54 |
||
55 |
def str_of(props: T): String = |
|
56 |
(Line.unapply(props), File.unapply(props)) match { |
|
57 |
case (Some(i), None) => " (line " + i.toString + ")" |
|
58 |
case (Some(i), Some(name)) => " (line " + i.toString + " of " + quote(name) + ")" |
|
59 |
case (None, Some(name)) => " (file " + quote(name) + ")" |
|
60 |
case _ => "" |
|
61 |
} |
|
27968 | 62 |
} |