equal
deleted
inserted
replaced
3 |
3 |
4 Position properties. |
4 Position properties. |
5 */ |
5 */ |
6 |
6 |
7 package isabelle |
7 package isabelle |
|
8 |
|
9 |
|
10 import java.io.{File => JFile} |
8 |
11 |
9 |
12 |
10 object Position |
13 object Position |
11 { |
14 { |
12 type T = Properties.T |
15 type T = Properties.T |
15 val Offset = new Properties.Int(Isabelle_Markup.OFFSET) |
18 val Offset = new Properties.Int(Isabelle_Markup.OFFSET) |
16 val End_Offset = new Properties.Int(Isabelle_Markup.END_OFFSET) |
19 val End_Offset = new Properties.Int(Isabelle_Markup.END_OFFSET) |
17 val File = new Properties.String(Isabelle_Markup.FILE) |
20 val File = new Properties.String(Isabelle_Markup.FILE) |
18 val Id = new Properties.Long(Isabelle_Markup.ID) |
21 val Id = new Properties.Long(Isabelle_Markup.ID) |
19 |
22 |
20 def file(f: java.io.File): T = File(Isabelle_System.posix_path(f.toString)) |
23 def file(f: JFile): T = File(Isabelle_System.posix_path(f.toString)) |
21 def line_file(i: Int, f: java.io.File): T = Line(i) ::: file(f) |
24 def line_file(i: Int, f: JFile): T = Line(i) ::: file(f) |
22 |
25 |
23 object Range |
26 object Range |
24 { |
27 { |
25 def apply(range: Text.Range): T = Offset(range.start) ++ Offset(range.stop) |
28 def apply(range: Text.Range): T = Offset(range.start) ++ Offset(range.stop) |
26 def unapply(pos: T): Option[Text.Range] = |
29 def unapply(pos: T): Option[Text.Range] = |