author | wenzelm |
Mon, 19 Jan 2009 21:04:30 +0100 | |
changeset 34482 | 0f4b34445f40 |
parent 34481 | 660c639870a4 |
child 34483 | 0923926022d7 |
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 |
34481
660c639870a4
replaced type parameter C by Command (thanks to globally simultaneous scope);
wenzelm
parents:
34407
diff
changeset
|
9 |
import isabelle.prover.Command |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
10 |
|
34388 | 11 |
object Token { |
34482 | 12 |
object Kind extends Enumeration { |
13 |
val COMMAND_START = Value("COMMAND_START") |
|
14 |
val COMMENT = Value("COMMENT") |
|
15 |
val OTHER = Value("OTHER") |
|
34388 | 16 |
} |
34389 | 17 |
|
34481
660c639870a4
replaced type parameter C by Command (thanks to globally simultaneous scope);
wenzelm
parents:
34407
diff
changeset
|
18 |
def checkStart(t : Token, P : (Int) => Boolean) |
34482 | 19 |
= t != null && P(t.start) |
34389 | 20 |
|
34481
660c639870a4
replaced type parameter C by Command (thanks to globally simultaneous scope);
wenzelm
parents:
34407
diff
changeset
|
21 |
def checkStop(t : Token, P : (Int) => Boolean) |
34482 | 22 |
= t != null && P(t.stop) |
34389 | 23 |
|
34481
660c639870a4
replaced type parameter C by Command (thanks to globally simultaneous scope);
wenzelm
parents:
34407
diff
changeset
|
24 |
def scan(s : Token, f : Token => Boolean) : Token = { |
34389 | 25 |
var current = s |
26 |
while (current != null) { |
|
27 |
val next = current.next |
|
28 |
if (next == null || f(next)) |
|
34482 | 29 |
return current |
34389 | 30 |
current = next |
31 |
} |
|
32 |
return null |
|
33 |
} |
|
34 |
||
34388 | 35 |
} |
36 |
||
34482 | 37 |
class Token(var start : Int, var stop : Int, var kind : Token.Kind.Value) { |
34481
660c639870a4
replaced type parameter C by Command (thanks to globally simultaneous scope);
wenzelm
parents:
34407
diff
changeset
|
38 |
var next : Token = null |
660c639870a4
replaced type parameter C by Command (thanks to globally simultaneous scope);
wenzelm
parents:
34407
diff
changeset
|
39 |
var previous : Token = null |
660c639870a4
replaced type parameter C by Command (thanks to globally simultaneous scope);
wenzelm
parents:
34407
diff
changeset
|
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 |
|
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
44 |
def shift(offset : Int, bottomClamp : Int) { |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
45 |
start = bottomClamp max (start + offset) |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
46 |
stop = bottomClamp max (stop + offset) |
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 |
|
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
49 |
override def hashCode() : Int = (31 + start) * 31 + stop |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
50 |
|
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
51 |
override def equals(obj : Any) : Boolean = { |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
52 |
if (super.equals(obj)) |
34482 | 53 |
return true; |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
54 |
|
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
55 |
if (null == obj) |
34482 | 56 |
return false; |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
57 |
|
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
58 |
obj match { |
34481
660c639870a4
replaced type parameter C by Command (thanks to globally simultaneous scope);
wenzelm
parents:
34407
diff
changeset
|
59 |
case other: Token => |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
60 |
(start == other.start) && (stop == other.stop) |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
61 |
case other: Any => false |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
62 |
} |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
63 |
} |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
64 |
} |