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