author | immler@in.tum.de |
Wed, 22 Apr 2009 17:35:49 +0200 | |
changeset 34554 | 7dc6c231da40 |
parent 34551 | bd2b8fde9e25 |
child 34584 | 3457ef52de04 |
child 34593 | cf37a9f988bf |
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 |
|
34526 | 21 |
private def fill(n: Int) = { |
22 |
val blanks = new Array[Char](n) |
|
23 |
for(i <- 0 to n - 1) blanks(i) = ' ' |
|
24 |
new String(blanks) |
|
25 |
} |
|
34551
bd2b8fde9e25
incomplete changes of immutable tokens and commands
immler@in.tum.de
parents:
34539
diff
changeset
|
26 |
def string_from_tokens (tokens: List[Token], starts: Map[Token, Int]): String = { |
bd2b8fde9e25
incomplete changes of immutable tokens and commands
immler@in.tum.de
parents:
34539
diff
changeset
|
27 |
def stop(t: Token) = starts(t) + t.length |
34526 | 28 |
tokens match { |
29 |
case Nil => "" |
|
34551
bd2b8fde9e25
incomplete changes of immutable tokens and commands
immler@in.tum.de
parents:
34539
diff
changeset
|
30 |
case t::tokens => ( tokens.foldLeft |
bd2b8fde9e25
incomplete changes of immutable tokens and commands
immler@in.tum.de
parents:
34539
diff
changeset
|
31 |
(t.content, stop(t)) |
bd2b8fde9e25
incomplete changes of immutable tokens and commands
immler@in.tum.de
parents:
34539
diff
changeset
|
32 |
((a, token) => (a._1 + fill(starts(token) - a._2) + token.content, stop(token))) |
34526 | 33 |
)._1 |
34389 | 34 |
} |
35 |
} |
|
34526 | 36 |
|
34388 | 37 |
} |
38 |
||
34551
bd2b8fde9e25
incomplete changes of immutable tokens and commands
immler@in.tum.de
parents:
34539
diff
changeset
|
39 |
class Token(val content: String, val kind: Token.Kind.Value) { |
34526 | 40 |
val length = content.length |
34554
7dc6c231da40
abs. stops, markup nodes depend on doc-version;
immler@in.tum.de
parents:
34551
diff
changeset
|
41 |
override def toString = content |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
42 |
} |