author | wenzelm |
Tue, 20 Jan 2009 22:29:41 +0100 | |
changeset 34492 | 2268cbe29fca |
parent 34483 | 0923926022d7 |
child 34526 | b504abb6eff6 |
child 34533 | 35308320713a |
permissions | -rw-r--r-- |
34407 | 1 |
/* |
2 |
* Document tokens as text ranges |
|
3 |
* |
|
4 |
* @author Johannes Hölzl, TU Munich |
|
5 |
* @author Fabian Immler, TU Munich |
|
6 |
*/ |
|
7 |
||
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
8 |
package isabelle.proofdocument |
34483 | 9 |
|
10 |
||
34481
660c639870a4
replaced type parameter C by Command (thanks to globally simultaneous scope);
wenzelm
parents:
34407
diff
changeset
|
11 |
import isabelle.prover.Command |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
12 |
|
34483 | 13 |
|
34388 | 14 |
object Token { |
34482 | 15 |
object Kind extends Enumeration { |
16 |
val COMMAND_START = Value("COMMAND_START") |
|
17 |
val COMMENT = Value("COMMENT") |
|
18 |
val OTHER = Value("OTHER") |
|
34388 | 19 |
} |
34389 | 20 |
|
34483 | 21 |
def check_start(t: Token, P: Int => Boolean) = { t != null && P(t.start) } |
22 |
def check_stop(t: Token, P: Int => Boolean) = { t != null && P(t.stop) } |
|
34389 | 23 |
|
34483 | 24 |
def scan(s: Token, f: Token => Boolean): Token = |
25 |
{ |
|
34389 | 26 |
var current = s |
27 |
while (current != null) { |
|
28 |
val next = current.next |
|
34483 | 29 |
if (next == null || f(next)) return current |
34389 | 30 |
current = next |
31 |
} |
|
32 |
return null |
|
33 |
} |
|
34388 | 34 |
} |
35 |
||
34492 | 36 |
class Token(var start: Int, var stop: Int, val kind: Token.Kind.Value) |
34483 | 37 |
{ |
38 |
var next: Token = null |
|
39 |
var prev: Token = null |
|
40 |
var command: Command = null |
|
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
41 |
|
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
42 |
def length = stop - start |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
43 |
|
34483 | 44 |
def shift(offset: Int, bottom_clamp: Int) { |
45 |
start = bottom_clamp max (start + offset) |
|
46 |
stop = bottom_clamp max (stop + offset) |
|
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
47 |
} |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
48 |
|
34483 | 49 |
override def hashCode: Int = (31 + start) * 31 + stop |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
50 |
|
34483 | 51 |
override def equals(obj: Any): Boolean = |
52 |
{ |
|
53 |
if (super.equals(obj)) return true |
|
54 |
if (null == obj) return false |
|
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
55 |
obj match { |
34483 | 56 |
case other: Token => (start == other.start) && (stop == other.stop) |
57 |
case other: Any => false |
|
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
58 |
} |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
59 |
} |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
60 |
} |