equal
deleted
inserted
replaced
11 |
11 |
12 |
12 |
13 import scala.collection.mutable |
13 import scala.collection.mutable |
14 import scala.util.Sorting |
14 import scala.util.Sorting |
15 |
15 |
16 import info.hupel.isabelle.api.XML // + for Isabelle/Isac |
16 import edu.tum.cs.isabelle.api.XML // + for Isabelle/Isac |
17 |
17 |
18 |
18 |
19 object Text |
19 object Text |
20 { |
20 { |
21 /* offset */ |
21 /* offset */ |
39 |
39 |
40 sealed case class Range(start: Offset, stop: Offset) |
40 sealed case class Range(start: Offset, stop: Offset) |
41 { |
41 { |
42 // denotation: {start} Un {i. start < i & i < stop} |
42 // denotation: {start} Un {i. start < i & i < stop} |
43 if (start > stop) |
43 if (start > stop) |
44 Console.printf("Bad range: [" + start.toString + ":" + stop.toString + "]") |
44 error("Bad range: [" + start.toString + ":" + stop.toString + "]") |
45 |
45 |
46 override def toString: String = "[" + start.toString + ":" + stop.toString + "]" |
46 override def toString: String = "[" + start.toString + ":" + stop.toString + "]" |
47 |
47 |
48 def length: Int = stop - start |
48 def length: Int = stop - start |
49 |
49 |