src/Pure/library.scala
author wenzelm
Thu Aug 02 12:36:54 2012 +0200 (2012-08-02)
changeset 48646 91281e9472d8
parent 48479 819f7a5f3e7f
child 48996 a8bad1369ada
permissions -rw-r--r--
more official command specifications, including source position;
wenzelm@34136
     1
/*  Title:      Pure/library.scala
wenzelm@45673
     2
    Module:     PIDE
wenzelm@34136
     3
    Author:     Makarius
wenzelm@34136
     4
wenzelm@34136
     5
Basic library.
wenzelm@34136
     6
*/
wenzelm@34136
     7
wenzelm@34136
     8
package isabelle
wenzelm@34136
     9
wenzelm@38258
    10
wenzelm@38636
    11
import java.lang.System
wenzelm@34216
    12
import java.awt.Component
wenzelm@34216
    13
import javax.swing.JOptionPane
wenzelm@34136
    14
wenzelm@47867
    15
import scala.swing.{ComboBox, TextArea, ScrollPane}
wenzelm@37018
    16
import scala.swing.event.SelectionChanged
wenzelm@43598
    17
import scala.collection.mutable
wenzelm@37018
    18
wenzelm@37018
    19
wenzelm@34136
    20
object Library
wenzelm@34136
    21
{
wenzelm@43652
    22
  /* user errors */
wenzelm@43652
    23
wenzelm@43652
    24
  object ERROR
wenzelm@43652
    25
  {
wenzelm@43652
    26
    def apply(message: String): Throwable = new RuntimeException(message)
wenzelm@48479
    27
    def unapply(exn: Throwable): Option[String] = Exn.user_message(exn)
wenzelm@43652
    28
  }
wenzelm@43652
    29
wenzelm@43652
    30
  def error(message: String): Nothing = throw ERROR(message)
wenzelm@43652
    31
wenzelm@43652
    32
  def cat_error(msg1: String, msg2: String): Nothing =
wenzelm@43652
    33
    if (msg1 == "") error(msg1)
wenzelm@43652
    34
    else error(msg1 + "\n" + msg2)
wenzelm@43652
    35
wenzelm@43652
    36
wenzelm@43598
    37
  /* lists */
wenzelm@36688
    38
wenzelm@36688
    39
  def separate[A](s: A, list: List[A]): List[A] =
wenzelm@36688
    40
    list match {
wenzelm@36688
    41
      case x :: xs if !xs.isEmpty => x :: s :: separate(s, xs)
wenzelm@36688
    42
      case _ => list
wenzelm@36688
    43
    }
wenzelm@36688
    44
wenzelm@43598
    45
  def space_explode(sep: Char, str: String): List[String] =
wenzelm@43598
    46
    if (str.isEmpty) Nil
wenzelm@43598
    47
    else {
wenzelm@43598
    48
      val result = new mutable.ListBuffer[String]
wenzelm@43598
    49
      var start = 0
wenzelm@43598
    50
      var finished = false
wenzelm@43598
    51
      while (!finished) {
wenzelm@43598
    52
        val i = str.indexOf(sep, start)
wenzelm@43598
    53
        if (i == -1) { result += str.substring(start); finished = true }
wenzelm@43598
    54
        else { result += str.substring(start, i); start = i + 1 }
wenzelm@43598
    55
      }
wenzelm@43598
    56
      result.toList
wenzelm@43598
    57
    }
wenzelm@43598
    58
wenzelm@43670
    59
  def split_lines(str: String): List[String] = space_explode('\n', str)
wenzelm@43670
    60
wenzelm@48425
    61
  def trim_line(str: String): String =
wenzelm@48425
    62
    if (str.endsWith("\n")) str.substring(0, str.length - 1)
wenzelm@48425
    63
    else str
wenzelm@48425
    64
wenzelm@43598
    65
wenzelm@43652
    66
  /* iterate over chunks (cf. space_explode) */
wenzelm@43652
    67
wenzelm@43652
    68
  def chunks(source: CharSequence, sep: Char = '\n') = new Iterator[CharSequence]
wenzelm@43652
    69
  {
wenzelm@43652
    70
    private val end = source.length
wenzelm@43652
    71
    private def next_chunk(i: Int): Option[(CharSequence, Int)] =
wenzelm@43652
    72
    {
wenzelm@43652
    73
      if (i < end) {
wenzelm@43652
    74
        var j = i; do j += 1 while (j < end && source.charAt(j) != sep)
wenzelm@43652
    75
        Some((source.subSequence(i + 1, j), j))
wenzelm@43652
    76
      }
wenzelm@43652
    77
      else None
wenzelm@43652
    78
    }
wenzelm@43652
    79
    private var state: Option[(CharSequence, Int)] = if (end == 0) None else next_chunk(-1)
wenzelm@43652
    80
wenzelm@43652
    81
    def hasNext(): Boolean = state.isDefined
wenzelm@43652
    82
    def next(): CharSequence =
wenzelm@43652
    83
      state match {
wenzelm@43652
    84
        case Some((s, i)) => { state = next_chunk(i); s }
wenzelm@43652
    85
        case None => Iterator.empty.next()
wenzelm@43652
    86
      }
wenzelm@43652
    87
  }
wenzelm@43652
    88
wenzelm@43652
    89
  def first_line(source: CharSequence): String =
wenzelm@43652
    90
  {
wenzelm@43652
    91
    val lines = chunks(source)
wenzelm@43652
    92
    if (lines.hasNext) lines.next.toString
wenzelm@43652
    93
    else ""
wenzelm@43652
    94
  }
wenzelm@43652
    95
wenzelm@43652
    96
wenzelm@43598
    97
  /* strings */
wenzelm@43598
    98
wenzelm@46196
    99
  def cat_lines(lines: TraversableOnce[String]): String = lines.mkString("\n")
wenzelm@46196
   100
wenzelm@43598
   101
  def quote(s: String): String = "\"" + s + "\""
wenzelm@43598
   102
  def commas(ss: Iterable[String]): String = ss.iterator.mkString(", ")
wenzelm@48362
   103
  def commas_quote(ss: Iterable[String]): String = ss.iterator.map(quote).mkString(", ")
wenzelm@43598
   104
wenzelm@36688
   105
wenzelm@34141
   106
  /* reverse CharSequence */
wenzelm@34141
   107
wenzelm@34141
   108
  class Reverse(text: CharSequence, start: Int, end: Int) extends CharSequence
wenzelm@34141
   109
  {
wenzelm@34141
   110
    require(0 <= start && start <= end && end <= text.length)
wenzelm@34141
   111
wenzelm@34141
   112
    def this(text: CharSequence) = this(text, 0, text.length)
wenzelm@34141
   113
wenzelm@34141
   114
    def length: Int = end - start
wenzelm@34141
   115
    def charAt(i: Int): Char = text.charAt(end - i - 1)
wenzelm@34141
   116
wenzelm@34141
   117
    def subSequence(i: Int, j: Int): CharSequence =
wenzelm@34141
   118
      if (0 <= i && i <= j && j <= length) new Reverse(text, end - j, end - i)
wenzelm@34141
   119
      else throw new IndexOutOfBoundsException
wenzelm@34141
   120
wenzelm@34141
   121
    override def toString: String =
wenzelm@34141
   122
    {
wenzelm@34141
   123
      val buf = new StringBuilder(length)
wenzelm@34141
   124
      for (i <- 0 until length)
wenzelm@34141
   125
        buf.append(charAt(i))
wenzelm@34141
   126
      buf.toString
wenzelm@34141
   127
    }
wenzelm@34141
   128
  }
wenzelm@34141
   129
wenzelm@34141
   130
wenzelm@34216
   131
  /* simple dialogs */
wenzelm@34216
   132
wenzelm@48345
   133
  def scrollable_text(txt: String, width: Int = 80, editable: Boolean = false): ScrollPane =
wenzelm@47867
   134
  {
wenzelm@47867
   135
    val text = new TextArea(txt)
wenzelm@47867
   136
    if (width > 0) text.columns = width
wenzelm@47867
   137
    text.editable = editable
wenzelm@47867
   138
    new ScrollPane(text)
wenzelm@47867
   139
  }
wenzelm@47867
   140
wenzelm@46997
   141
  private def simple_dialog(kind: Int, default_title: String,
wenzelm@46997
   142
    parent: Component, title: String, message: Seq[Any])
wenzelm@34216
   143
  {
wenzelm@36791
   144
    Swing_Thread.now {
wenzelm@38232
   145
      val java_message = message map { case x: scala.swing.Component => x.peer case x => x }
wenzelm@36791
   146
      JOptionPane.showMessageDialog(parent,
wenzelm@38232
   147
        java_message.toArray.asInstanceOf[Array[AnyRef]],
wenzelm@36791
   148
        if (title == null) default_title else title, kind)
wenzelm@36791
   149
    }
wenzelm@34216
   150
  }
wenzelm@34216
   151
wenzelm@46997
   152
  def dialog(parent: Component, title: String, message: Any*) =
wenzelm@46997
   153
    simple_dialog(JOptionPane.PLAIN_MESSAGE, null, parent, title, message)
wenzelm@46997
   154
wenzelm@46997
   155
  def warning_dialog(parent: Component, title: String, message: Any*) =
wenzelm@46997
   156
    simple_dialog(JOptionPane.WARNING_MESSAGE, "Warning", parent, title, message)
wenzelm@46997
   157
wenzelm@46997
   158
  def error_dialog(parent: Component, title: String, message: Any*) =
wenzelm@46997
   159
    simple_dialog(JOptionPane.ERROR_MESSAGE, "Error", parent, title, message)
wenzelm@34216
   160
wenzelm@44573
   161
  def confirm_dialog(parent: Component, title: String, option_type: Int, message: Any*): Int =
wenzelm@44573
   162
    Swing_Thread.now {
wenzelm@44573
   163
      val java_message = message map { case x: scala.swing.Component => x.peer case x => x }
wenzelm@44573
   164
      JOptionPane.showConfirmDialog(parent,
wenzelm@44573
   165
        java_message.toArray.asInstanceOf[Array[AnyRef]], title,
wenzelm@44573
   166
          option_type, JOptionPane.QUESTION_MESSAGE)
wenzelm@44573
   167
    }
wenzelm@44573
   168
wenzelm@34216
   169
wenzelm@37018
   170
  /* zoom box */
wenzelm@37018
   171
wenzelm@37048
   172
  class Zoom_Box(apply_factor: Int => Unit) extends ComboBox[String](
wenzelm@37048
   173
    List("50%", "70%", "85%", "100%", "125%", "150%", "175%", "200%", "300%", "400%"))
wenzelm@37048
   174
  {
wenzelm@47993
   175
    val Factor = "([0-9]+)%?".r
wenzelm@37048
   176
    def parse(text: String): Int =
wenzelm@37048
   177
      text match {
wenzelm@37048
   178
        case Factor(s) =>
wenzelm@37048
   179
          val i = Integer.parseInt(s)
wenzelm@37048
   180
          if (10 <= i && i <= 1000) i else 100
wenzelm@37048
   181
        case _ => 100
wenzelm@37048
   182
      }
wenzelm@37048
   183
    def print(i: Int): String = i.toString + "%"
wenzelm@37018
   184
wenzelm@37048
   185
    makeEditable()(c => new ComboBox.BuiltInEditor(c)(text => print(parse(text)), x => x))
wenzelm@37048
   186
    reactions += {
wenzelm@37048
   187
      case SelectionChanged(_) => apply_factor(parse(selection.item))
wenzelm@37018
   188
    }
wenzelm@37048
   189
    listenTo(selection)
wenzelm@37048
   190
    selection.index = 3
wenzelm@37048
   191
    prototypeDisplayValue = Some("00000%")
wenzelm@37048
   192
  }
wenzelm@34136
   193
}
wenzelm@43652
   194
wenzelm@43652
   195
wenzelm@43652
   196
class Basic_Library
wenzelm@43652
   197
{
wenzelm@43670
   198
  val ERROR = Library.ERROR
wenzelm@43670
   199
  val error = Library.error _
wenzelm@43670
   200
  val cat_error = Library.cat_error _
wenzelm@43670
   201
wenzelm@43652
   202
  val space_explode = Library.space_explode _
wenzelm@43670
   203
  val split_lines = Library.split_lines _
wenzelm@46196
   204
  val cat_lines = Library.cat_lines _
wenzelm@43652
   205
  val quote = Library.quote _
wenzelm@43652
   206
  val commas = Library.commas _
wenzelm@43652
   207
  val commas_quote = Library.commas_quote _
wenzelm@43652
   208
}