src/Pure/library.scala
author paulson <lp15@cam.ac.uk>
Sun, 20 May 2018 18:37:34 +0100
changeset 68239 0764ee22a4d1
parent 67885 839a624aabb9
child 68715 8197c2857267
permissions -rw-r--r--
tidy up of Derivative
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
34136
3dcb46ae6185 added basic library -- Scala version;
wenzelm
parents:
diff changeset
     1
/*  Title:      Pure/library.scala
3dcb46ae6185 added basic library -- Scala version;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
3dcb46ae6185 added basic library -- Scala version;
wenzelm
parents:
diff changeset
     3
3dcb46ae6185 added basic library -- Scala version;
wenzelm
parents:
diff changeset
     4
Basic library.
3dcb46ae6185 added basic library -- Scala version;
wenzelm
parents:
diff changeset
     5
*/
3dcb46ae6185 added basic library -- Scala version;
wenzelm
parents:
diff changeset
     6
3dcb46ae6185 added basic library -- Scala version;
wenzelm
parents:
diff changeset
     7
package isabelle
3dcb46ae6185 added basic library -- Scala version;
wenzelm
parents:
diff changeset
     8
38258
dd7dcb9b2637 added Library.thread_actor -- thread as actor;
wenzelm
parents: 38232
diff changeset
     9
63781
af9fe0b6b78e support for (single) primary key;
wenzelm
parents: 63773
diff changeset
    10
import scala.annotation.tailrec
51981
a8ffd3692f57 more scalable Library.separate -- NB: JVM has tiny fixed-size stack;
wenzelm
parents: 51616
diff changeset
    11
import scala.collection.mutable
59224
wenzelm
parents: 58592
diff changeset
    12
import scala.util.matching.Regex
51981
a8ffd3692f57 more scalable Library.separate -- NB: JVM has tiny fixed-size stack;
wenzelm
parents: 51616
diff changeset
    13
37018
39f4cce5a22c added somewhat generic zoom box;
wenzelm
parents: 36791
diff changeset
    14
34136
3dcb46ae6185 added basic library -- Scala version;
wenzelm
parents:
diff changeset
    15
object Library
3dcb46ae6185 added basic library -- Scala version;
wenzelm
parents:
diff changeset
    16
{
63789
af28929ff219 support resource management;
wenzelm
parents: 63781
diff changeset
    17
  /* resource management */
af28929ff219 support resource management;
wenzelm
parents: 63781
diff changeset
    18
af28929ff219 support resource management;
wenzelm
parents: 63781
diff changeset
    19
  def using[A <: { def close() }, B](x: A)(f: A => B): B =
af28929ff219 support resource management;
wenzelm
parents: 63781
diff changeset
    20
  {
63926
70973a1b4ec0 tuned -- fewer warnings;
wenzelm
parents: 63867
diff changeset
    21
    import scala.language.reflectiveCalls
70973a1b4ec0 tuned -- fewer warnings;
wenzelm
parents: 63867
diff changeset
    22
63789
af28929ff219 support resource management;
wenzelm
parents: 63781
diff changeset
    23
    try { f(x) }
af28929ff219 support resource management;
wenzelm
parents: 63781
diff changeset
    24
    finally { if (x != null) x.close() }
af28929ff219 support resource management;
wenzelm
parents: 63781
diff changeset
    25
  }
af28929ff219 support resource management;
wenzelm
parents: 63781
diff changeset
    26
af28929ff219 support resource management;
wenzelm
parents: 63781
diff changeset
    27
57909
0fb331032f02 more compact representation of special string values;
wenzelm
parents: 57831
diff changeset
    28
  /* integers */
0fb331032f02 more compact representation of special string values;
wenzelm
parents: 57831
diff changeset
    29
0fb331032f02 more compact representation of special string values;
wenzelm
parents: 57831
diff changeset
    30
  private val small_int = 10000
0fb331032f02 more compact representation of special string values;
wenzelm
parents: 57831
diff changeset
    31
  private lazy val small_int_table =
0fb331032f02 more compact representation of special string values;
wenzelm
parents: 57831
diff changeset
    32
  {
0fb331032f02 more compact representation of special string values;
wenzelm
parents: 57831
diff changeset
    33
    val array = new Array[String](small_int)
0fb331032f02 more compact representation of special string values;
wenzelm
parents: 57831
diff changeset
    34
    for (i <- 0 until small_int) array(i) = i.toString
0fb331032f02 more compact representation of special string values;
wenzelm
parents: 57831
diff changeset
    35
    array
0fb331032f02 more compact representation of special string values;
wenzelm
parents: 57831
diff changeset
    36
  }
0fb331032f02 more compact representation of special string values;
wenzelm
parents: 57831
diff changeset
    37
0fb331032f02 more compact representation of special string values;
wenzelm
parents: 57831
diff changeset
    38
  def is_small_int(s: String): Boolean =
0fb331032f02 more compact representation of special string values;
wenzelm
parents: 57831
diff changeset
    39
  {
0fb331032f02 more compact representation of special string values;
wenzelm
parents: 57831
diff changeset
    40
    val len = s.length
0fb331032f02 more compact representation of special string values;
wenzelm
parents: 57831
diff changeset
    41
    1 <= len && len <= 4 &&
0fb331032f02 more compact representation of special string values;
wenzelm
parents: 57831
diff changeset
    42
    s.forall(c => '0' <= c && c <= '9') &&
0fb331032f02 more compact representation of special string values;
wenzelm
parents: 57831
diff changeset
    43
    (len == 1 || s(0) != '0')
0fb331032f02 more compact representation of special string values;
wenzelm
parents: 57831
diff changeset
    44
  }
0fb331032f02 more compact representation of special string values;
wenzelm
parents: 57831
diff changeset
    45
0fb331032f02 more compact representation of special string values;
wenzelm
parents: 57831
diff changeset
    46
  def signed_string_of_long(i: Long): String =
0fb331032f02 more compact representation of special string values;
wenzelm
parents: 57831
diff changeset
    47
    if (0 <= i && i < small_int) small_int_table(i.toInt)
0fb331032f02 more compact representation of special string values;
wenzelm
parents: 57831
diff changeset
    48
    else i.toString
0fb331032f02 more compact representation of special string values;
wenzelm
parents: 57831
diff changeset
    49
0fb331032f02 more compact representation of special string values;
wenzelm
parents: 57831
diff changeset
    50
  def signed_string_of_int(i: Int): String =
0fb331032f02 more compact representation of special string values;
wenzelm
parents: 57831
diff changeset
    51
    if (0 <= i && i < small_int) small_int_table(i)
0fb331032f02 more compact representation of special string values;
wenzelm
parents: 57831
diff changeset
    52
    else i.toString
0fb331032f02 more compact representation of special string values;
wenzelm
parents: 57831
diff changeset
    53
0fb331032f02 more compact representation of special string values;
wenzelm
parents: 57831
diff changeset
    54
48996
a8bad1369ada clarified separated_chunks vs. space_explode;
wenzelm
parents: 48479
diff changeset
    55
  /* separated chunks */
36688
321d392ab12e added separate;
wenzelm
parents: 36685
diff changeset
    56
321d392ab12e added separate;
wenzelm
parents: 36685
diff changeset
    57
  def separate[A](s: A, list: List[A]): List[A] =
51981
a8ffd3692f57 more scalable Library.separate -- NB: JVM has tiny fixed-size stack;
wenzelm
parents: 51616
diff changeset
    58
  {
a8ffd3692f57 more scalable Library.separate -- NB: JVM has tiny fixed-size stack;
wenzelm
parents: 51616
diff changeset
    59
    val result = new mutable.ListBuffer[A]
a8ffd3692f57 more scalable Library.separate -- NB: JVM has tiny fixed-size stack;
wenzelm
parents: 51616
diff changeset
    60
    var first = true
a8ffd3692f57 more scalable Library.separate -- NB: JVM has tiny fixed-size stack;
wenzelm
parents: 51616
diff changeset
    61
    for (x <- list) {
a8ffd3692f57 more scalable Library.separate -- NB: JVM has tiny fixed-size stack;
wenzelm
parents: 51616
diff changeset
    62
      if (first) {
a8ffd3692f57 more scalable Library.separate -- NB: JVM has tiny fixed-size stack;
wenzelm
parents: 51616
diff changeset
    63
        first = false
a8ffd3692f57 more scalable Library.separate -- NB: JVM has tiny fixed-size stack;
wenzelm
parents: 51616
diff changeset
    64
        result += x
a8ffd3692f57 more scalable Library.separate -- NB: JVM has tiny fixed-size stack;
wenzelm
parents: 51616
diff changeset
    65
      }
a8ffd3692f57 more scalable Library.separate -- NB: JVM has tiny fixed-size stack;
wenzelm
parents: 51616
diff changeset
    66
      else {
a8ffd3692f57 more scalable Library.separate -- NB: JVM has tiny fixed-size stack;
wenzelm
parents: 51616
diff changeset
    67
        result += s
a8ffd3692f57 more scalable Library.separate -- NB: JVM has tiny fixed-size stack;
wenzelm
parents: 51616
diff changeset
    68
        result += x
a8ffd3692f57 more scalable Library.separate -- NB: JVM has tiny fixed-size stack;
wenzelm
parents: 51616
diff changeset
    69
      }
36688
321d392ab12e added separate;
wenzelm
parents: 36685
diff changeset
    70
    }
51981
a8ffd3692f57 more scalable Library.separate -- NB: JVM has tiny fixed-size stack;
wenzelm
parents: 51616
diff changeset
    71
    result.toList
a8ffd3692f57 more scalable Library.separate -- NB: JVM has tiny fixed-size stack;
wenzelm
parents: 51616
diff changeset
    72
  }
36688
321d392ab12e added separate;
wenzelm
parents: 36685
diff changeset
    73
56600
628e039cc34d more specific support for sequence of words;
wenzelm
parents: 56599
diff changeset
    74
  def separated_chunks(sep: Char => Boolean, source: CharSequence): Iterator[CharSequence] =
48996
a8bad1369ada clarified separated_chunks vs. space_explode;
wenzelm
parents: 48479
diff changeset
    75
    new Iterator[CharSequence] {
a8bad1369ada clarified separated_chunks vs. space_explode;
wenzelm
parents: 48479
diff changeset
    76
      private val end = source.length
a8bad1369ada clarified separated_chunks vs. space_explode;
wenzelm
parents: 48479
diff changeset
    77
      private def next_chunk(i: Int): Option[(CharSequence, Int)] =
a8bad1369ada clarified separated_chunks vs. space_explode;
wenzelm
parents: 48479
diff changeset
    78
      {
a8bad1369ada clarified separated_chunks vs. space_explode;
wenzelm
parents: 48479
diff changeset
    79
        if (i < end) {
56600
628e039cc34d more specific support for sequence of words;
wenzelm
parents: 56599
diff changeset
    80
          var j = i; do j += 1 while (j < end && !sep(source.charAt(j)))
48996
a8bad1369ada clarified separated_chunks vs. space_explode;
wenzelm
parents: 48479
diff changeset
    81
          Some((source.subSequence(i + 1, j), j))
a8bad1369ada clarified separated_chunks vs. space_explode;
wenzelm
parents: 48479
diff changeset
    82
        }
a8bad1369ada clarified separated_chunks vs. space_explode;
wenzelm
parents: 48479
diff changeset
    83
        else None
43598
826ddd91ae2b basic operations on lists and strings;
wenzelm
parents: 43442
diff changeset
    84
      }
48996
a8bad1369ada clarified separated_chunks vs. space_explode;
wenzelm
parents: 48479
diff changeset
    85
      private var state: Option[(CharSequence, Int)] = if (end == 0) None else next_chunk(-1)
a8bad1369ada clarified separated_chunks vs. space_explode;
wenzelm
parents: 48479
diff changeset
    86
a8bad1369ada clarified separated_chunks vs. space_explode;
wenzelm
parents: 48479
diff changeset
    87
      def hasNext(): Boolean = state.isDefined
a8bad1369ada clarified separated_chunks vs. space_explode;
wenzelm
parents: 48479
diff changeset
    88
      def next(): CharSequence =
a8bad1369ada clarified separated_chunks vs. space_explode;
wenzelm
parents: 48479
diff changeset
    89
        state match {
60215
5fb4990dfc73 misc tuning, based on warnings by IntelliJ IDEA;
wenzelm
parents: 59697
diff changeset
    90
          case Some((s, i)) => state = next_chunk(i); s
48996
a8bad1369ada clarified separated_chunks vs. space_explode;
wenzelm
parents: 48479
diff changeset
    91
          case None => Iterator.empty.next()
a8bad1369ada clarified separated_chunks vs. space_explode;
wenzelm
parents: 48479
diff changeset
    92
        }
43598
826ddd91ae2b basic operations on lists and strings;
wenzelm
parents: 43442
diff changeset
    93
    }
826ddd91ae2b basic operations on lists and strings;
wenzelm
parents: 43442
diff changeset
    94
48996
a8bad1369ada clarified separated_chunks vs. space_explode;
wenzelm
parents: 48479
diff changeset
    95
  def space_explode(sep: Char, str: String): List[String] =
56600
628e039cc34d more specific support for sequence of words;
wenzelm
parents: 56599
diff changeset
    96
    separated_chunks(_ == sep, str).map(_.toString).toList
48996
a8bad1369ada clarified separated_chunks vs. space_explode;
wenzelm
parents: 48479
diff changeset
    97
a8bad1369ada clarified separated_chunks vs. space_explode;
wenzelm
parents: 48479
diff changeset
    98
a8bad1369ada clarified separated_chunks vs. space_explode;
wenzelm
parents: 48479
diff changeset
    99
  /* lines */
a8bad1369ada clarified separated_chunks vs. space_explode;
wenzelm
parents: 48479
diff changeset
   100
64002
08f89f0e8a62 clarified modules;
wenzelm
parents: 63926
diff changeset
   101
  def terminate_lines(lines: TraversableOnce[String]): String = lines.mkString("", "\n", "\n")
51983
32692ce4c61a more frugal line termination, to cope with huge log files (see also 016cb7d8f297);
wenzelm
parents: 51981
diff changeset
   102
48996
a8bad1369ada clarified separated_chunks vs. space_explode;
wenzelm
parents: 48479
diff changeset
   103
  def cat_lines(lines: TraversableOnce[String]): String = lines.mkString("\n")
a8bad1369ada clarified separated_chunks vs. space_explode;
wenzelm
parents: 48479
diff changeset
   104
43670
7f933761764b prefer space_explode/split_lines as in Isabelle/ML;
wenzelm
parents: 43652
diff changeset
   105
  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
   106
62590
0c837beeb5e7 upgrade "isabelle build" to Isabelle/Scala;
wenzelm
parents: 62492
diff changeset
   107
  def prefix_lines(prfx: String, str: String): String =
0c837beeb5e7 upgrade "isabelle build" to Isabelle/Scala;
wenzelm
parents: 62492
diff changeset
   108
    if (str == "") str
0c837beeb5e7 upgrade "isabelle build" to Isabelle/Scala;
wenzelm
parents: 62492
diff changeset
   109
    else cat_lines(split_lines(str).map(s => prfx + s))
0c837beeb5e7 upgrade "isabelle build" to Isabelle/Scala;
wenzelm
parents: 62492
diff changeset
   110
48996
a8bad1369ada clarified separated_chunks vs. space_explode;
wenzelm
parents: 48479
diff changeset
   111
  def first_line(source: CharSequence): String =
a8bad1369ada clarified separated_chunks vs. space_explode;
wenzelm
parents: 48479
diff changeset
   112
  {
56600
628e039cc34d more specific support for sequence of words;
wenzelm
parents: 56599
diff changeset
   113
    val lines = separated_chunks(_ == '\n', source)
48996
a8bad1369ada clarified separated_chunks vs. space_explode;
wenzelm
parents: 48479
diff changeset
   114
    if (lines.hasNext) lines.next.toString
a8bad1369ada clarified separated_chunks vs. space_explode;
wenzelm
parents: 48479
diff changeset
   115
    else ""
a8bad1369ada clarified separated_chunks vs. space_explode;
wenzelm
parents: 48479
diff changeset
   116
  }
a8bad1369ada clarified separated_chunks vs. space_explode;
wenzelm
parents: 48479
diff changeset
   117
65932
db5e701b691a clarified modules;
wenzelm
parents: 65903
diff changeset
   118
  def encode_lines(s: String): String = s.replace('\n', '\u000b')
db5e701b691a clarified modules;
wenzelm
parents: 65903
diff changeset
   119
  def decode_lines(s: String): String = s.replace('\u000b', '\n')
db5e701b691a clarified modules;
wenzelm
parents: 65903
diff changeset
   120
50847
78c40f1cc9b3 tuned signature;
wenzelm
parents: 50845
diff changeset
   121
78c40f1cc9b3 tuned signature;
wenzelm
parents: 50845
diff changeset
   122
  /* strings */
78c40f1cc9b3 tuned signature;
wenzelm
parents: 50845
diff changeset
   123
64355
c6a1031cf925 support for XML as HTML;
wenzelm
parents: 64207
diff changeset
   124
  def make_string(f: StringBuilder => Unit): String =
c6a1031cf925 support for XML as HTML;
wenzelm
parents: 64207
diff changeset
   125
  {
c6a1031cf925 support for XML as HTML;
wenzelm
parents: 64207
diff changeset
   126
    val s = new StringBuilder
c6a1031cf925 support for XML as HTML;
wenzelm
parents: 64207
diff changeset
   127
    f(s)
c6a1031cf925 support for XML as HTML;
wenzelm
parents: 64207
diff changeset
   128
    s.toString
c6a1031cf925 support for XML as HTML;
wenzelm
parents: 64207
diff changeset
   129
  }
c6a1031cf925 support for XML as HTML;
wenzelm
parents: 64207
diff changeset
   130
50847
78c40f1cc9b3 tuned signature;
wenzelm
parents: 50845
diff changeset
   131
  def try_unprefix(prfx: String, s: String): Option[String] =
78c40f1cc9b3 tuned signature;
wenzelm
parents: 50845
diff changeset
   132
    if (s.startsWith(prfx)) Some(s.substring(prfx.length)) else None
78c40f1cc9b3 tuned signature;
wenzelm
parents: 50845
diff changeset
   133
55033
8e8243975860 support for nested text cartouches;
wenzelm
parents: 54548
diff changeset
   134
  def try_unsuffix(sffx: String, s: String): Option[String] =
8e8243975860 support for nested text cartouches;
wenzelm
parents: 54548
diff changeset
   135
    if (s.endsWith(sffx)) Some(s.substring(0, s.length - sffx.length)) else None
8e8243975860 support for nested text cartouches;
wenzelm
parents: 54548
diff changeset
   136
65606
wenzelm
parents: 64871
diff changeset
   137
  def perhaps_unprefix(prfx: String, s: String): String = try_unprefix(prfx, s) getOrElse s
wenzelm
parents: 64871
diff changeset
   138
  def perhaps_unsuffix(sffx: String, s: String): String = try_unsuffix(sffx, s) getOrElse s
wenzelm
parents: 64871
diff changeset
   139
52444
2cfe6656d6d6 slightly improved "isabelle doc" based on Isabelle/Scala;
wenzelm
parents: 51983
diff changeset
   140
  def trim_line(s: String): String =
2cfe6656d6d6 slightly improved "isabelle doc" based on Isabelle/Scala;
wenzelm
parents: 51983
diff changeset
   141
    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
   142
    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
   143
    else s
2cfe6656d6d6 slightly improved "isabelle doc" based on Isabelle/Scala;
wenzelm
parents: 51983
diff changeset
   144
64063
2c5039363ea3 tuned signature;
wenzelm
parents: 64002
diff changeset
   145
  def trim_split_lines(s: String): List[String] =
2c5039363ea3 tuned signature;
wenzelm
parents: 64002
diff changeset
   146
    split_lines(trim_line(s)).map(trim_line(_))
2c5039363ea3 tuned signature;
wenzelm
parents: 64002
diff changeset
   147
65903
692e428803c8 clarified signature;
wenzelm
parents: 65761
diff changeset
   148
  def isolate_substring(s: String): String = new String(s.toCharArray)
64820
00488a8c042f Line.Document consists of independently allocated strings;
wenzelm
parents: 64370
diff changeset
   149
43598
826ddd91ae2b basic operations on lists and strings;
wenzelm
parents: 43442
diff changeset
   150
48996
a8bad1369ada clarified separated_chunks vs. space_explode;
wenzelm
parents: 48479
diff changeset
   151
  /* quote */
46196
805de058722b added cat_lines convenience;
wenzelm
parents: 45900
diff changeset
   152
67820
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67436
diff changeset
   153
  def single_quote(s: String): String = "'" + s + "'"
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67436
diff changeset
   154
43598
826ddd91ae2b basic operations on lists and strings;
wenzelm
parents: 43442
diff changeset
   155
  def quote(s: String): String = "\"" + s + "\""
56843
b2bfcd8cda80 support for path completion based on file-system content;
wenzelm
parents: 56730
diff changeset
   156
b2bfcd8cda80 support for path completion based on file-system content;
wenzelm
parents: 56730
diff changeset
   157
  def try_unquote(s: String): Option[String] =
b2bfcd8cda80 support for path completion based on file-system content;
wenzelm
parents: 56730
diff changeset
   158
    if (s.startsWith("\"") && s.endsWith("\"")) Some(s.substring(1, s.length - 1))
b2bfcd8cda80 support for path completion based on file-system content;
wenzelm
parents: 56730
diff changeset
   159
    else None
b2bfcd8cda80 support for path completion based on file-system content;
wenzelm
parents: 56730
diff changeset
   160
58592
b0fff34d3247 completion for bibtex entries;
wenzelm
parents: 57909
diff changeset
   161
  def perhaps_unquote(s: String): String = try_unquote(s) getOrElse s
b0fff34d3247 completion for bibtex entries;
wenzelm
parents: 57909
diff changeset
   162
43598
826ddd91ae2b basic operations on lists and strings;
wenzelm
parents: 43442
diff changeset
   163
  def commas(ss: Iterable[String]): String = ss.iterator.mkString(", ")
48362
c3192ccb0ff4 proper commas_quote;
wenzelm
parents: 48345
diff changeset
   164
  def commas_quote(ss: Iterable[String]): String = ss.iterator.map(quote).mkString(", ")
43598
826ddd91ae2b basic operations on lists and strings;
wenzelm
parents: 43442
diff changeset
   165
36688
321d392ab12e added separate;
wenzelm
parents: 36685
diff changeset
   166
51983
32692ce4c61a more frugal line termination, to cope with huge log files (see also 016cb7d8f297);
wenzelm
parents: 51981
diff changeset
   167
  /* CharSequence */
34141
297b2149077d simiplified result of keyword parser (again);
wenzelm
parents: 34136
diff changeset
   168
297b2149077d simiplified result of keyword parser (again);
wenzelm
parents: 34136
diff changeset
   169
  class Reverse(text: CharSequence, start: Int, end: Int) extends CharSequence
297b2149077d simiplified result of keyword parser (again);
wenzelm
parents: 34136
diff changeset
   170
  {
297b2149077d simiplified result of keyword parser (again);
wenzelm
parents: 34136
diff changeset
   171
    require(0 <= start && start <= end && end <= text.length)
297b2149077d simiplified result of keyword parser (again);
wenzelm
parents: 34136
diff changeset
   172
297b2149077d simiplified result of keyword parser (again);
wenzelm
parents: 34136
diff changeset
   173
    def this(text: CharSequence) = this(text, 0, text.length)
297b2149077d simiplified result of keyword parser (again);
wenzelm
parents: 34136
diff changeset
   174
297b2149077d simiplified result of keyword parser (again);
wenzelm
parents: 34136
diff changeset
   175
    def length: Int = end - start
297b2149077d simiplified result of keyword parser (again);
wenzelm
parents: 34136
diff changeset
   176
    def charAt(i: Int): Char = text.charAt(end - i - 1)
297b2149077d simiplified result of keyword parser (again);
wenzelm
parents: 34136
diff changeset
   177
297b2149077d simiplified result of keyword parser (again);
wenzelm
parents: 34136
diff changeset
   178
    def subSequence(i: Int, j: Int): CharSequence =
297b2149077d simiplified result of keyword parser (again);
wenzelm
parents: 34136
diff changeset
   179
      if (0 <= i && i <= j && j <= length) new Reverse(text, end - j, end - i)
297b2149077d simiplified result of keyword parser (again);
wenzelm
parents: 34136
diff changeset
   180
      else throw new IndexOutOfBoundsException
297b2149077d simiplified result of keyword parser (again);
wenzelm
parents: 34136
diff changeset
   181
297b2149077d simiplified result of keyword parser (again);
wenzelm
parents: 34136
diff changeset
   182
    override def toString: String =
297b2149077d simiplified result of keyword parser (again);
wenzelm
parents: 34136
diff changeset
   183
    {
297b2149077d simiplified result of keyword parser (again);
wenzelm
parents: 34136
diff changeset
   184
      val buf = new StringBuilder(length)
297b2149077d simiplified result of keyword parser (again);
wenzelm
parents: 34136
diff changeset
   185
      for (i <- 0 until length)
297b2149077d simiplified result of keyword parser (again);
wenzelm
parents: 34136
diff changeset
   186
        buf.append(charAt(i))
297b2149077d simiplified result of keyword parser (again);
wenzelm
parents: 34136
diff changeset
   187
      buf.toString
297b2149077d simiplified result of keyword parser (again);
wenzelm
parents: 34136
diff changeset
   188
    }
297b2149077d simiplified result of keyword parser (again);
wenzelm
parents: 34136
diff changeset
   189
  }
297b2149077d simiplified result of keyword parser (again);
wenzelm
parents: 34136
diff changeset
   190
51983
32692ce4c61a more frugal line termination, to cope with huge log files (see also 016cb7d8f297);
wenzelm
parents: 51981
diff changeset
   191
  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
   192
  {
32692ce4c61a more frugal line termination, to cope with huge log files (see also 016cb7d8f297);
wenzelm
parents: 51981
diff changeset
   193
    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
   194
    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
   195
    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
   196
      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
   197
      else text.subSequence(i, j)
32692ce4c61a more frugal line termination, to cope with huge log files (see also 016cb7d8f297);
wenzelm
parents: 51981
diff changeset
   198
    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
   199
  }
32692ce4c61a more frugal line termination, to cope with huge log files (see also 016cb7d8f297);
wenzelm
parents: 51981
diff changeset
   200
34141
297b2149077d simiplified result of keyword parser (again);
wenzelm
parents: 34136
diff changeset
   201
59224
wenzelm
parents: 58592
diff changeset
   202
  /* regular expressions */
wenzelm
parents: 58592
diff changeset
   203
wenzelm
parents: 58592
diff changeset
   204
  def make_regex(s: String): Option[Regex] =
wenzelm
parents: 58592
diff changeset
   205
    try { Some(new Regex(s)) } catch { case ERROR(_) => None }
wenzelm
parents: 58592
diff changeset
   206
64871
wenzelm
parents: 64820
diff changeset
   207
  def is_regex_meta(c: Char): Boolean = """()[]{}\^$|?*+.<>-=!""".contains(c)
wenzelm
parents: 64820
diff changeset
   208
wenzelm
parents: 64820
diff changeset
   209
  def escape_regex(s: String): String =
wenzelm
parents: 64820
diff changeset
   210
    if (s.exists(is_regex_meta(_))) {
wenzelm
parents: 64820
diff changeset
   211
      (for (c <- s.iterator)
wenzelm
parents: 64820
diff changeset
   212
       yield { if (is_regex_meta(c)) "\\" + c.toString else c.toString }).mkString
wenzelm
parents: 64820
diff changeset
   213
    }
wenzelm
parents: 64820
diff changeset
   214
    else s
wenzelm
parents: 64820
diff changeset
   215
59224
wenzelm
parents: 58592
diff changeset
   216
61883
c0f34fe6aa61 clarified length of block with pre-existant forced breaks;
wenzelm
parents: 60215
diff changeset
   217
  /* lists */
c0f34fe6aa61 clarified length of block with pre-existant forced breaks;
wenzelm
parents: 60215
diff changeset
   218
c0f34fe6aa61 clarified length of block with pre-existant forced breaks;
wenzelm
parents: 60215
diff changeset
   219
  def take_prefix[A](pred: A => Boolean, xs: List[A]): (List[A], List[A]) =
c0f34fe6aa61 clarified length of block with pre-existant forced breaks;
wenzelm
parents: 60215
diff changeset
   220
    (xs.takeWhile(pred), xs.dropWhile(pred))
56686
2386d1a3ca8f canonical list operations, as in ML;
wenzelm
parents: 56672
diff changeset
   221
67434
a38c74b0886d more operations (as in ML);
wenzelm
parents: 67431
diff changeset
   222
  def take_suffix[A](pred: A => Boolean, xs: List[A]): (List[A], List[A]) =
a38c74b0886d more operations (as in ML);
wenzelm
parents: 67431
diff changeset
   223
  {
a38c74b0886d more operations (as in ML);
wenzelm
parents: 67431
diff changeset
   224
    val rev_xs = xs.reverse
a38c74b0886d more operations (as in ML);
wenzelm
parents: 67431
diff changeset
   225
    (rev_xs.dropWhile(pred).reverse, rev_xs.takeWhile(pred).reverse)
a38c74b0886d more operations (as in ML);
wenzelm
parents: 67431
diff changeset
   226
  }
a38c74b0886d more operations (as in ML);
wenzelm
parents: 67431
diff changeset
   227
a38c74b0886d more operations (as in ML);
wenzelm
parents: 67431
diff changeset
   228
  def trim[A](pred: A => Boolean, xs: List[A]): List[A] =
a38c74b0886d more operations (as in ML);
wenzelm
parents: 67431
diff changeset
   229
    take_suffix(pred, take_prefix(pred, xs)._2)._1
a38c74b0886d more operations (as in ML);
wenzelm
parents: 67431
diff changeset
   230
60215
5fb4990dfc73 misc tuning, based on warnings by IntelliJ IDEA;
wenzelm
parents: 59697
diff changeset
   231
  def member[A, B](xs: List[A])(x: B): Boolean = xs.contains(x)
56688
f3932166a33d more canonical list operations;
wenzelm
parents: 56686
diff changeset
   232
  def insert[A](x: A)(xs: List[A]): List[A] = if (xs.contains(x)) xs else x :: xs
f3932166a33d more canonical list operations;
wenzelm
parents: 56686
diff changeset
   233
  def remove[A, B](x: B)(xs: List[A]): List[A] = if (member(xs)(x)) xs.filterNot(_ == x) else xs
f3932166a33d more canonical list operations;
wenzelm
parents: 56686
diff changeset
   234
  def update[A](x: A)(xs: List[A]): List[A] = x :: remove(x)(xs)
63734
133e3e84e6fb some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents: 62590
diff changeset
   235
63867
fb46c031c841 maintain abbrevs in canonical reverse order;
wenzelm
parents: 63789
diff changeset
   236
  def merge[A](xs: List[A], ys: List[A]): List[A] =
fb46c031c841 maintain abbrevs in canonical reverse order;
wenzelm
parents: 63789
diff changeset
   237
    if (xs.eq(ys)) xs
fb46c031c841 maintain abbrevs in canonical reverse order;
wenzelm
parents: 63789
diff changeset
   238
    else if (xs.isEmpty) ys
fb46c031c841 maintain abbrevs in canonical reverse order;
wenzelm
parents: 63789
diff changeset
   239
    else ys.foldRight(xs)(Library.insert(_)(_))
fb46c031c841 maintain abbrevs in canonical reverse order;
wenzelm
parents: 63789
diff changeset
   240
64207
ad15c2f478b5 more general operations;
wenzelm
parents: 64063
diff changeset
   241
  def distinct[A](xs: List[A], eq: (A, A) => Boolean = (x: A, y: A) => x == y): List[A] =
63734
133e3e84e6fb some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents: 62590
diff changeset
   242
  {
133e3e84e6fb some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents: 62590
diff changeset
   243
    val result = new mutable.ListBuffer[A]
64207
ad15c2f478b5 more general operations;
wenzelm
parents: 64063
diff changeset
   244
    xs.foreach(x => if (!result.exists(y => eq(x, y))) result += x)
63734
133e3e84e6fb some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents: 62590
diff changeset
   245
    result.toList
133e3e84e6fb some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents: 62590
diff changeset
   246
  }
63781
af9fe0b6b78e support for (single) primary key;
wenzelm
parents: 63773
diff changeset
   247
64207
ad15c2f478b5 more general operations;
wenzelm
parents: 64063
diff changeset
   248
  def duplicates[A](lst: List[A], eq: (A, A) => Boolean = (x: A, y: A) => x == y): List[A] =
63781
af9fe0b6b78e support for (single) primary key;
wenzelm
parents: 63773
diff changeset
   249
  {
af9fe0b6b78e support for (single) primary key;
wenzelm
parents: 63773
diff changeset
   250
    val result = new mutable.ListBuffer[A]
af9fe0b6b78e support for (single) primary key;
wenzelm
parents: 63773
diff changeset
   251
    @tailrec def dups(rest: List[A]): Unit =
af9fe0b6b78e support for (single) primary key;
wenzelm
parents: 63773
diff changeset
   252
      rest match {
af9fe0b6b78e support for (single) primary key;
wenzelm
parents: 63773
diff changeset
   253
        case Nil =>
af9fe0b6b78e support for (single) primary key;
wenzelm
parents: 63773
diff changeset
   254
        case x :: xs =>
64207
ad15c2f478b5 more general operations;
wenzelm
parents: 64063
diff changeset
   255
          if (!result.exists(y => eq(x, y)) && xs.exists(y => eq(x, y))) result += x
63781
af9fe0b6b78e support for (single) primary key;
wenzelm
parents: 63773
diff changeset
   256
          dups(xs)
af9fe0b6b78e support for (single) primary key;
wenzelm
parents: 63773
diff changeset
   257
      }
af9fe0b6b78e support for (single) primary key;
wenzelm
parents: 63773
diff changeset
   258
    dups(lst)
af9fe0b6b78e support for (single) primary key;
wenzelm
parents: 63773
diff changeset
   259
    result.toList
af9fe0b6b78e support for (single) primary key;
wenzelm
parents: 63773
diff changeset
   260
  }
65761
ce909161d030 more operations;
wenzelm
parents: 65718
diff changeset
   261
ce909161d030 more operations;
wenzelm
parents: 65718
diff changeset
   262
ce909161d030 more operations;
wenzelm
parents: 65718
diff changeset
   263
  /* proper values */
ce909161d030 more operations;
wenzelm
parents: 65718
diff changeset
   264
ce909161d030 more operations;
wenzelm
parents: 65718
diff changeset
   265
  def proper[A](x: A): Option[A] =
ce909161d030 more operations;
wenzelm
parents: 65718
diff changeset
   266
    if (x == null) None else Some(x)
ce909161d030 more operations;
wenzelm
parents: 65718
diff changeset
   267
ce909161d030 more operations;
wenzelm
parents: 65718
diff changeset
   268
  def proper_string(s: String): Option[String] =
ce909161d030 more operations;
wenzelm
parents: 65718
diff changeset
   269
    if (s == null || s == "") None else Some(s)
ce909161d030 more operations;
wenzelm
parents: 65718
diff changeset
   270
ce909161d030 more operations;
wenzelm
parents: 65718
diff changeset
   271
  def proper_list[A](list: List[A]): Option[List[A]] =
ce909161d030 more operations;
wenzelm
parents: 65718
diff changeset
   272
    if (list == null || list.isEmpty) None else Some(list)
34136
3dcb46ae6185 added basic library -- Scala version;
wenzelm
parents:
diff changeset
   273
}