pervasive Basic_Library in Scala;
authorwenzelm
Mon Jul 04 16:51:45 2011 +0200 (2011-07-04)
changeset 43652dcd0b667f73d
parent 43651 511df47bcadc
child 43659 67d82d94a076
pervasive Basic_Library in Scala;
tuned;
src/Pure/General/path.scala
src/Pure/System/session.scala
src/Pure/Thy/thy_header.scala
src/Pure/Thy/thy_info.scala
src/Pure/library.ML
src/Pure/library.scala
src/Pure/package.scala
     1.1 --- a/src/Pure/General/path.scala	Mon Jul 04 16:27:11 2011 +0200
     1.2 +++ b/src/Pure/General/path.scala	Mon Jul 04 16:51:45 2011 +0200
     1.3 @@ -19,7 +19,7 @@
     1.4    private case object Parent extends Elem
     1.5  
     1.6    private def err_elem(msg: String, s: String): Nothing =
     1.7 -    error (msg + " path element specification: " + Library.quote(s))
     1.8 +    error (msg + " path element specification: " + quote(s))
     1.9  
    1.10    private def check_elem(s: String): String =
    1.11      if (s == "" || s == "~" || s == "~~") err_elem("Illegal", s)
    1.12 @@ -27,7 +27,7 @@
    1.13        s.iterator.filter(c => c == '/' || c == '\\' || c == '$' || c == ':').toList match {
    1.14          case Nil => s
    1.15          case bads =>
    1.16 -          err_elem ("Illegal character(s) " + Library.commas_quote(bads.map(_.toString)) + " in", s)
    1.17 +          err_elem ("Illegal character(s) " + commas_quote(bads.map(_.toString)) + " in", s)
    1.18        }
    1.19  
    1.20    private def root_elem(s: String): Elem = Root(check_elem(s))
    1.21 @@ -114,7 +114,7 @@
    1.22        case _ => elems.map(Path.implode_elem).reverse.mkString("/")
    1.23      }
    1.24  
    1.25 -  override def toString: String = Library.quote(implode)
    1.26 +  override def toString: String = quote(implode)
    1.27  
    1.28  
    1.29    /* base element */
     2.1 --- a/src/Pure/System/session.scala	Mon Jul 04 16:27:11 2011 +0200
     2.2 +++ b/src/Pure/System/session.scala	Mon Jul 04 16:51:45 2011 +0200
     2.3 @@ -154,7 +154,7 @@
     2.4      override def check_thy(dir: Path, name: String): (String, Thy_Header.Header) =
     2.5      {
     2.6        val file = system.platform_file(dir + Thy_Header.thy_path(name))
     2.7 -      if (!file.exists || !file.isFile) error("No such file: " + Library.quote(file.toString))
     2.8 +      if (!file.exists || !file.isFile) error("No such file: " + quote(file.toString))
     2.9        val text = Standard_System.read_file(file)
    2.10        val header = thy_header.read(text)
    2.11        (text, header)
     3.1 --- a/src/Pure/Thy/thy_header.scala	Mon Jul 04 16:27:11 2011 +0200
     3.2 +++ b/src/Pure/Thy/thy_header.scala	Mon Jul 04 16:51:45 2011 +0200
     3.3 @@ -119,6 +119,6 @@
     3.4      val header = read(source)
     3.5      val name1 = header.name
     3.6      if (name == name1) header
     3.7 -    else error("Bad file name " + Thy_Header.thy_path(name) + " for theory " + Library.quote(name1))
     3.8 +    else error("Bad file name " + Thy_Header.thy_path(name) + " for theory " + quote(name1))
     3.9    }
    3.10  }
     4.1 --- a/src/Pure/Thy/thy_info.scala	Mon Jul 04 16:27:11 2011 +0200
     4.2 +++ b/src/Pure/Thy/thy_info.scala	Mon Jul 04 16:51:45 2011 +0200
     4.3 @@ -12,7 +12,7 @@
     4.4    /* messages */
     4.5  
     4.6    private def show_path(names: List[String]): String =
     4.7 -    names.map(Library.quote).mkString(" via ")
     4.8 +    names.map(quote).mkString(" via ")
     4.9  
    4.10    private def cycle_msg(names: List[String]): String =
    4.11      "Cyclic dependency of " + show_path(names)
    4.12 @@ -45,7 +45,7 @@
    4.13            catch {
    4.14              case ERROR(msg) =>
    4.15                cat_error(msg, "The error(s) above occurred while examining theory " +
    4.16 -                Library.quote(name) + required_by("\n", initiators))
    4.17 +                quote(name) + required_by("\n", initiators))
    4.18            }
    4.19          require_thys(name :: initiators, dir1,
    4.20            deps + (name -> Exn.Res(text, header)), header.imports)
     5.1 --- a/src/Pure/library.ML	Mon Jul 04 16:27:11 2011 +0200
     5.2 +++ b/src/Pure/library.ML	Mon Jul 04 16:51:45 2011 +0200
     5.3 @@ -28,7 +28,7 @@
     5.4    val funpow: int -> ('a -> 'a) -> 'a -> 'a
     5.5    val funpow_yield: int -> ('a -> 'b * 'a) -> 'a -> 'b list * 'a
     5.6  
     5.7 -  (*errors*)
     5.8 +  (*user errors*)
     5.9    exception ERROR of string
    5.10    val error: string -> 'a
    5.11    val cat_error: string -> string -> 'a
    5.12 @@ -260,7 +260,7 @@
    5.13    | funpow_yield n f x = x |> f ||>> funpow_yield (n - 1) f |>> op ::;
    5.14  
    5.15  
    5.16 -(* errors *)
    5.17 +(* user errors *)
    5.18  
    5.19  exception ERROR of string;
    5.20  fun error msg = raise ERROR msg;
     6.1 --- a/src/Pure/library.scala	Mon Jul 04 16:27:11 2011 +0200
     6.2 +++ b/src/Pure/library.scala	Mon Jul 04 16:51:45 2011 +0200
     6.3 @@ -18,6 +18,27 @@
     6.4  
     6.5  object Library
     6.6  {
     6.7 +  /* user errors */
     6.8 +
     6.9 +  object ERROR
    6.10 +  {
    6.11 +    def apply(message: String): Throwable = new RuntimeException(message)
    6.12 +    def unapply(exn: Throwable): Option[String] =
    6.13 +      exn match {
    6.14 +        case e: RuntimeException =>
    6.15 +          val msg = e.getMessage
    6.16 +          Some(if (msg == null) "" else msg)
    6.17 +        case _ => None
    6.18 +      }
    6.19 +  }
    6.20 +
    6.21 +  def error(message: String): Nothing = throw ERROR(message)
    6.22 +
    6.23 +  def cat_error(msg1: String, msg2: String): Nothing =
    6.24 +    if (msg1 == "") error(msg1)
    6.25 +    else error(msg1 + "\n" + msg2)
    6.26 +
    6.27 +
    6.28    /* lists */
    6.29  
    6.30    def separate[A](s: A, list: List[A]): List[A] =
    6.31 @@ -41,6 +62,37 @@
    6.32      }
    6.33  
    6.34  
    6.35 +  /* iterate over chunks (cf. space_explode) */
    6.36 +
    6.37 +  def chunks(source: CharSequence, sep: Char = '\n') = new Iterator[CharSequence]
    6.38 +  {
    6.39 +    private val end = source.length
    6.40 +    private def next_chunk(i: Int): Option[(CharSequence, Int)] =
    6.41 +    {
    6.42 +      if (i < end) {
    6.43 +        var j = i; do j += 1 while (j < end && source.charAt(j) != sep)
    6.44 +        Some((source.subSequence(i + 1, j), j))
    6.45 +      }
    6.46 +      else None
    6.47 +    }
    6.48 +    private var state: Option[(CharSequence, Int)] = if (end == 0) None else next_chunk(-1)
    6.49 +
    6.50 +    def hasNext(): Boolean = state.isDefined
    6.51 +    def next(): CharSequence =
    6.52 +      state match {
    6.53 +        case Some((s, i)) => { state = next_chunk(i); s }
    6.54 +        case None => Iterator.empty.next()
    6.55 +      }
    6.56 +  }
    6.57 +
    6.58 +  def first_line(source: CharSequence): String =
    6.59 +  {
    6.60 +    val lines = chunks(source)
    6.61 +    if (lines.hasNext) lines.next.toString
    6.62 +    else ""
    6.63 +  }
    6.64 +
    6.65 +
    6.66    /* strings */
    6.67  
    6.68    def quote(s: String): String = "\"" + s + "\""
    6.69 @@ -73,37 +125,6 @@
    6.70    }
    6.71  
    6.72  
    6.73 -  /* iterate over chunks (cf. space_explode/split_lines in ML) */
    6.74 -
    6.75 -  def chunks(source: CharSequence, sep: Char = '\n') = new Iterator[CharSequence]
    6.76 -  {
    6.77 -    private val end = source.length
    6.78 -    private def next_chunk(i: Int): Option[(CharSequence, Int)] =
    6.79 -    {
    6.80 -      if (i < end) {
    6.81 -        var j = i; do j += 1 while (j < end && source.charAt(j) != sep)
    6.82 -        Some((source.subSequence(i + 1, j), j))
    6.83 -      }
    6.84 -      else None
    6.85 -    }
    6.86 -    private var state: Option[(CharSequence, Int)] = if (end == 0) None else next_chunk(-1)
    6.87 -
    6.88 -    def hasNext(): Boolean = state.isDefined
    6.89 -    def next(): CharSequence =
    6.90 -      state match {
    6.91 -        case Some((s, i)) => { state = next_chunk(i); s }
    6.92 -        case None => Iterator.empty.next()
    6.93 -      }
    6.94 -  }
    6.95 -
    6.96 -  def first_line(source: CharSequence): String =
    6.97 -  {
    6.98 -    val lines = chunks(source)
    6.99 -    if (lines.hasNext) lines.next.toString
   6.100 -    else ""
   6.101 -  }
   6.102 -
   6.103 -
   6.104    /* simple dialogs */
   6.105  
   6.106    private def simple_dialog(kind: Int, default_title: String)
   6.107 @@ -160,3 +181,17 @@
   6.108      Exn.release(result)
   6.109    }
   6.110  }
   6.111 +
   6.112 +
   6.113 +class Basic_Library
   6.114 +{
   6.115 +  val space_explode = Library.space_explode _
   6.116 +
   6.117 +  val quote = Library.quote _
   6.118 +  val commas = Library.commas _
   6.119 +  val commas_quote = Library.commas_quote _
   6.120 +
   6.121 +  val ERROR = Library.ERROR
   6.122 +  val error = Library.error _
   6.123 +  val cat_error = Library.cat_error _
   6.124 +}
     7.1 --- a/src/Pure/package.scala	Mon Jul 04 16:27:11 2011 +0200
     7.2 +++ b/src/Pure/package.scala	Mon Jul 04 16:51:45 2011 +0200
     7.3 @@ -4,26 +4,7 @@
     7.4  Toplevel isabelle package.
     7.5  */
     7.6  
     7.7 -package object isabelle
     7.8 +package object isabelle extends isabelle.Basic_Library
     7.9  {
    7.10 -  /* errors */
    7.11 -
    7.12 -  object ERROR
    7.13 -  {
    7.14 -    def apply(message: String): Throwable = new RuntimeException(message)
    7.15 -    def unapply(exn: Throwable): Option[String] =
    7.16 -      exn match {
    7.17 -        case e: RuntimeException =>
    7.18 -          val msg = e.getMessage
    7.19 -          Some(if (msg == null) "" else msg)
    7.20 -        case _ => None
    7.21 -      }
    7.22 -  }
    7.23 -
    7.24 -  def error(message: String): Nothing = throw ERROR(message)
    7.25 -
    7.26 -  def cat_error(msg1: String, msg2: String): Nothing =
    7.27 -    if (msg1 == "") error(msg1)
    7.28 -    else error(msg1 + "\n" + msg2)
    7.29  }
    7.30