equal
deleted
inserted
replaced
5 */ |
5 */ |
6 |
6 |
7 package isabelle |
7 package isabelle |
8 |
8 |
9 import java.lang.System |
9 import java.lang.System |
10 import java.io.File |
|
11 |
10 |
12 |
11 |
13 object Library |
12 object Library |
14 { |
13 { |
15 /* reverse CharSequence */ |
14 /* reverse CharSequence */ |
35 buf.toString |
34 buf.toString |
36 } |
35 } |
37 } |
36 } |
38 |
37 |
39 |
38 |
40 /* permissive UTF-8 decoding */ |
|
41 |
|
42 // see also http://en.wikipedia.org/wiki/UTF-8#Description |
|
43 def decode_permissive_utf8(text: CharSequence): String = |
|
44 { |
|
45 val buf = new java.lang.StringBuilder(text.length) |
|
46 var code = -1 |
|
47 var rest = 0 |
|
48 def flush() |
|
49 { |
|
50 if (code != -1) { |
|
51 if (rest == 0 && Character.isValidCodePoint(code)) |
|
52 buf.appendCodePoint(code) |
|
53 else buf.append('\uFFFD') |
|
54 code = -1 |
|
55 rest = 0 |
|
56 } |
|
57 } |
|
58 def init(x: Int, n: Int) |
|
59 { |
|
60 flush() |
|
61 code = x |
|
62 rest = n |
|
63 } |
|
64 def push(x: Int) |
|
65 { |
|
66 if (rest <= 0) init(x, -1) |
|
67 else { |
|
68 code <<= 6 |
|
69 code += x |
|
70 rest -= 1 |
|
71 } |
|
72 } |
|
73 for (i <- 0 until text.length) { |
|
74 val c = text.charAt(i) |
|
75 if (c < 128) { flush(); buf.append(c) } |
|
76 else if ((c & 0xC0) == 0x80) push(c & 0x3F) |
|
77 else if ((c & 0xE0) == 0xC0) init(c & 0x1F, 1) |
|
78 else if ((c & 0xF0) == 0xE0) init(c & 0x0F, 2) |
|
79 else if ((c & 0xF8) == 0xF0) init(c & 0x07, 3) |
|
80 } |
|
81 flush() |
|
82 buf.toString |
|
83 } |
|
84 |
|
85 |
|
86 /* temporary file */ |
|
87 |
|
88 def with_tmp_file[A](prefix: String)(body: File => A): A = |
|
89 { |
|
90 val file = File.createTempFile(prefix, null) |
|
91 val result = |
|
92 try { body(file) } |
|
93 finally { file.delete } |
|
94 result |
|
95 } |
|
96 |
|
97 |
|
98 /* timing */ |
39 /* timing */ |
99 |
40 |
100 def timeit[A](e: => A) = |
41 def timeit[A](e: => A) = |
101 { |
42 { |
102 val start = System.currentTimeMillis() |
43 val start = System.currentTimeMillis() |