src/Pure/library.scala
author wenzelm
Wed, 03 Mar 2021 21:58:29 +0100
changeset 73602 ec52a1a6ed31
parent 73594 f5c147654661
child 73604 31d4274f32de
permissions -rw-r--r--
tuned --- fewer warnings;
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
69403
ed0824ef337e static type for Library.using: avoid Java 11 warnings on "Illegal reflective access";
wenzelm
parents: 68715
diff changeset
    19
  def using[A <: AutoCloseable, B](a: A)(f: A => B): B =
63789
af28929ff219 support resource management;
wenzelm
parents: 63781
diff changeset
    20
  {
69403
ed0824ef337e static type for Library.using: avoid Java 11 warnings on "Illegal reflective access";
wenzelm
parents: 68715
diff changeset
    21
    try { f(a) }
ed0824ef337e static type for Library.using: avoid Java 11 warnings on "Illegal reflective access";
wenzelm
parents: 68715
diff changeset
    22
    finally { if (a != null) a.close() }
63789
af28929ff219 support resource management;
wenzelm
parents: 63781
diff changeset
    23
  }
af28929ff219 support resource management;
wenzelm
parents: 63781
diff changeset
    24
af28929ff219 support resource management;
wenzelm
parents: 63781
diff changeset
    25
57909
0fb331032f02 more compact representation of special string values;
wenzelm
parents: 57831
diff changeset
    26
  /* integers */
0fb331032f02 more compact representation of special string values;
wenzelm
parents: 57831
diff changeset
    27
0fb331032f02 more compact representation of special string values;
wenzelm
parents: 57831
diff changeset
    28
  private val small_int = 10000
0fb331032f02 more compact representation of special string values;
wenzelm
parents: 57831
diff changeset
    29
  private lazy val small_int_table =
0fb331032f02 more compact representation of special string values;
wenzelm
parents: 57831
diff changeset
    30
  {
0fb331032f02 more compact representation of special string values;
wenzelm
parents: 57831
diff changeset
    31
    val array = new Array[String](small_int)
0fb331032f02 more compact representation of special string values;
wenzelm
parents: 57831
diff changeset
    32
    for (i <- 0 until small_int) array(i) = i.toString
0fb331032f02 more compact representation of special string values;
wenzelm
parents: 57831
diff changeset
    33
    array
0fb331032f02 more compact representation of special string values;
wenzelm
parents: 57831
diff changeset
    34
  }
0fb331032f02 more compact representation of special string values;
wenzelm
parents: 57831
diff changeset
    35
0fb331032f02 more compact representation of special string values;
wenzelm
parents: 57831
diff changeset
    36
  def is_small_int(s: String): Boolean =
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
    val len = s.length
0fb331032f02 more compact representation of special string values;
wenzelm
parents: 57831
diff changeset
    39
    1 <= len && len <= 4 &&
0fb331032f02 more compact representation of special string values;
wenzelm
parents: 57831
diff changeset
    40
    s.forall(c => '0' <= c && c <= '9') &&
0fb331032f02 more compact representation of special string values;
wenzelm
parents: 57831
diff changeset
    41
    (len == 1 || s(0) != '0')
0fb331032f02 more compact representation of special string values;
wenzelm
parents: 57831
diff changeset
    42
  }
0fb331032f02 more compact representation of special string values;
wenzelm
parents: 57831
diff changeset
    43
0fb331032f02 more compact representation of special string values;
wenzelm
parents: 57831
diff changeset
    44
  def signed_string_of_long(i: Long): String =
0fb331032f02 more compact representation of special string values;
wenzelm
parents: 57831
diff changeset
    45
    if (0 <= i && i < small_int) small_int_table(i.toInt)
0fb331032f02 more compact representation of special string values;
wenzelm
parents: 57831
diff changeset
    46
    else i.toString
0fb331032f02 more compact representation of special string values;
wenzelm
parents: 57831
diff changeset
    47
0fb331032f02 more compact representation of special string values;
wenzelm
parents: 57831
diff changeset
    48
  def signed_string_of_int(i: Int): String =
0fb331032f02 more compact representation of special string values;
wenzelm
parents: 57831
diff changeset
    49
    if (0 <= i && i < small_int) small_int_table(i)
0fb331032f02 more compact representation of special string values;
wenzelm
parents: 57831
diff changeset
    50
    else i.toString
0fb331032f02 more compact representation of special string values;
wenzelm
parents: 57831
diff changeset
    51
0fb331032f02 more compact representation of special string values;
wenzelm
parents: 57831
diff changeset
    52
48996
a8bad1369ada clarified separated_chunks vs. space_explode;
wenzelm
parents: 48479
diff changeset
    53
  /* separated chunks */
36688
321d392ab12e added separate;
wenzelm
parents: 36685
diff changeset
    54
321d392ab12e added separate;
wenzelm
parents: 36685
diff changeset
    55
  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
    56
  {
a8ffd3692f57 more scalable Library.separate -- NB: JVM has tiny fixed-size stack;
wenzelm
parents: 51616
diff changeset
    57
    val result = new mutable.ListBuffer[A]
a8ffd3692f57 more scalable Library.separate -- NB: JVM has tiny fixed-size stack;
wenzelm
parents: 51616
diff changeset
    58
    var first = true
a8ffd3692f57 more scalable Library.separate -- NB: JVM has tiny fixed-size stack;
wenzelm
parents: 51616
diff changeset
    59
    for (x <- list) {
a8ffd3692f57 more scalable Library.separate -- NB: JVM has tiny fixed-size stack;
wenzelm
parents: 51616
diff changeset
    60
      if (first) {
a8ffd3692f57 more scalable Library.separate -- NB: JVM has tiny fixed-size stack;
wenzelm
parents: 51616
diff changeset
    61
        first = false
a8ffd3692f57 more scalable Library.separate -- NB: JVM has tiny fixed-size stack;
wenzelm
parents: 51616
diff changeset
    62
        result += x
a8ffd3692f57 more scalable Library.separate -- NB: JVM has tiny fixed-size stack;
wenzelm
parents: 51616
diff changeset
    63
      }
a8ffd3692f57 more scalable Library.separate -- NB: JVM has tiny fixed-size stack;
wenzelm
parents: 51616
diff changeset
    64
      else {
a8ffd3692f57 more scalable Library.separate -- NB: JVM has tiny fixed-size stack;
wenzelm
parents: 51616
diff changeset
    65
        result += s
a8ffd3692f57 more scalable Library.separate -- NB: JVM has tiny fixed-size stack;
wenzelm
parents: 51616
diff changeset
    66
        result += x
a8ffd3692f57 more scalable Library.separate -- NB: JVM has tiny fixed-size stack;
wenzelm
parents: 51616
diff changeset
    67
      }
36688
321d392ab12e added separate;
wenzelm
parents: 36685
diff changeset
    68
    }
51981
a8ffd3692f57 more scalable Library.separate -- NB: JVM has tiny fixed-size stack;
wenzelm
parents: 51616
diff changeset
    69
    result.toList
a8ffd3692f57 more scalable Library.separate -- NB: JVM has tiny fixed-size stack;
wenzelm
parents: 51616
diff changeset
    70
  }
36688
321d392ab12e added separate;
wenzelm
parents: 36685
diff changeset
    71
56600
628e039cc34d more specific support for sequence of words;
wenzelm
parents: 56599
diff changeset
    72
  def separated_chunks(sep: Char => Boolean, source: CharSequence): Iterator[CharSequence] =
48996
a8bad1369ada clarified separated_chunks vs. space_explode;
wenzelm
parents: 48479
diff changeset
    73
    new Iterator[CharSequence] {
a8bad1369ada clarified separated_chunks vs. space_explode;
wenzelm
parents: 48479
diff changeset
    74
      private val end = source.length
a8bad1369ada clarified separated_chunks vs. space_explode;
wenzelm
parents: 48479
diff changeset
    75
      private def next_chunk(i: Int): Option[(CharSequence, Int)] =
a8bad1369ada clarified separated_chunks vs. space_explode;
wenzelm
parents: 48479
diff changeset
    76
      {
a8bad1369ada clarified separated_chunks vs. space_explode;
wenzelm
parents: 48479
diff changeset
    77
        if (i < end) {
56600
628e039cc34d more specific support for sequence of words;
wenzelm
parents: 56599
diff changeset
    78
          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
    79
          Some((source.subSequence(i + 1, j), j))
a8bad1369ada clarified separated_chunks vs. space_explode;
wenzelm
parents: 48479
diff changeset
    80
        }
a8bad1369ada clarified separated_chunks vs. space_explode;
wenzelm
parents: 48479
diff changeset
    81
        else None
43598
826ddd91ae2b basic operations on lists and strings;
wenzelm
parents: 43442
diff changeset
    82
      }
48996
a8bad1369ada clarified separated_chunks vs. space_explode;
wenzelm
parents: 48479
diff changeset
    83
      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
    84
73587
0af9e7e4476f tuned --- fewer warnings;
wenzelm
parents: 73583
diff changeset
    85
      def hasNext: Boolean = state.isDefined
48996
a8bad1369ada clarified separated_chunks vs. space_explode;
wenzelm
parents: 48479
diff changeset
    86
      def next(): CharSequence =
a8bad1369ada clarified separated_chunks vs. space_explode;
wenzelm
parents: 48479
diff changeset
    87
        state match {
60215
5fb4990dfc73 misc tuning, based on warnings by IntelliJ IDEA;
wenzelm
parents: 59697
diff changeset
    88
          case Some((s, i)) => state = next_chunk(i); s
48996
a8bad1369ada clarified separated_chunks vs. space_explode;
wenzelm
parents: 48479
diff changeset
    89
          case None => Iterator.empty.next()
a8bad1369ada clarified separated_chunks vs. space_explode;
wenzelm
parents: 48479
diff changeset
    90
        }
43598
826ddd91ae2b basic operations on lists and strings;
wenzelm
parents: 43442
diff changeset
    91
    }
826ddd91ae2b basic operations on lists and strings;
wenzelm
parents: 43442
diff changeset
    92
48996
a8bad1369ada clarified separated_chunks vs. space_explode;
wenzelm
parents: 48479
diff changeset
    93
  def space_explode(sep: Char, str: String): List[String] =
56600
628e039cc34d more specific support for sequence of words;
wenzelm
parents: 56599
diff changeset
    94
    separated_chunks(_ == sep, str).map(_.toString).toList
48996
a8bad1369ada clarified separated_chunks vs. space_explode;
wenzelm
parents: 48479
diff changeset
    95
a8bad1369ada clarified separated_chunks vs. space_explode;
wenzelm
parents: 48479
diff changeset
    96
a8bad1369ada clarified separated_chunks vs. space_explode;
wenzelm
parents: 48479
diff changeset
    97
  /* lines */
a8bad1369ada clarified separated_chunks vs. space_explode;
wenzelm
parents: 48479
diff changeset
    98
64002
08f89f0e8a62 clarified modules;
wenzelm
parents: 63926
diff changeset
    99
  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
   100
48996
a8bad1369ada clarified separated_chunks vs. space_explode;
wenzelm
parents: 48479
diff changeset
   101
  def cat_lines(lines: TraversableOnce[String]): String = lines.mkString("\n")
a8bad1369ada clarified separated_chunks vs. space_explode;
wenzelm
parents: 48479
diff changeset
   102
43670
7f933761764b prefer space_explode/split_lines as in Isabelle/ML;
wenzelm
parents: 43652
diff changeset
   103
  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
   104
62590
0c837beeb5e7 upgrade "isabelle build" to Isabelle/Scala;
wenzelm
parents: 62492
diff changeset
   105
  def prefix_lines(prfx: String, str: String): String =
71362
wenzelm
parents: 69403
diff changeset
   106
    if (str == "") str else cat_lines(split_lines(str).map(prfx + _))
62590
0c837beeb5e7 upgrade "isabelle build" to Isabelle/Scala;
wenzelm
parents: 62492
diff changeset
   107
48996
a8bad1369ada clarified separated_chunks vs. space_explode;
wenzelm
parents: 48479
diff changeset
   108
  def first_line(source: CharSequence): String =
a8bad1369ada clarified separated_chunks vs. space_explode;
wenzelm
parents: 48479
diff changeset
   109
  {
56600
628e039cc34d more specific support for sequence of words;
wenzelm
parents: 56599
diff changeset
   110
    val lines = separated_chunks(_ == '\n', source)
73594
f5c147654661 tuned --- fewer warnings;
wenzelm
parents: 73589
diff changeset
   111
    if (lines.hasNext) lines.next().toString
48996
a8bad1369ada clarified separated_chunks vs. space_explode;
wenzelm
parents: 48479
diff changeset
   112
    else ""
a8bad1369ada clarified separated_chunks vs. space_explode;
wenzelm
parents: 48479
diff changeset
   113
  }
a8bad1369ada clarified separated_chunks vs. space_explode;
wenzelm
parents: 48479
diff changeset
   114
73582
wenzelm
parents: 73364
diff changeset
   115
  def trim_line(s: String): String =
wenzelm
parents: 73364
diff changeset
   116
    if (s.endsWith("\r\n")) s.substring(0, s.length - 2)
wenzelm
parents: 73364
diff changeset
   117
    else if (s.endsWith("\r") || s.endsWith("\n")) s.substring(0, s.length - 1)
wenzelm
parents: 73364
diff changeset
   118
    else s
wenzelm
parents: 73364
diff changeset
   119
wenzelm
parents: 73364
diff changeset
   120
  def trim_split_lines(s: String): List[String] =
wenzelm
parents: 73364
diff changeset
   121
    split_lines(trim_line(s)).map(trim_line)
wenzelm
parents: 73364
diff changeset
   122
65932
db5e701b691a clarified modules;
wenzelm
parents: 65903
diff changeset
   123
  def encode_lines(s: String): String = s.replace('\n', '\u000b')
db5e701b691a clarified modules;
wenzelm
parents: 65903
diff changeset
   124
  def decode_lines(s: String): String = s.replace('\u000b', '\n')
db5e701b691a clarified modules;
wenzelm
parents: 65903
diff changeset
   125
50847
78c40f1cc9b3 tuned signature;
wenzelm
parents: 50845
diff changeset
   126
78c40f1cc9b3 tuned signature;
wenzelm
parents: 50845
diff changeset
   127
  /* strings */
78c40f1cc9b3 tuned signature;
wenzelm
parents: 50845
diff changeset
   128
73583
b70d82358c6d clarified signature;
wenzelm
parents: 73582
diff changeset
   129
  def cat_strings0(strs: TraversableOnce[String]): String = strs.mkString("\u0000")
b70d82358c6d clarified signature;
wenzelm
parents: 73582
diff changeset
   130
  def split_strings0(str: String): List[String] = space_explode('\u0000', str)
b70d82358c6d clarified signature;
wenzelm
parents: 73582
diff changeset
   131
64355
c6a1031cf925 support for XML as HTML;
wenzelm
parents: 64207
diff changeset
   132
  def make_string(f: StringBuilder => Unit): String =
c6a1031cf925 support for XML as HTML;
wenzelm
parents: 64207
diff changeset
   133
  {
c6a1031cf925 support for XML as HTML;
wenzelm
parents: 64207
diff changeset
   134
    val s = new StringBuilder
c6a1031cf925 support for XML as HTML;
wenzelm
parents: 64207
diff changeset
   135
    f(s)
c6a1031cf925 support for XML as HTML;
wenzelm
parents: 64207
diff changeset
   136
    s.toString
c6a1031cf925 support for XML as HTML;
wenzelm
parents: 64207
diff changeset
   137
  }
c6a1031cf925 support for XML as HTML;
wenzelm
parents: 64207
diff changeset
   138
50847
78c40f1cc9b3 tuned signature;
wenzelm
parents: 50845
diff changeset
   139
  def try_unprefix(prfx: String, s: String): Option[String] =
78c40f1cc9b3 tuned signature;
wenzelm
parents: 50845
diff changeset
   140
    if (s.startsWith(prfx)) Some(s.substring(prfx.length)) else None
78c40f1cc9b3 tuned signature;
wenzelm
parents: 50845
diff changeset
   141
55033
8e8243975860 support for nested text cartouches;
wenzelm
parents: 54548
diff changeset
   142
  def try_unsuffix(sffx: String, s: String): Option[String] =
8e8243975860 support for nested text cartouches;
wenzelm
parents: 54548
diff changeset
   143
    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
   144
65606
wenzelm
parents: 64871
diff changeset
   145
  def perhaps_unprefix(prfx: String, s: String): String = try_unprefix(prfx, s) getOrElse s
wenzelm
parents: 64871
diff changeset
   146
  def perhaps_unsuffix(sffx: String, s: String): String = try_unsuffix(sffx, s) getOrElse s
wenzelm
parents: 64871
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
72090
bfc120aa737a clarified signature;
wenzelm
parents: 71816
diff changeset
   150
  def strip_ansi_color(s: String): String =
73602
ec52a1a6ed31 tuned --- fewer warnings;
wenzelm
parents: 73594
diff changeset
   151
    s.replaceAll("\u001b\\[\\d+m", "")
72090
bfc120aa737a clarified signature;
wenzelm
parents: 71816
diff changeset
   152
43598
826ddd91ae2b basic operations on lists and strings;
wenzelm
parents: 43442
diff changeset
   153
48996
a8bad1369ada clarified separated_chunks vs. space_explode;
wenzelm
parents: 48479
diff changeset
   154
  /* quote */
46196
805de058722b added cat_lines convenience;
wenzelm
parents: 45900
diff changeset
   155
67820
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67436
diff changeset
   156
  def single_quote(s: String): String = "'" + s + "'"
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67436
diff changeset
   157
43598
826ddd91ae2b basic operations on lists and strings;
wenzelm
parents: 43442
diff changeset
   158
  def quote(s: String): String = "\"" + s + "\""
56843
b2bfcd8cda80 support for path completion based on file-system content;
wenzelm
parents: 56730
diff changeset
   159
b2bfcd8cda80 support for path completion based on file-system content;
wenzelm
parents: 56730
diff changeset
   160
  def try_unquote(s: String): Option[String] =
b2bfcd8cda80 support for path completion based on file-system content;
wenzelm
parents: 56730
diff changeset
   161
    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
   162
    else None
b2bfcd8cda80 support for path completion based on file-system content;
wenzelm
parents: 56730
diff changeset
   163
58592
b0fff34d3247 completion for bibtex entries;
wenzelm
parents: 57909
diff changeset
   164
  def perhaps_unquote(s: String): String = try_unquote(s) getOrElse s
b0fff34d3247 completion for bibtex entries;
wenzelm
parents: 57909
diff changeset
   165
43598
826ddd91ae2b basic operations on lists and strings;
wenzelm
parents: 43442
diff changeset
   166
  def commas(ss: Iterable[String]): String = ss.iterator.mkString(", ")
48362
c3192ccb0ff4 proper commas_quote;
wenzelm
parents: 48345
diff changeset
   167
  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
   168
36688
321d392ab12e added separate;
wenzelm
parents: 36685
diff changeset
   169
51983
32692ce4c61a more frugal line termination, to cope with huge log files (see also 016cb7d8f297);
wenzelm
parents: 51981
diff changeset
   170
  /* CharSequence */
34141
297b2149077d simiplified result of keyword parser (again);
wenzelm
parents: 34136
diff changeset
   171
297b2149077d simiplified result of keyword parser (again);
wenzelm
parents: 34136
diff changeset
   172
  class Reverse(text: CharSequence, start: Int, end: Int) extends CharSequence
297b2149077d simiplified result of keyword parser (again);
wenzelm
parents: 34136
diff changeset
   173
  {
73364
c3589f2dff31 more informative errors: simplify diagnosis of spurious failures reported by users;
wenzelm
parents: 72449
diff changeset
   174
    require(0 <= start && start <= end && end <= text.length, "bad reverse range")
34141
297b2149077d simiplified result of keyword parser (again);
wenzelm
parents: 34136
diff changeset
   175
297b2149077d simiplified result of keyword parser (again);
wenzelm
parents: 34136
diff changeset
   176
    def this(text: CharSequence) = this(text, 0, text.length)
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 length: Int = end - start
297b2149077d simiplified result of keyword parser (again);
wenzelm
parents: 34136
diff changeset
   179
    def charAt(i: Int): Char = text.charAt(end - i - 1)
297b2149077d simiplified result of keyword parser (again);
wenzelm
parents: 34136
diff changeset
   180
297b2149077d simiplified result of keyword parser (again);
wenzelm
parents: 34136
diff changeset
   181
    def subSequence(i: Int, j: Int): CharSequence =
297b2149077d simiplified result of keyword parser (again);
wenzelm
parents: 34136
diff changeset
   182
      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
   183
      else throw new IndexOutOfBoundsException
297b2149077d simiplified result of keyword parser (again);
wenzelm
parents: 34136
diff changeset
   184
297b2149077d simiplified result of keyword parser (again);
wenzelm
parents: 34136
diff changeset
   185
    override def toString: String =
297b2149077d simiplified result of keyword parser (again);
wenzelm
parents: 34136
diff changeset
   186
    {
297b2149077d simiplified result of keyword parser (again);
wenzelm
parents: 34136
diff changeset
   187
      val buf = new StringBuilder(length)
297b2149077d simiplified result of keyword parser (again);
wenzelm
parents: 34136
diff changeset
   188
      for (i <- 0 until length)
297b2149077d simiplified result of keyword parser (again);
wenzelm
parents: 34136
diff changeset
   189
        buf.append(charAt(i))
297b2149077d simiplified result of keyword parser (again);
wenzelm
parents: 34136
diff changeset
   190
      buf.toString
297b2149077d simiplified result of keyword parser (again);
wenzelm
parents: 34136
diff changeset
   191
    }
297b2149077d simiplified result of keyword parser (again);
wenzelm
parents: 34136
diff changeset
   192
  }
297b2149077d simiplified result of keyword parser (again);
wenzelm
parents: 34136
diff changeset
   193
51983
32692ce4c61a more frugal line termination, to cope with huge log files (see also 016cb7d8f297);
wenzelm
parents: 51981
diff changeset
   194
  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
   195
  {
32692ce4c61a more frugal line termination, to cope with huge log files (see also 016cb7d8f297);
wenzelm
parents: 51981
diff changeset
   196
    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
   197
    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
   198
    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
   199
      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
   200
      else text.subSequence(i, j)
32692ce4c61a more frugal line termination, to cope with huge log files (see also 016cb7d8f297);
wenzelm
parents: 51981
diff changeset
   201
    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
   202
  }
32692ce4c61a more frugal line termination, to cope with huge log files (see also 016cb7d8f297);
wenzelm
parents: 51981
diff changeset
   203
34141
297b2149077d simiplified result of keyword parser (again);
wenzelm
parents: 34136
diff changeset
   204
59224
wenzelm
parents: 58592
diff changeset
   205
  /* regular expressions */
wenzelm
parents: 58592
diff changeset
   206
wenzelm
parents: 58592
diff changeset
   207
  def make_regex(s: String): Option[Regex] =
wenzelm
parents: 58592
diff changeset
   208
    try { Some(new Regex(s)) } catch { case ERROR(_) => None }
wenzelm
parents: 58592
diff changeset
   209
64871
wenzelm
parents: 64820
diff changeset
   210
  def is_regex_meta(c: Char): Boolean = """()[]{}\^$|?*+.<>-=!""".contains(c)
wenzelm
parents: 64820
diff changeset
   211
wenzelm
parents: 64820
diff changeset
   212
  def escape_regex(s: String): String =
71816
97ccf48c2f0c misc tuning based on hints by IntelliJ IDEA;
wenzelm
parents: 71588
diff changeset
   213
    if (s.exists(is_regex_meta)) {
64871
wenzelm
parents: 64820
diff changeset
   214
      (for (c <- s.iterator)
wenzelm
parents: 64820
diff changeset
   215
       yield { if (is_regex_meta(c)) "\\" + c.toString else c.toString }).mkString
wenzelm
parents: 64820
diff changeset
   216
    }
wenzelm
parents: 64820
diff changeset
   217
    else s
wenzelm
parents: 64820
diff changeset
   218
59224
wenzelm
parents: 58592
diff changeset
   219
61885
c0f34fe6aa61 clarified length of block with pre-existant forced breaks;
wenzelm
parents: 60215
diff changeset
   220
  /* lists */
c0f34fe6aa61 clarified length of block with pre-existant forced breaks;
wenzelm
parents: 60215
diff changeset
   221
c0f34fe6aa61 clarified length of block with pre-existant forced breaks;
wenzelm
parents: 60215
diff changeset
   222
  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
   223
    (xs.takeWhile(pred), xs.dropWhile(pred))
56686
2386d1a3ca8f canonical list operations, as in ML;
wenzelm
parents: 56672
diff changeset
   224
67434
a38c74b0886d more operations (as in ML);
wenzelm
parents: 67431
diff changeset
   225
  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
   226
  {
a38c74b0886d more operations (as in ML);
wenzelm
parents: 67431
diff changeset
   227
    val rev_xs = xs.reverse
a38c74b0886d more operations (as in ML);
wenzelm
parents: 67431
diff changeset
   228
    (rev_xs.dropWhile(pred).reverse, rev_xs.takeWhile(pred).reverse)
a38c74b0886d more operations (as in ML);
wenzelm
parents: 67431
diff changeset
   229
  }
a38c74b0886d more operations (as in ML);
wenzelm
parents: 67431
diff changeset
   230
a38c74b0886d more operations (as in ML);
wenzelm
parents: 67431
diff changeset
   231
  def trim[A](pred: A => Boolean, xs: List[A]): List[A] =
a38c74b0886d more operations (as in ML);
wenzelm
parents: 67431
diff changeset
   232
    take_suffix(pred, take_prefix(pred, xs)._2)._1
a38c74b0886d more operations (as in ML);
wenzelm
parents: 67431
diff changeset
   233
60215
5fb4990dfc73 misc tuning, based on warnings by IntelliJ IDEA;
wenzelm
parents: 59697
diff changeset
   234
  def member[A, B](xs: List[A])(x: B): Boolean = xs.contains(x)
56688
f3932166a33d more canonical list operations;
wenzelm
parents: 56686
diff changeset
   235
  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
   236
  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
   237
  def update[A](x: A)(xs: List[A]): List[A] = x :: remove(x)(xs)
63736
133e3e84e6fb some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents: 62590
diff changeset
   238
63867
fb46c031c841 maintain abbrevs in canonical reverse order;
wenzelm
parents: 63789
diff changeset
   239
  def merge[A](xs: List[A], ys: List[A]): List[A] =
fb46c031c841 maintain abbrevs in canonical reverse order;
wenzelm
parents: 63789
diff changeset
   240
    if (xs.eq(ys)) xs
fb46c031c841 maintain abbrevs in canonical reverse order;
wenzelm
parents: 63789
diff changeset
   241
    else if (xs.isEmpty) ys
fb46c031c841 maintain abbrevs in canonical reverse order;
wenzelm
parents: 63789
diff changeset
   242
    else ys.foldRight(xs)(Library.insert(_)(_))
fb46c031c841 maintain abbrevs in canonical reverse order;
wenzelm
parents: 63789
diff changeset
   243
64207
ad15c2f478b5 more general operations;
wenzelm
parents: 64065
diff changeset
   244
  def distinct[A](xs: List[A], eq: (A, A) => Boolean = (x: A, y: A) => x == y): List[A] =
63736
133e3e84e6fb some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents: 62590
diff changeset
   245
  {
133e3e84e6fb some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents: 62590
diff changeset
   246
    val result = new mutable.ListBuffer[A]
64207
ad15c2f478b5 more general operations;
wenzelm
parents: 64065
diff changeset
   247
    xs.foreach(x => if (!result.exists(y => eq(x, y))) result += x)
63736
133e3e84e6fb some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents: 62590
diff changeset
   248
    result.toList
133e3e84e6fb some support for merge of Isabelle/jEdit shortcuts wrt. jEdit keymap;
wenzelm
parents: 62590
diff changeset
   249
  }
63781
af9fe0b6b78e support for (single) primary key;
wenzelm
parents: 63773
diff changeset
   250
64207
ad15c2f478b5 more general operations;
wenzelm
parents: 64065
diff changeset
   251
  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
   252
  {
af9fe0b6b78e support for (single) primary key;
wenzelm
parents: 63773
diff changeset
   253
    val result = new mutable.ListBuffer[A]
af9fe0b6b78e support for (single) primary key;
wenzelm
parents: 63773
diff changeset
   254
    @tailrec def dups(rest: List[A]): Unit =
af9fe0b6b78e support for (single) primary key;
wenzelm
parents: 63773
diff changeset
   255
      rest match {
af9fe0b6b78e support for (single) primary key;
wenzelm
parents: 63773
diff changeset
   256
        case Nil =>
af9fe0b6b78e support for (single) primary key;
wenzelm
parents: 63773
diff changeset
   257
        case x :: xs =>
64207
ad15c2f478b5 more general operations;
wenzelm
parents: 64065
diff changeset
   258
          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
   259
          dups(xs)
af9fe0b6b78e support for (single) primary key;
wenzelm
parents: 63773
diff changeset
   260
      }
af9fe0b6b78e support for (single) primary key;
wenzelm
parents: 63773
diff changeset
   261
    dups(lst)
af9fe0b6b78e support for (single) primary key;
wenzelm
parents: 63773
diff changeset
   262
    result.toList
af9fe0b6b78e support for (single) primary key;
wenzelm
parents: 63773
diff changeset
   263
  }
65761
ce909161d030 more operations;
wenzelm
parents: 65718
diff changeset
   264
68715
8197c2857267 more operations (as in ML);
wenzelm
parents: 67885
diff changeset
   265
  def replicate[A](n: Int, a: A): List[A] =
8197c2857267 more operations (as in ML);
wenzelm
parents: 67885
diff changeset
   266
    if (n < 0) throw new IllegalArgumentException
8197c2857267 more operations (as in ML);
wenzelm
parents: 67885
diff changeset
   267
    else if (n == 0) Nil
8197c2857267 more operations (as in ML);
wenzelm
parents: 67885
diff changeset
   268
    else {
8197c2857267 more operations (as in ML);
wenzelm
parents: 67885
diff changeset
   269
      val res = new mutable.ListBuffer[A]
8197c2857267 more operations (as in ML);
wenzelm
parents: 67885
diff changeset
   270
      (1 to n).foreach(_ => res += a)
8197c2857267 more operations (as in ML);
wenzelm
parents: 67885
diff changeset
   271
      res.toList
8197c2857267 more operations (as in ML);
wenzelm
parents: 67885
diff changeset
   272
    }
8197c2857267 more operations (as in ML);
wenzelm
parents: 67885
diff changeset
   273
65761
ce909161d030 more operations;
wenzelm
parents: 65718
diff changeset
   274
ce909161d030 more operations;
wenzelm
parents: 65718
diff changeset
   275
  /* proper values */
ce909161d030 more operations;
wenzelm
parents: 65718
diff changeset
   276
ce909161d030 more operations;
wenzelm
parents: 65718
diff changeset
   277
  def proper_string(s: String): Option[String] =
ce909161d030 more operations;
wenzelm
parents: 65718
diff changeset
   278
    if (s == null || s == "") None else Some(s)
ce909161d030 more operations;
wenzelm
parents: 65718
diff changeset
   279
ce909161d030 more operations;
wenzelm
parents: 65718
diff changeset
   280
  def proper_list[A](list: List[A]): Option[List[A]] =
ce909161d030 more operations;
wenzelm
parents: 65718
diff changeset
   281
    if (list == null || list.isEmpty) None else Some(list)
72449
5924c1da3c45 clarified modules;
wenzelm
parents: 72090
diff changeset
   282
5924c1da3c45 clarified modules;
wenzelm
parents: 72090
diff changeset
   283
5924c1da3c45 clarified modules;
wenzelm
parents: 72090
diff changeset
   284
  /* reflection */
5924c1da3c45 clarified modules;
wenzelm
parents: 72090
diff changeset
   285
5924c1da3c45 clarified modules;
wenzelm
parents: 72090
diff changeset
   286
  def is_subclass[A, B](a: Class[A], b: Class[B]): Boolean =
5924c1da3c45 clarified modules;
wenzelm
parents: 72090
diff changeset
   287
  {
73589
9efdebe24c65 tuned --- fewer warnings;
wenzelm
parents: 73587
diff changeset
   288
    import scala.language.existentials
72449
5924c1da3c45 clarified modules;
wenzelm
parents: 72090
diff changeset
   289
    @tailrec def subclass(c: Class[_]): Boolean =
5924c1da3c45 clarified modules;
wenzelm
parents: 72090
diff changeset
   290
    {
5924c1da3c45 clarified modules;
wenzelm
parents: 72090
diff changeset
   291
      c == b ||
5924c1da3c45 clarified modules;
wenzelm
parents: 72090
diff changeset
   292
        {
5924c1da3c45 clarified modules;
wenzelm
parents: 72090
diff changeset
   293
          val d = c.getSuperclass
5924c1da3c45 clarified modules;
wenzelm
parents: 72090
diff changeset
   294
          d != null && subclass(d)
5924c1da3c45 clarified modules;
wenzelm
parents: 72090
diff changeset
   295
        }
5924c1da3c45 clarified modules;
wenzelm
parents: 72090
diff changeset
   296
    }
5924c1da3c45 clarified modules;
wenzelm
parents: 72090
diff changeset
   297
    subclass(a)
5924c1da3c45 clarified modules;
wenzelm
parents: 72090
diff changeset
   298
  }
34136
3dcb46ae6185 added basic library -- Scala version;
wenzelm
parents:
diff changeset
   299
}