author  wenzelm 
Fri, 07 Mar 2014 14:37:25 +0100  
changeset 55977  ec4830499634 
parent 55033  8e8243975860 
child 56552  76cf86240cb7 
permissions  rwrr 
34136  1 
/* Title: Pure/library.scala 
45673
cd41e3903fbf
separate compilation of PIDE vs. Pure sources, which enables independent Scala library;
wenzelm
parents:
45667
diff
changeset

2 
Module: PIDE 
34136  3 
Author: Makarius 
4 

5 
Basic library. 

6 
*/ 

7 

8 
package isabelle 

9 

38258  10 

51981
a8ffd3692f57
more scalable Library.separate  NB: JVM has tiny fixedsize stack;
wenzelm
parents:
51616
diff
changeset

11 
import scala.collection.mutable 
a8ffd3692f57
more scalable Library.separate  NB: JVM has tiny fixedsize stack;
wenzelm
parents:
51616
diff
changeset

12 

49245
cb70157293c0
manage Isabelle/jEdit options as Isabelle/Scala options (with persistent preferences);
wenzelm
parents:
48996
diff
changeset

13 
import java.util.Locale 
50414
e17a1f179bb0
explore theory_body_files via future, for improved performance;
wenzelm
parents:
50299
diff
changeset

14 
import java.util.concurrent.{Future => JFuture, TimeUnit} 
37018  15 

16 

34136  17 
object Library 
18 
{ 

43652  19 
/* user errors */ 
20 

21 
object ERROR 

22 
{ 

23 
def apply(message: String): Throwable = new RuntimeException(message) 

48479
819f7a5f3e7f
more general notion of user ERROR (cf. 44f56fe01528);
wenzelm
parents:
48425
diff
changeset

24 
def unapply(exn: Throwable): Option[String] = Exn.user_message(exn) 
43652  25 
} 
26 

27 
def error(message: String): Nothing = throw ERROR(message) 

28 

54548  29 
def cat_message(msg1: String, msg2: String): String = 
30 
if (msg1 == "") msg2 

31 
else msg1 + "\n" + msg2 

32 

43652  33 
def cat_error(msg1: String, msg2: String): Nothing = 
54548  34 
error(cat_message(msg1, msg2)) 
43652  35 

36 

48996  37 
/* separated chunks */ 
36688  38 

39 
def separate[A](s: A, list: List[A]): List[A] = 

51981
a8ffd3692f57
more scalable Library.separate  NB: JVM has tiny fixedsize stack;
wenzelm
parents:
51616
diff
changeset

40 
{ 
a8ffd3692f57
more scalable Library.separate  NB: JVM has tiny fixedsize stack;
wenzelm
parents:
51616
diff
changeset

41 
val result = new mutable.ListBuffer[A] 
a8ffd3692f57
more scalable Library.separate  NB: JVM has tiny fixedsize stack;
wenzelm
parents:
51616
diff
changeset

42 
var first = true 
a8ffd3692f57
more scalable Library.separate  NB: JVM has tiny fixedsize stack;
wenzelm
parents:
51616
diff
changeset

43 
for (x < list) { 
a8ffd3692f57
more scalable Library.separate  NB: JVM has tiny fixedsize stack;
wenzelm
parents:
51616
diff
changeset

44 
if (first) { 
a8ffd3692f57
more scalable Library.separate  NB: JVM has tiny fixedsize stack;
wenzelm
parents:
51616
diff
changeset

45 
first = false 
a8ffd3692f57
more scalable Library.separate  NB: JVM has tiny fixedsize stack;
wenzelm
parents:
51616
diff
changeset

46 
result += x 
a8ffd3692f57
more scalable Library.separate  NB: JVM has tiny fixedsize stack;
wenzelm
parents:
51616
diff
changeset

47 
} 
a8ffd3692f57
more scalable Library.separate  NB: JVM has tiny fixedsize stack;
wenzelm
parents:
51616
diff
changeset

48 
else { 
a8ffd3692f57
more scalable Library.separate  NB: JVM has tiny fixedsize stack;
wenzelm
parents:
51616
diff
changeset

49 
result += s 
a8ffd3692f57
more scalable Library.separate  NB: JVM has tiny fixedsize stack;
wenzelm
parents:
51616
diff
changeset

50 
result += x 
a8ffd3692f57
more scalable Library.separate  NB: JVM has tiny fixedsize stack;
wenzelm
parents:
51616
diff
changeset

51 
} 
36688  52 
} 
51981
a8ffd3692f57
more scalable Library.separate  NB: JVM has tiny fixedsize stack;
wenzelm
parents:
51616
diff
changeset

53 
result.toList 
a8ffd3692f57
more scalable Library.separate  NB: JVM has tiny fixedsize stack;
wenzelm
parents:
51616
diff
changeset

54 
} 
36688  55 

48996  56 
def separated_chunks(sep: Char, source: CharSequence): Iterator[CharSequence] = 
57 
new Iterator[CharSequence] { 

58 
private val end = source.length 

59 
private def next_chunk(i: Int): Option[(CharSequence, Int)] = 

60 
{ 

61 
if (i < end) { 

62 
var j = i; do j += 1 while (j < end && source.charAt(j) != sep) 

63 
Some((source.subSequence(i + 1, j), j)) 

64 
} 

65 
else None 

43598  66 
} 
48996  67 
private var state: Option[(CharSequence, Int)] = if (end == 0) None else next_chunk(1) 
68 

69 
def hasNext(): Boolean = state.isDefined 

70 
def next(): CharSequence = 

71 
state match { 

72 
case Some((s, i)) => { state = next_chunk(i); s } 

73 
case None => Iterator.empty.next() 

74 
} 

43598  75 
} 
76 

48996  77 
def space_explode(sep: Char, str: String): List[String] = 
78 
separated_chunks(sep, str).map(_.toString).toList 

79 

80 

81 
/* lines */ 

82 

51983
32692ce4c61a
more frugal line termination, to cope with huge log files (see also 016cb7d8f297);
wenzelm
parents:
51981
diff
changeset

83 
def terminate_lines(lines: Iterable[CharSequence]): Iterable[CharSequence] = 
32692ce4c61a
more frugal line termination, to cope with huge log files (see also 016cb7d8f297);
wenzelm
parents:
51981
diff
changeset

84 
new Iterable[CharSequence] { 
32692ce4c61a
more frugal line termination, to cope with huge log files (see also 016cb7d8f297);
wenzelm
parents:
51981
diff
changeset

85 
def iterator: Iterator[CharSequence] = 
32692ce4c61a
more frugal line termination, to cope with huge log files (see also 016cb7d8f297);
wenzelm
parents:
51981
diff
changeset

86 
lines.iterator.map(line => new Line_Termination(line)) 
32692ce4c61a
more frugal line termination, to cope with huge log files (see also 016cb7d8f297);
wenzelm
parents:
51981
diff
changeset

87 
} 
32692ce4c61a
more frugal line termination, to cope with huge log files (see also 016cb7d8f297);
wenzelm
parents:
51981
diff
changeset

88 

48996  89 
def cat_lines(lines: TraversableOnce[String]): String = lines.mkString("\n") 
90 

43670
7f933761764b
prefer space_explode/split_lines as in Isabelle/ML;
wenzelm
parents:
43652
diff
changeset

91 
def split_lines(str: String): List[String] = space_explode('\n', str) 
7f933761764b
prefer space_explode/split_lines as in Isabelle/ML;
wenzelm
parents:
43652
diff
changeset

92 

48996  93 
def first_line(source: CharSequence): String = 
94 
{ 

95 
val lines = separated_chunks('\n', source) 

96 
if (lines.hasNext) lines.next.toString 

97 
else "" 

98 
} 

99 

55977  100 
def plain_words(str: String): String = 
101 
space_explode('_', str).mkString(" ") 

102 

50847  103 

104 
/* strings */ 

105 

50299  106 
def lowercase(str: String): String = str.toLowerCase(Locale.ENGLISH) 
107 
def uppercase(str: String): String = str.toUpperCase(Locale.ENGLISH) 

108 

49245
cb70157293c0
manage Isabelle/jEdit options as Isabelle/Scala options (with persistent preferences);
wenzelm
parents:
48996
diff
changeset

109 
def capitalize(str: String): String = 
cb70157293c0
manage Isabelle/jEdit options as Isabelle/Scala options (with persistent preferences);
wenzelm
parents:
48996
diff
changeset

110 
if (str.length == 0) str 
50299  111 
else uppercase(str.substring(0, 1)) + str.substring(1) 
49245
cb70157293c0
manage Isabelle/jEdit options as Isabelle/Scala options (with persistent preferences);
wenzelm
parents:
48996
diff
changeset

112 

50847  113 
def try_unprefix(prfx: String, s: String): Option[String] = 
114 
if (s.startsWith(prfx)) Some(s.substring(prfx.length)) else None 

115 

55033  116 
def try_unsuffix(sffx: String, s: String): Option[String] = 
117 
if (s.endsWith(sffx)) Some(s.substring(0, s.length  sffx.length)) else None 

118 

52444
2cfe6656d6d6
slightly improved "isabelle doc" based on Isabelle/Scala;
wenzelm
parents:
51983
diff
changeset

119 
def trim_line(s: String): String = 
2cfe6656d6d6
slightly improved "isabelle doc" based on Isabelle/Scala;
wenzelm
parents:
51983
diff
changeset

120 
if (s.endsWith("\r\n")) s.substring(0, s.length  2) 
2cfe6656d6d6
slightly improved "isabelle doc" based on Isabelle/Scala;
wenzelm
parents:
51983
diff
changeset

121 
else if (s.endsWith("\r")  s.endsWith("\n")) s.substring(0, s.length  1) 
2cfe6656d6d6
slightly improved "isabelle doc" based on Isabelle/Scala;
wenzelm
parents:
51983
diff
changeset

122 
else s 
2cfe6656d6d6
slightly improved "isabelle doc" based on Isabelle/Scala;
wenzelm
parents:
51983
diff
changeset

123 

43598  124 

48996  125 
/* quote */ 
46196  126 

43598  127 
def quote(s: String): String = "\"" + s + "\"" 
128 
def commas(ss: Iterable[String]): String = ss.iterator.mkString(", ") 

48362  129 
def commas_quote(ss: Iterable[String]): String = ss.iterator.map(quote).mkString(", ") 
43598  130 

36688  131 

51983
32692ce4c61a
more frugal line termination, to cope with huge log files (see also 016cb7d8f297);
wenzelm
parents:
51981
diff
changeset

132 
/* CharSequence */ 
34141  133 

134 
class Reverse(text: CharSequence, start: Int, end: Int) extends CharSequence 

135 
{ 

136 
require(0 <= start && start <= end && end <= text.length) 

137 

138 
def this(text: CharSequence) = this(text, 0, text.length) 

139 

140 
def length: Int = end  start 

141 
def charAt(i: Int): Char = text.charAt(end  i  1) 

142 

143 
def subSequence(i: Int, j: Int): CharSequence = 

144 
if (0 <= i && i <= j && j <= length) new Reverse(text, end  j, end  i) 

145 
else throw new IndexOutOfBoundsException 

146 

147 
override def toString: String = 

148 
{ 

149 
val buf = new StringBuilder(length) 

150 
for (i < 0 until length) 

151 
buf.append(charAt(i)) 

152 
buf.toString 

153 
} 

154 
} 

155 

51983
32692ce4c61a
more frugal line termination, to cope with huge log files (see also 016cb7d8f297);
wenzelm
parents:
51981
diff
changeset

156 
class Line_Termination(text: CharSequence) extends CharSequence 
32692ce4c61a
more frugal line termination, to cope with huge log files (see also 016cb7d8f297);
wenzelm
parents:
51981
diff
changeset

157 
{ 
32692ce4c61a
more frugal line termination, to cope with huge log files (see also 016cb7d8f297);
wenzelm
parents:
51981
diff
changeset

158 
def length: Int = text.length + 1 
32692ce4c61a
more frugal line termination, to cope with huge log files (see also 016cb7d8f297);
wenzelm
parents:
51981
diff
changeset

159 
def charAt(i: Int): Char = if (i == text.length) '\n' else text.charAt(i) 
32692ce4c61a
more frugal line termination, to cope with huge log files (see also 016cb7d8f297);
wenzelm
parents:
51981
diff
changeset

160 
def subSequence(i: Int, j: Int): CharSequence = 
32692ce4c61a
more frugal line termination, to cope with huge log files (see also 016cb7d8f297);
wenzelm
parents:
51981
diff
changeset

161 
if (j == text.length + 1) new Line_Termination(text.subSequence(i, j  1)) 
32692ce4c61a
more frugal line termination, to cope with huge log files (see also 016cb7d8f297);
wenzelm
parents:
51981
diff
changeset

162 
else text.subSequence(i, j) 
32692ce4c61a
more frugal line termination, to cope with huge log files (see also 016cb7d8f297);
wenzelm
parents:
51981
diff
changeset

163 
override def toString: String = text.toString + "\n" 
32692ce4c61a
more frugal line termination, to cope with huge log files (see also 016cb7d8f297);
wenzelm
parents:
51981
diff
changeset

164 
} 
32692ce4c61a
more frugal line termination, to cope with huge log files (see also 016cb7d8f297);
wenzelm
parents:
51981
diff
changeset

165 

34141  166 

50414
e17a1f179bb0
explore theory_body_files via future, for improved performance;
wenzelm
parents:
50299
diff
changeset

167 
/* Java futures */ 
e17a1f179bb0
explore theory_body_files via future, for improved performance;
wenzelm
parents:
50299
diff
changeset

168 

e17a1f179bb0
explore theory_body_files via future, for improved performance;
wenzelm
parents:
50299
diff
changeset

169 
def future_value[A](x: A) = new JFuture[A] 
e17a1f179bb0
explore theory_body_files via future, for improved performance;
wenzelm
parents:
50299
diff
changeset

170 
{ 
e17a1f179bb0
explore theory_body_files via future, for improved performance;
wenzelm
parents:
50299
diff
changeset

171 
def cancel(may_interrupt: Boolean): Boolean = false 
e17a1f179bb0
explore theory_body_files via future, for improved performance;
wenzelm
parents:
50299
diff
changeset

172 
def isCancelled(): Boolean = false 
e17a1f179bb0
explore theory_body_files via future, for improved performance;
wenzelm
parents:
50299
diff
changeset

173 
def isDone(): Boolean = true 
e17a1f179bb0
explore theory_body_files via future, for improved performance;
wenzelm
parents:
50299
diff
changeset

174 
def get(): A = x 
e17a1f179bb0
explore theory_body_files via future, for improved performance;
wenzelm
parents:
50299
diff
changeset

175 
def get(timeout: Long, time_unit: TimeUnit): A = x 
e17a1f179bb0
explore theory_body_files via future, for improved performance;
wenzelm
parents:
50299
diff
changeset

176 
} 
34136  177 
} 
43652  178 

179 

180 
class Basic_Library 

181 
{ 

43670
7f933761764b
prefer space_explode/split_lines as in Isabelle/ML;
wenzelm
parents:
43652
diff
changeset

182 
val ERROR = Library.ERROR 
7f933761764b
prefer space_explode/split_lines as in Isabelle/ML;
wenzelm
parents:
43652
diff
changeset

183 
val error = Library.error _ 
7f933761764b
prefer space_explode/split_lines as in Isabelle/ML;
wenzelm
parents:
43652
diff
changeset

184 
val cat_error = Library.cat_error _ 
7f933761764b
prefer space_explode/split_lines as in Isabelle/ML;
wenzelm
parents:
43652
diff
changeset

185 

43652  186 
val space_explode = Library.space_explode _ 
43670
7f933761764b
prefer space_explode/split_lines as in Isabelle/ML;
wenzelm
parents:
43652
diff
changeset

187 
val split_lines = Library.split_lines _ 
46196  188 
val cat_lines = Library.cat_lines _ 
43652  189 
val quote = Library.quote _ 
190 
val commas = Library.commas _ 

191 
val commas_quote = Library.commas_quote _ 

49470  192 

193 

194 
/* parallel tasks */ 

195 

196 
implicit def function_as_callable[A](f: () => A) = 

197 
new java.util.concurrent.Callable[A] { def call = f() } 

198 

199 
val default_thread_pool = 

200 
scala.collection.parallel.ThreadPoolTasks.defaultThreadPool 

43652  201 
} 