author | wenzelm |
Mon, 10 Mar 2014 13:55:03 +0100 | |
changeset 56025 | d74fed45fa8b |
parent 55884 | f2c0eaedd579 |
child 56462 | b64b0cb845fe |
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 |
|
55490 | 17 |
val none: T = Nil |
18 |
||
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49419
diff
changeset
|
19 |
val Line = new Properties.Int(Markup.LINE) |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49419
diff
changeset
|
20 |
val Offset = new Properties.Int(Markup.OFFSET) |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49419
diff
changeset
|
21 |
val End_Offset = new Properties.Int(Markup.END_OFFSET) |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49419
diff
changeset
|
22 |
val File = new Properties.String(Markup.FILE) |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49419
diff
changeset
|
23 |
val Id = new Properties.Long(Markup.ID) |
31705 | 24 |
|
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49419
diff
changeset
|
25 |
val Def_Line = new Properties.Int(Markup.DEF_LINE) |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49419
diff
changeset
|
26 |
val Def_Offset = new Properties.Int(Markup.DEF_OFFSET) |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49419
diff
changeset
|
27 |
val Def_End_Offset = new Properties.Int(Markup.DEF_END_OFFSET) |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49419
diff
changeset
|
28 |
val Def_File = new Properties.String(Markup.DEF_FILE) |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49419
diff
changeset
|
29 |
val Def_Id = new Properties.Long(Markup.DEF_ID) |
49419
e2726211f834
pass base_snapshot to enable hyperlinks into other nodes;
wenzelm
parents:
48992
diff
changeset
|
30 |
|
48920 | 31 |
object Line_File |
32 |
{ |
|
33 |
def unapply(pos: T): Option[(Int, String)] = |
|
34 |
(pos, pos) match { |
|
35 |
case (Line(i), File(name)) => Some((i, name)) |
|
36 |
case (_, File(name)) => Some((1, name)) |
|
37 |
case _ => None |
|
38 |
} |
|
39 |
} |
|
40 |
||
49419
e2726211f834
pass base_snapshot to enable hyperlinks into other nodes;
wenzelm
parents:
48992
diff
changeset
|
41 |
object Def_Line_File |
e2726211f834
pass base_snapshot to enable hyperlinks into other nodes;
wenzelm
parents:
48992
diff
changeset
|
42 |
{ |
e2726211f834
pass base_snapshot to enable hyperlinks into other nodes;
wenzelm
parents:
48992
diff
changeset
|
43 |
def unapply(pos: T): Option[(Int, String)] = |
e2726211f834
pass base_snapshot to enable hyperlinks into other nodes;
wenzelm
parents:
48992
diff
changeset
|
44 |
(pos, pos) match { |
e2726211f834
pass base_snapshot to enable hyperlinks into other nodes;
wenzelm
parents:
48992
diff
changeset
|
45 |
case (Def_Line(i), Def_File(name)) => Some((i, name)) |
e2726211f834
pass base_snapshot to enable hyperlinks into other nodes;
wenzelm
parents:
48992
diff
changeset
|
46 |
case (_, Def_File(name)) => Some((1, name)) |
e2726211f834
pass base_snapshot to enable hyperlinks into other nodes;
wenzelm
parents:
48992
diff
changeset
|
47 |
case _ => None |
e2726211f834
pass base_snapshot to enable hyperlinks into other nodes;
wenzelm
parents:
48992
diff
changeset
|
48 |
} |
e2726211f834
pass base_snapshot to enable hyperlinks into other nodes;
wenzelm
parents:
48992
diff
changeset
|
49 |
} |
e2726211f834
pass base_snapshot to enable hyperlinks into other nodes;
wenzelm
parents:
48992
diff
changeset
|
50 |
|
38722
ba31936497c2
organized markup properties via apply/unapply patterns;
wenzelm
parents:
38568
diff
changeset
|
51 |
object Range |
ba31936497c2
organized markup properties via apply/unapply patterns;
wenzelm
parents:
38568
diff
changeset
|
52 |
{ |
55884
f2c0eaedd579
tuned signature -- emphasize symbol positions (prover) vs. decoded text offsets (editor);
wenzelm
parents:
55555
diff
changeset
|
53 |
def apply(range: Symbol.Range): T = Offset(range.start) ::: Offset(range.stop) |
f2c0eaedd579
tuned signature -- emphasize symbol positions (prover) vs. decoded text offsets (editor);
wenzelm
parents:
55555
diff
changeset
|
54 |
def unapply(pos: T): Option[Symbol.Range] = |
48920 | 55 |
(pos, pos) match { |
56 |
case (Offset(start), End_Offset(stop)) if start <= stop => Some(Text.Range(start, stop)) |
|
57 |
case (Offset(start), _) => Some(Text.Range(start, start + 1)) |
|
58 |
case _ => None |
|
59 |
} |
|
60 |
} |
|
61 |
||
62 |
object Id_Offset |
|
63 |
{ |
|
55884
f2c0eaedd579
tuned signature -- emphasize symbol positions (prover) vs. decoded text offsets (editor);
wenzelm
parents:
55555
diff
changeset
|
64 |
def unapply(pos: T): Option[(Long, Symbol.Offset)] = |
48920 | 65 |
(pos, pos) match { |
66 |
case (Id(id), Offset(offset)) => Some((id, offset)) |
|
38722
ba31936497c2
organized markup properties via apply/unapply patterns;
wenzelm
parents:
38568
diff
changeset
|
67 |
case _ => None |
ba31936497c2
organized markup properties via apply/unapply patterns;
wenzelm
parents:
38568
diff
changeset
|
68 |
} |
ba31936497c2
organized markup properties via apply/unapply patterns;
wenzelm
parents:
38568
diff
changeset
|
69 |
} |
38872 | 70 |
|
49419
e2726211f834
pass base_snapshot to enable hyperlinks into other nodes;
wenzelm
parents:
48992
diff
changeset
|
71 |
object Def_Id_Offset |
e2726211f834
pass base_snapshot to enable hyperlinks into other nodes;
wenzelm
parents:
48992
diff
changeset
|
72 |
{ |
55884
f2c0eaedd579
tuned signature -- emphasize symbol positions (prover) vs. decoded text offsets (editor);
wenzelm
parents:
55555
diff
changeset
|
73 |
def unapply(pos: T): Option[(Long, Symbol.Offset)] = |
49419
e2726211f834
pass base_snapshot to enable hyperlinks into other nodes;
wenzelm
parents:
48992
diff
changeset
|
74 |
(pos, pos) match { |
e2726211f834
pass base_snapshot to enable hyperlinks into other nodes;
wenzelm
parents:
48992
diff
changeset
|
75 |
case (Def_Id(id), Def_Offset(offset)) => Some((id, offset)) |
e2726211f834
pass base_snapshot to enable hyperlinks into other nodes;
wenzelm
parents:
48992
diff
changeset
|
76 |
case _ => None |
e2726211f834
pass base_snapshot to enable hyperlinks into other nodes;
wenzelm
parents:
48992
diff
changeset
|
77 |
} |
e2726211f834
pass base_snapshot to enable hyperlinks into other nodes;
wenzelm
parents:
48992
diff
changeset
|
78 |
} |
e2726211f834
pass base_snapshot to enable hyperlinks into other nodes;
wenzelm
parents:
48992
diff
changeset
|
79 |
|
55429
4a50f9e70dc1
report (but ignore) markup within auxiliary files;
wenzelm
parents:
50201
diff
changeset
|
80 |
object Reported |
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
|
81 |
{ |
55884
f2c0eaedd579
tuned signature -- emphasize symbol positions (prover) vs. decoded text offsets (editor);
wenzelm
parents:
55555
diff
changeset
|
82 |
def unapply(pos: T): Option[(Long, String, Symbol.Range)] = |
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
|
83 |
(pos, pos) match { |
55429
4a50f9e70dc1
report (but ignore) markup within auxiliary files;
wenzelm
parents:
50201
diff
changeset
|
84 |
case (Id(id), Range(range)) => |
4a50f9e70dc1
report (but ignore) markup within auxiliary files;
wenzelm
parents:
50201
diff
changeset
|
85 |
Some((id, File.unapply(pos).getOrElse(""), range)) |
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
|
86 |
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
|
87 |
} |
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
|
88 |
} |
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
|
89 |
|
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49419
diff
changeset
|
90 |
def purge(props: T): T = props.filterNot(p => Markup.POSITION_PROPERTIES(p._1)) |
48370 | 91 |
|
92 |
||
48992 | 93 |
/* here: inlined formal markup */ |
94 |
||
95 |
def here(pos: T): String = |
|
48920 | 96 |
(Line.unapply(pos), File.unapply(pos)) match { |
48370 | 97 |
case (Some(i), None) => " (line " + i.toString + ")" |
98 |
case (Some(i), Some(name)) => " (line " + i.toString + " of " + quote(name) + ")" |
|
99 |
case (None, Some(name)) => " (file " + quote(name) + ")" |
|
100 |
case _ => "" |
|
101 |
} |
|
27968 | 102 |
} |