src/Pure/library.scala
author blanchet
Thu, 16 Dec 2010 22:45:02 +0100
changeset 41220 4d11b0de7dd8
parent 40848 8662b9b1f123
child 43442 e1fff67b23ac
permissions -rw-r--r--
discriminate SMT errors a bit better
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
38636
b7647ca7de5a module for simplified thread operations (Scala version);
wenzelm
parents: 38583
diff changeset
    10
import java.lang.System
34216
ada8eb23a08e added simple dialogs;
wenzelm
parents: 34198
diff changeset
    11
import java.awt.Component
ada8eb23a08e added simple dialogs;
wenzelm
parents: 34198
diff changeset
    12
import javax.swing.JOptionPane
34136
3dcb46ae6185 added basic library -- Scala version;
wenzelm
parents:
diff changeset
    13
37018
39f4cce5a22c added somewhat generic zoom box;
wenzelm
parents: 36791
diff changeset
    14
import scala.swing.ComboBox
39f4cce5a22c added somewhat generic zoom box;
wenzelm
parents: 36791
diff changeset
    15
import scala.swing.event.SelectionChanged
39f4cce5a22c added somewhat generic zoom box;
wenzelm
parents: 36791
diff changeset
    16
39f4cce5a22c added somewhat generic zoom box;
wenzelm
parents: 36791
diff changeset
    17
34136
3dcb46ae6185 added basic library -- Scala version;
wenzelm
parents:
diff changeset
    18
object Library
3dcb46ae6185 added basic library -- Scala version;
wenzelm
parents:
diff changeset
    19
{
37035
4834c3112788 added Library.undefined (in Scala);
wenzelm
parents: 37018
diff changeset
    20
  /* partial functions */
4834c3112788 added Library.undefined (in Scala);
wenzelm
parents: 37018
diff changeset
    21
4834c3112788 added Library.undefined (in Scala);
wenzelm
parents: 37018
diff changeset
    22
  def undefined[A, B] = new PartialFunction[A, B] {
4834c3112788 added Library.undefined (in Scala);
wenzelm
parents: 37018
diff changeset
    23
    def apply(x: A): B = throw new NoSuchElementException("undefined")
4834c3112788 added Library.undefined (in Scala);
wenzelm
parents: 37018
diff changeset
    24
    def isDefinedAt(x: A) = false
4834c3112788 added Library.undefined (in Scala);
wenzelm
parents: 37018
diff changeset
    25
  }
4834c3112788 added Library.undefined (in Scala);
wenzelm
parents: 37018
diff changeset
    26
4834c3112788 added Library.undefined (in Scala);
wenzelm
parents: 37018
diff changeset
    27
36688
321d392ab12e added separate;
wenzelm
parents: 36685
diff changeset
    28
  /* separate */
321d392ab12e added separate;
wenzelm
parents: 36685
diff changeset
    29
321d392ab12e added separate;
wenzelm
parents: 36685
diff changeset
    30
  def separate[A](s: A, list: List[A]): List[A] =
321d392ab12e added separate;
wenzelm
parents: 36685
diff changeset
    31
    list match {
321d392ab12e added separate;
wenzelm
parents: 36685
diff changeset
    32
      case x :: xs if !xs.isEmpty => x :: s :: separate(s, xs)
321d392ab12e added separate;
wenzelm
parents: 36685
diff changeset
    33
      case _ => list
321d392ab12e added separate;
wenzelm
parents: 36685
diff changeset
    34
    }
321d392ab12e added separate;
wenzelm
parents: 36685
diff changeset
    35
321d392ab12e added separate;
wenzelm
parents: 36685
diff changeset
    36
34141
297b2149077d simiplified result of keyword parser (again);
wenzelm
parents: 34136
diff changeset
    37
  /* reverse CharSequence */
297b2149077d simiplified result of keyword parser (again);
wenzelm
parents: 34136
diff changeset
    38
297b2149077d simiplified result of keyword parser (again);
wenzelm
parents: 34136
diff changeset
    39
  class Reverse(text: CharSequence, start: Int, end: Int) extends CharSequence
297b2149077d simiplified result of keyword parser (again);
wenzelm
parents: 34136
diff changeset
    40
  {
297b2149077d simiplified result of keyword parser (again);
wenzelm
parents: 34136
diff changeset
    41
    require(0 <= start && start <= end && end <= text.length)
297b2149077d simiplified result of keyword parser (again);
wenzelm
parents: 34136
diff changeset
    42
297b2149077d simiplified result of keyword parser (again);
wenzelm
parents: 34136
diff changeset
    43
    def this(text: CharSequence) = this(text, 0, text.length)
297b2149077d simiplified result of keyword parser (again);
wenzelm
parents: 34136
diff changeset
    44
297b2149077d simiplified result of keyword parser (again);
wenzelm
parents: 34136
diff changeset
    45
    def length: Int = end - start
297b2149077d simiplified result of keyword parser (again);
wenzelm
parents: 34136
diff changeset
    46
    def charAt(i: Int): Char = text.charAt(end - i - 1)
297b2149077d simiplified result of keyword parser (again);
wenzelm
parents: 34136
diff changeset
    47
297b2149077d simiplified result of keyword parser (again);
wenzelm
parents: 34136
diff changeset
    48
    def subSequence(i: Int, j: Int): CharSequence =
297b2149077d simiplified result of keyword parser (again);
wenzelm
parents: 34136
diff changeset
    49
      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
    50
      else throw new IndexOutOfBoundsException
297b2149077d simiplified result of keyword parser (again);
wenzelm
parents: 34136
diff changeset
    51
297b2149077d simiplified result of keyword parser (again);
wenzelm
parents: 34136
diff changeset
    52
    override def toString: String =
297b2149077d simiplified result of keyword parser (again);
wenzelm
parents: 34136
diff changeset
    53
    {
297b2149077d simiplified result of keyword parser (again);
wenzelm
parents: 34136
diff changeset
    54
      val buf = new StringBuilder(length)
297b2149077d simiplified result of keyword parser (again);
wenzelm
parents: 34136
diff changeset
    55
      for (i <- 0 until length)
297b2149077d simiplified result of keyword parser (again);
wenzelm
parents: 34136
diff changeset
    56
        buf.append(charAt(i))
297b2149077d simiplified result of keyword parser (again);
wenzelm
parents: 34136
diff changeset
    57
      buf.toString
297b2149077d simiplified result of keyword parser (again);
wenzelm
parents: 34136
diff changeset
    58
    }
297b2149077d simiplified result of keyword parser (again);
wenzelm
parents: 34136
diff changeset
    59
  }
297b2149077d simiplified result of keyword parser (again);
wenzelm
parents: 34136
diff changeset
    60
297b2149077d simiplified result of keyword parser (again);
wenzelm
parents: 34136
diff changeset
    61
36685
2b3076cfd6dd slightly more general Library.chunks;
wenzelm
parents: 34317
diff changeset
    62
  /* iterate over chunks (cf. space_explode/split_lines in ML) */
2b3076cfd6dd slightly more general Library.chunks;
wenzelm
parents: 34317
diff changeset
    63
2b3076cfd6dd slightly more general Library.chunks;
wenzelm
parents: 34317
diff changeset
    64
  def chunks(source: CharSequence, sep: Char = '\n') = new Iterator[CharSequence]
2b3076cfd6dd slightly more general Library.chunks;
wenzelm
parents: 34317
diff changeset
    65
  {
2b3076cfd6dd slightly more general Library.chunks;
wenzelm
parents: 34317
diff changeset
    66
    private val end = source.length
2b3076cfd6dd slightly more general Library.chunks;
wenzelm
parents: 34317
diff changeset
    67
    private def next_chunk(i: Int): Option[(CharSequence, Int)] =
2b3076cfd6dd slightly more general Library.chunks;
wenzelm
parents: 34317
diff changeset
    68
    {
2b3076cfd6dd slightly more general Library.chunks;
wenzelm
parents: 34317
diff changeset
    69
      if (i < end) {
2b3076cfd6dd slightly more general Library.chunks;
wenzelm
parents: 34317
diff changeset
    70
        var j = i; do j += 1 while (j < end && source.charAt(j) != sep)
2b3076cfd6dd slightly more general Library.chunks;
wenzelm
parents: 34317
diff changeset
    71
        Some((source.subSequence(i + 1, j), j))
2b3076cfd6dd slightly more general Library.chunks;
wenzelm
parents: 34317
diff changeset
    72
      }
2b3076cfd6dd slightly more general Library.chunks;
wenzelm
parents: 34317
diff changeset
    73
      else None
2b3076cfd6dd slightly more general Library.chunks;
wenzelm
parents: 34317
diff changeset
    74
    }
2b3076cfd6dd slightly more general Library.chunks;
wenzelm
parents: 34317
diff changeset
    75
    private var state: Option[(CharSequence, Int)] = if (end == 0) None else next_chunk(-1)
2b3076cfd6dd slightly more general Library.chunks;
wenzelm
parents: 34317
diff changeset
    76
2b3076cfd6dd slightly more general Library.chunks;
wenzelm
parents: 34317
diff changeset
    77
    def hasNext(): Boolean = state.isDefined
2b3076cfd6dd slightly more general Library.chunks;
wenzelm
parents: 34317
diff changeset
    78
    def next(): CharSequence =
2b3076cfd6dd slightly more general Library.chunks;
wenzelm
parents: 34317
diff changeset
    79
      state match {
2b3076cfd6dd slightly more general Library.chunks;
wenzelm
parents: 34317
diff changeset
    80
        case Some((s, i)) => { state = next_chunk(i); s }
38583
wenzelm
parents: 38258
diff changeset
    81
        case None => Iterator.empty.next()
36685
2b3076cfd6dd slightly more general Library.chunks;
wenzelm
parents: 34317
diff changeset
    82
      }
2b3076cfd6dd slightly more general Library.chunks;
wenzelm
parents: 34317
diff changeset
    83
  }
2b3076cfd6dd slightly more general Library.chunks;
wenzelm
parents: 34317
diff changeset
    84
40475
8a57ff2c2600 Sidekick block asset: show first line only;
wenzelm
parents: 38636
diff changeset
    85
  def first_line(source: CharSequence): String =
8a57ff2c2600 Sidekick block asset: show first line only;
wenzelm
parents: 38636
diff changeset
    86
  {
8a57ff2c2600 Sidekick block asset: show first line only;
wenzelm
parents: 38636
diff changeset
    87
    val lines = chunks(source)
8a57ff2c2600 Sidekick block asset: show first line only;
wenzelm
parents: 38636
diff changeset
    88
    if (lines.hasNext) lines.next.toString
8a57ff2c2600 Sidekick block asset: show first line only;
wenzelm
parents: 38636
diff changeset
    89
    else ""
8a57ff2c2600 Sidekick block asset: show first line only;
wenzelm
parents: 38636
diff changeset
    90
  }
8a57ff2c2600 Sidekick block asset: show first line only;
wenzelm
parents: 38636
diff changeset
    91
36685
2b3076cfd6dd slightly more general Library.chunks;
wenzelm
parents: 34317
diff changeset
    92
34216
ada8eb23a08e added simple dialogs;
wenzelm
parents: 34198
diff changeset
    93
  /* simple dialogs */
ada8eb23a08e added simple dialogs;
wenzelm
parents: 34198
diff changeset
    94
ada8eb23a08e added simple dialogs;
wenzelm
parents: 34198
diff changeset
    95
  private def simple_dialog(kind: Int, default_title: String)
ada8eb23a08e added simple dialogs;
wenzelm
parents: 34198
diff changeset
    96
    (parent: Component, title: String, message: Any*)
ada8eb23a08e added simple dialogs;
wenzelm
parents: 34198
diff changeset
    97
  {
36791
b8384c455b40 simple dialogs: ensure Swing thread;
wenzelm
parents: 36688
diff changeset
    98
    Swing_Thread.now {
38232
00b72526dc64 simple_dialog: allow scala.swing.Component as well;
wenzelm
parents: 37686
diff changeset
    99
      val java_message = message map { case x: scala.swing.Component => x.peer case x => x }
36791
b8384c455b40 simple dialogs: ensure Swing thread;
wenzelm
parents: 36688
diff changeset
   100
      JOptionPane.showMessageDialog(parent,
38232
00b72526dc64 simple_dialog: allow scala.swing.Component as well;
wenzelm
parents: 37686
diff changeset
   101
        java_message.toArray.asInstanceOf[Array[AnyRef]],
36791
b8384c455b40 simple dialogs: ensure Swing thread;
wenzelm
parents: 36688
diff changeset
   102
        if (title == null) default_title else title, kind)
b8384c455b40 simple dialogs: ensure Swing thread;
wenzelm
parents: 36688
diff changeset
   103
    }
34216
ada8eb23a08e added simple dialogs;
wenzelm
parents: 34198
diff changeset
   104
  }
ada8eb23a08e added simple dialogs;
wenzelm
parents: 34198
diff changeset
   105
ada8eb23a08e added simple dialogs;
wenzelm
parents: 34198
diff changeset
   106
  def dialog = simple_dialog(JOptionPane.PLAIN_MESSAGE, null) _
ada8eb23a08e added simple dialogs;
wenzelm
parents: 34198
diff changeset
   107
  def warning_dialog = simple_dialog(JOptionPane.WARNING_MESSAGE, "Warning") _
ada8eb23a08e added simple dialogs;
wenzelm
parents: 34198
diff changeset
   108
  def error_dialog = simple_dialog(JOptionPane.ERROR_MESSAGE, "Error") _
ada8eb23a08e added simple dialogs;
wenzelm
parents: 34198
diff changeset
   109
ada8eb23a08e added simple dialogs;
wenzelm
parents: 34198
diff changeset
   110
37018
39f4cce5a22c added somewhat generic zoom box;
wenzelm
parents: 36791
diff changeset
   111
  /* zoom box */
39f4cce5a22c added somewhat generic zoom box;
wenzelm
parents: 36791
diff changeset
   112
37048
d014976dd690 tuned zoom_box;
wenzelm
parents: 37035
diff changeset
   113
  class Zoom_Box(apply_factor: Int => Unit) extends ComboBox[String](
d014976dd690 tuned zoom_box;
wenzelm
parents: 37035
diff changeset
   114
    List("50%", "70%", "85%", "100%", "125%", "150%", "175%", "200%", "300%", "400%"))
d014976dd690 tuned zoom_box;
wenzelm
parents: 37035
diff changeset
   115
  {
d014976dd690 tuned zoom_box;
wenzelm
parents: 37035
diff changeset
   116
    val Factor = "([0-9]+)%?"r
d014976dd690 tuned zoom_box;
wenzelm
parents: 37035
diff changeset
   117
    def parse(text: String): Int =
d014976dd690 tuned zoom_box;
wenzelm
parents: 37035
diff changeset
   118
      text match {
d014976dd690 tuned zoom_box;
wenzelm
parents: 37035
diff changeset
   119
        case Factor(s) =>
d014976dd690 tuned zoom_box;
wenzelm
parents: 37035
diff changeset
   120
          val i = Integer.parseInt(s)
d014976dd690 tuned zoom_box;
wenzelm
parents: 37035
diff changeset
   121
          if (10 <= i && i <= 1000) i else 100
d014976dd690 tuned zoom_box;
wenzelm
parents: 37035
diff changeset
   122
        case _ => 100
d014976dd690 tuned zoom_box;
wenzelm
parents: 37035
diff changeset
   123
      }
d014976dd690 tuned zoom_box;
wenzelm
parents: 37035
diff changeset
   124
    def print(i: Int): String = i.toString + "%"
37018
39f4cce5a22c added somewhat generic zoom box;
wenzelm
parents: 36791
diff changeset
   125
37048
d014976dd690 tuned zoom_box;
wenzelm
parents: 37035
diff changeset
   126
    makeEditable()(c => new ComboBox.BuiltInEditor(c)(text => print(parse(text)), x => x))
d014976dd690 tuned zoom_box;
wenzelm
parents: 37035
diff changeset
   127
    reactions += {
d014976dd690 tuned zoom_box;
wenzelm
parents: 37035
diff changeset
   128
      case SelectionChanged(_) => apply_factor(parse(selection.item))
37018
39f4cce5a22c added somewhat generic zoom box;
wenzelm
parents: 36791
diff changeset
   129
    }
37048
d014976dd690 tuned zoom_box;
wenzelm
parents: 37035
diff changeset
   130
    listenTo(selection)
d014976dd690 tuned zoom_box;
wenzelm
parents: 37035
diff changeset
   131
    selection.index = 3
d014976dd690 tuned zoom_box;
wenzelm
parents: 37035
diff changeset
   132
    prototypeDisplayValue = Some("00000%")
d014976dd690 tuned zoom_box;
wenzelm
parents: 37035
diff changeset
   133
  }
37018
39f4cce5a22c added somewhat generic zoom box;
wenzelm
parents: 36791
diff changeset
   134
39f4cce5a22c added somewhat generic zoom box;
wenzelm
parents: 36791
diff changeset
   135
34136
3dcb46ae6185 added basic library -- Scala version;
wenzelm
parents:
diff changeset
   136
  /* timing */
3dcb46ae6185 added basic library -- Scala version;
wenzelm
parents:
diff changeset
   137
34314
f799f3749596 timeit message;
wenzelm
parents: 34216
diff changeset
   138
  def timeit[A](message: String)(e: => A) =
34136
3dcb46ae6185 added basic library -- Scala version;
wenzelm
parents:
diff changeset
   139
  {
40848
8662b9b1f123 more abstract/uniform handling of time, preferring seconds as Double;
wenzelm
parents: 40475
diff changeset
   140
    val start = System.currentTimeMillis()
34136
3dcb46ae6185 added basic library -- Scala version;
wenzelm
parents:
diff changeset
   141
    val result = Exn.capture(e)
40848
8662b9b1f123 more abstract/uniform handling of time, preferring seconds as Double;
wenzelm
parents: 40475
diff changeset
   142
    val stop = System.currentTimeMillis()
34314
f799f3749596 timeit message;
wenzelm
parents: 34216
diff changeset
   143
    System.err.println(
37686
bb27d99a9a69 more precise timing;
wenzelm
parents: 37048
diff changeset
   144
      (if (message == null || message.isEmpty) "" else message + ": ") +
40848
8662b9b1f123 more abstract/uniform handling of time, preferring seconds as Double;
wenzelm
parents: 40475
diff changeset
   145
        new Time(stop - start).message + " elapsed time")
34136
3dcb46ae6185 added basic library -- Scala version;
wenzelm
parents:
diff changeset
   146
    Exn.release(result)
3dcb46ae6185 added basic library -- Scala version;
wenzelm
parents:
diff changeset
   147
  }
3dcb46ae6185 added basic library -- Scala version;
wenzelm
parents:
diff changeset
   148
}