src/Pure/ROOT.scala
author wenzelm
Mon, 05 Feb 2024 12:59:34 +0100
changeset 79578 4c4d71b00001
parent 79528 667cb8b79909
child 79749 a861b0df74b4
permissions -rw-r--r--
tuned README;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
57647
5c600dd17617 clarified file names;
wenzelm
parents: 45673
diff changeset
     1
/*  Title:      Pure/ROOT.scala
42720
caa4f1279154 added toplevel isabelle package -- reduce warnings with scala-2.9.0.final;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
caa4f1279154 added toplevel isabelle package -- reduce warnings with scala-2.9.0.final;
wenzelm
parents:
diff changeset
     3
57647
5c600dd17617 clarified file names;
wenzelm
parents: 45673
diff changeset
     4
Root of isabelle package.
42720
caa4f1279154 added toplevel isabelle package -- reduce warnings with scala-2.9.0.final;
wenzelm
parents:
diff changeset
     5
*/
caa4f1279154 added toplevel isabelle package -- reduce warnings with scala-2.9.0.final;
wenzelm
parents:
diff changeset
     6
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75295
diff changeset
     7
package object isabelle {
62492
0e53fade87fe clarified modules;
wenzelm
parents: 57649
diff changeset
     8
  val ERROR = Exn.ERROR
0e53fade87fe clarified modules;
wenzelm
parents: 57649
diff changeset
     9
  val error = Exn.error _
68131
62a3294edda3 tuned signature;
wenzelm
parents: 67885
diff changeset
    10
  def cat_error(msgs: String*): Nothing = Exn.cat_error(msgs:_*)
62492
0e53fade87fe clarified modules;
wenzelm
parents: 57649
diff changeset
    11
77515
6aae7486e94a more operations;
wenzelm
parents: 77367
diff changeset
    12
  def using[A <: AutoCloseable, B](a: A)(f: A => B): B =
6aae7486e94a more operations;
wenzelm
parents: 77367
diff changeset
    13
    Library.using(a)(f)
6aae7486e94a more operations;
wenzelm
parents: 77367
diff changeset
    14
  def using_option[A <: AutoCloseable, B](opt: Option[A])(f: A => B): Option[B] =
6aae7486e94a more operations;
wenzelm
parents: 77367
diff changeset
    15
    Library.using_option(opt)(f)
78198
c268def0784b clarified signature: prefer explicit combinator;
wenzelm
parents: 78126
diff changeset
    16
  def using_optional[A <: AutoCloseable, B](opt: Option[A])(f: Option[A] => B): B =
c268def0784b clarified signature: prefer explicit combinator;
wenzelm
parents: 78126
diff changeset
    17
    Library.using_optional(opt)(f)
77515
6aae7486e94a more operations;
wenzelm
parents: 77367
diff changeset
    18
62492
0e53fade87fe clarified modules;
wenzelm
parents: 57649
diff changeset
    19
  val space_explode = Library.space_explode _
0e53fade87fe clarified modules;
wenzelm
parents: 57649
diff changeset
    20
  val split_lines = Library.split_lines _
0e53fade87fe clarified modules;
wenzelm
parents: 57649
diff changeset
    21
  val cat_lines = Library.cat_lines _
64173
85ff21510ba9 tuned signature;
wenzelm
parents: 63789
diff changeset
    22
  val terminate_lines = Library.terminate_lines _
62492
0e53fade87fe clarified modules;
wenzelm
parents: 57649
diff changeset
    23
  val quote = Library.quote _
0e53fade87fe clarified modules;
wenzelm
parents: 57649
diff changeset
    24
  val commas = Library.commas _
0e53fade87fe clarified modules;
wenzelm
parents: 57649
diff changeset
    25
  val commas_quote = Library.commas_quote _
75295
38398766be6b command-line arguments for "isabelle vscode", similar to "isabelle jedit";
wenzelm
parents: 74356
diff changeset
    26
  val proper_bool = Library.proper_bool _
65712
ddd6dfc28e80 more operations;
wenzelm
parents: 64370
diff changeset
    27
  val proper_string = Library.proper_string _
65761
ce909161d030 more operations;
wenzelm
parents: 65715
diff changeset
    28
  def proper_list[A](list: List[A]): Option[List[A]] = Library.proper_list(list)
77367
d27d1224c67f more operations;
wenzelm
parents: 77108
diff changeset
    29
  def if_proper[A](x: Iterable[A], body: => String): String = Library.if_proper(x, body)
77614
b619d80f61fa clarified signature;
wenzelm
parents: 77515
diff changeset
    30
  def if_proper(b: Boolean, body: => String): String = Library.if_proper(b, body)
42720
caa4f1279154 added toplevel isabelle package -- reduce warnings with scala-2.9.0.final;
wenzelm
parents:
diff changeset
    31
}
79528
667cb8b79909 update to jdk-21.0.2;
wenzelm
parents: 79508
diff changeset
    32