diff --git a/src/Pure/System/isabelle_system.scala b/src/Pure/System/isabelle_system.scala --- a/src/Pure/System/isabelle_system.scala +++ b/src/Pure/System/isabelle_system.scala @@ -1,614 +1,614 @@ /* Title: Pure/System/isabelle_system.scala Author: Makarius Fundamental Isabelle system environment: quasi-static module with optional init operation. */ package isabelle import java.io.{File => JFile, IOException} import java.nio.file.{Path => JPath, Files, SimpleFileVisitor, FileVisitResult, StandardCopyOption, FileSystemException} import java.nio.file.attribute.BasicFileAttributes object Isabelle_System { /** bootstrap information **/ def jdk_home(): String = { val java_home = System.getProperty("java.home", "") val home = new JFile(java_home) val parent = home.getParent if (home.getName == "jre" && parent != null && (new JFile(new JFile(parent, "bin"), "javac")).exists) parent else java_home } def bootstrap_directory( preference: String, envar: String, property: String, description: String): String = { val value = proper_string(preference) orElse // explicit argument proper_string(System.getenv(envar)) orElse // e.g. inherited from running isabelle tool proper_string(System.getProperty(property)) getOrElse // e.g. via JVM application boot process error("Unknown " + description + " directory") if ((new JFile(value)).isDirectory) value else error("Bad " + description + " directory " + quote(value)) } /** implicit settings environment **/ abstract class Service @volatile private var _settings: Option[Map[String, String]] = None @volatile private var _services: Option[List[Class[Service]]] = None def settings(): Map[String, String] = { if (_settings.isEmpty) init() // unsynchronized check _settings.get } def services(): List[Class[Service]] = { if (_services.isEmpty) init() // unsynchronized check _services.get } def make_services[C](c: Class[C]): List[C] = for { c1 <- services() if Library.is_subclass(c1, c) } yield c1.getDeclaredConstructor().newInstance().asInstanceOf[C] def init(isabelle_root: String = "", cygwin_root: String = ""): Unit = synchronized { if (_settings.isEmpty || _services.isEmpty) { val isabelle_root1 = bootstrap_directory(isabelle_root, "ISABELLE_ROOT", "isabelle.root", "Isabelle root") val cygwin_root1 = if (Platform.is_windows) bootstrap_directory(cygwin_root, "CYGWIN_ROOT", "cygwin.root", "Cygwin root") else "" if (Platform.is_windows) Cygwin.init(isabelle_root1, cygwin_root1) def set_cygwin_root(): Unit = { if (Platform.is_windows) _settings = Some(_settings.getOrElse(Map.empty) + ("CYGWIN_ROOT" -> cygwin_root1)) } set_cygwin_root() def default(env: Map[String, String], entry: (String, String)): Map[String, String] = if (env.isDefinedAt(entry._1) || entry._2 == "") env else env + entry val env = { val temp_windows = { val temp = if (Platform.is_windows) System.getenv("TEMP") else null if (temp != null && temp.contains('\\')) temp else "" } val user_home = System.getProperty("user.home", "") val isabelle_app = System.getProperty("isabelle.app", "") default( default( default(sys.env + ("ISABELLE_JDK_HOME" -> File.standard_path(jdk_home())), "TEMP_WINDOWS" -> temp_windows), "HOME" -> user_home), "ISABELLE_APP" -> "true") } val settings = { val dump = JFile.createTempFile("settings", null) dump.deleteOnExit try { val cmd1 = if (Platform.is_windows) List(cygwin_root1 + "\\bin\\bash", "-l", File.standard_path(isabelle_root1 + "\\bin\\isabelle")) else List(isabelle_root1 + "/bin/isabelle") val cmd = cmd1 ::: List("getenv", "-d", dump.toString) val (output, rc) = process_output(process(cmd, env = env, redirect = true)) if (rc != 0) error(output) val entries = - (for (entry <- Library.split_strings0(File.read(dump)) if entry != "") yield { + (for (entry <- space_explode('\u0000', File.read(dump)) if entry != "") yield { val i = entry.indexOf('=') if (i <= 0) entry -> "" else entry.substring(0, i) -> entry.substring(i + 1) }).toMap entries + ("PATH" -> entries("PATH_JVM")) - "PATH_JVM" } finally { dump.delete } } _settings = Some(settings) set_cygwin_root() val variable = "ISABELLE_SCALA_SERVICES" val services = for (name <- space_explode(':', settings.getOrElse(variable, getenv_error(variable)))) yield { def err(msg: String): Nothing = error("Bad entry " + quote(name) + " in " + variable + "\n" + msg) try { Class.forName(name).asInstanceOf[Class[Service]] } catch { case _: ClassNotFoundException => err("Class not found") case exn: Throwable => err(Exn.message(exn)) } } _services = Some(services) } } /* getenv -- dynamic process environment */ private def getenv_error(name: String): Nothing = error("Undefined Isabelle environment variable: " + quote(name)) def getenv(name: String, env: Map[String, String] = settings()): String = env.getOrElse(name, "") def getenv_strict(name: String, env: Map[String, String] = settings()): String = proper_string(getenv(name, env)) getOrElse error("Undefined Isabelle environment variable: " + quote(name)) def cygwin_root(): String = getenv_strict("CYGWIN_ROOT") /* getetc -- static distribution parameters */ def getetc(name: String, root: Path = Path.ISABELLE_HOME): Option[String] = { val path = root + Path.basic("etc") + Path.basic(name) if (path.is_file) { Library.trim_split_lines(File.read(path)) match { case Nil => None case List(s) => Some(s) case _ => error("Single line expected in " + path.absolute) } } else None } /* Isabelle distribution identification */ def isabelle_id(root: Path = Path.ISABELLE_HOME): String = getetc("ISABELLE_ID", root = root) orElse Mercurial.archive_id(root) getOrElse { if (Mercurial.is_repository(root)) Mercurial.repository(root).parent() else error("Failed to identify Isabelle distribution " + root) } object Isabelle_Id extends Scala.Fun_String("isabelle_id") { val here = Scala_Project.here def apply(arg: String): String = isabelle_id() } def isabelle_tags(root: Path = Path.ISABELLE_HOME): String = getetc("ISABELLE_TAGS", root = root) orElse Mercurial.archive_tags(root) getOrElse { if (Mercurial.is_repository(root)) { val hg = Mercurial.repository(root) hg.tags(rev = hg.parent()) } else "" } def isabelle_identifier(): Option[String] = proper_string(getenv("ISABELLE_IDENTIFIER")) def isabelle_heading(): String = isabelle_identifier() match { case None => "" case Some(version) => " (" + version + ")" } def isabelle_name(): String = getenv_strict("ISABELLE_NAME") def identification(): String = "Isabelle/" + isabelle_id() + isabelle_heading() /** file-system operations **/ /* scala functions */ private def apply_paths(args: List[String], fun: List[Path] => Unit): List[String] = { fun(args.map(Path.explode)); Nil } private def apply_paths1(args: List[String], fun: Path => Unit): List[String] = apply_paths(args, { case List(path) => fun(path) }) private def apply_paths2(args: List[String], fun: (Path, Path) => Unit): List[String] = apply_paths(args, { case List(path1, path2) => fun(path1, path2) }) private def apply_paths3(args: List[String], fun: (Path, Path, Path) => Unit): List[String] = apply_paths(args, { case List(path1, path2, path3) => fun(path1, path2, path3) }) /* permissions */ def chmod(arg: String, path: Path): Unit = bash("chmod " + arg + " " + File.bash_path(path)).check def chown(arg: String, path: Path): Unit = bash("chown " + arg + " " + File.bash_path(path)).check /* directories */ def make_directory(path: Path): Path = { if (!path.is_dir) { try { Files.createDirectories(path.file.toPath) } catch { case ERROR(_) => error("Failed to create directory: " + path.absolute) } } path } def new_directory(path: Path): Path = if (path.is_dir) error("Directory already exists: " + path.absolute) else make_directory(path) def copy_dir(dir1: Path, dir2: Path): Unit = { val res = bash("cp -a " + File.bash_path(dir1) + " " + File.bash_path(dir2)) if (!res.ok) { cat_error("Failed to copy directory " + dir1.absolute + " to " + dir2.absolute, res.err) } } object Make_Directory extends Scala.Fun_Strings("make_directory") { val here = Scala_Project.here def apply(args: List[String]): List[String] = apply_paths1(args, make_directory) } object Copy_Dir extends Scala.Fun_Strings("copy_dir") { val here = Scala_Project.here def apply(args: List[String]): List[String] = apply_paths2(args, copy_dir) } /* copy files */ def copy_file(src: JFile, dst: JFile): Unit = { val target = if (dst.isDirectory) new JFile(dst, src.getName) else dst if (!File.eq(src, target)) { try { Files.copy(src.toPath, target.toPath, StandardCopyOption.COPY_ATTRIBUTES, StandardCopyOption.REPLACE_EXISTING) } catch { case ERROR(msg) => cat_error("Failed top copy file " + File.path(src).absolute + " to " + File.path(dst).absolute, msg) } } } def copy_file(src: Path, dst: Path): Unit = copy_file(src.file, dst.file) def copy_file_base(base_dir: Path, src: Path, target_dir: Path): Unit = { val src1 = src.expand val src1_dir = src1.dir if (!src1.starts_basic) error("Illegal path specification " + src1 + " beyond base directory") copy_file(base_dir + src1, Isabelle_System.make_directory(target_dir + src1_dir)) } object Copy_File extends Scala.Fun_Strings("copy_file") { val here = Scala_Project.here def apply(args: List[String]): List[String] = apply_paths2(args, copy_file) } object Copy_File_Base extends Scala.Fun_Strings("copy_file_base") { val here = Scala_Project.here def apply(args: List[String]): List[String] = apply_paths3(args, copy_file_base) } /* move files */ def move_file(src: JFile, dst: JFile): Unit = { val target = if (dst.isDirectory) new JFile(dst, src.getName) else dst if (!File.eq(src, target)) Files.move(src.toPath, target.toPath, StandardCopyOption.REPLACE_EXISTING) } def move_file(src: Path, dst: Path): Unit = move_file(src.file, dst.file) /* symbolic link */ def symlink(src: Path, dst: Path, force: Boolean = false): Unit = { val src_file = src.file val dst_file = dst.file val target = if (dst_file.isDirectory) new JFile(dst_file, src_file.getName) else dst_file if (force) target.delete try { Files.createSymbolicLink(target.toPath, src_file.toPath) } catch { case _: UnsupportedOperationException if Platform.is_windows => Cygwin.link(File.standard_path(src), target) case _: FileSystemException if Platform.is_windows => Cygwin.link(File.standard_path(src), target) } } /* tmp files */ def isabelle_tmp_prefix(): JFile = { val path = Path.explode("$ISABELLE_TMP_PREFIX") path.file.mkdirs // low-level mkdirs to avoid recursion via Isabelle environment File.platform_file(path) } def tmp_file(name: String, ext: String = "", base_dir: JFile = isabelle_tmp_prefix()): JFile = { val suffix = if (ext == "") "" else "." + ext val file = Files.createTempFile(base_dir.toPath, name, suffix).toFile file.deleteOnExit file } def with_tmp_file[A](name: String, ext: String = "")(body: Path => A): A = { val file = tmp_file(name, ext) try { body(File.path(file)) } finally { file.delete } } /* tmp dirs */ def rm_tree(root: JFile): Unit = { root.delete if (root.isDirectory) { Files.walkFileTree(root.toPath, new SimpleFileVisitor[JPath] { override def visitFile(file: JPath, attrs: BasicFileAttributes): FileVisitResult = { try { Files.deleteIfExists(file) } catch { case _: IOException => } FileVisitResult.CONTINUE } override def postVisitDirectory(dir: JPath, e: IOException): FileVisitResult = { if (e == null) { try { Files.deleteIfExists(dir) } catch { case _: IOException => } FileVisitResult.CONTINUE } else throw e } } ) } } def rm_tree(root: Path): Unit = rm_tree(root.file) object Rm_Tree extends Scala.Fun_Strings("rm_tree") { val here = Scala_Project.here def apply(args: List[String]): List[String] = apply_paths1(args, rm_tree) } def tmp_dir(name: String, base_dir: JFile = isabelle_tmp_prefix()): JFile = { val dir = Files.createTempDirectory(base_dir.toPath, name).toFile dir.deleteOnExit dir } def with_tmp_dir[A](name: String)(body: Path => A): A = { val dir = tmp_dir(name) try { body(File.path(dir)) } finally { rm_tree(dir) } } /* quasi-atomic update of directory */ def update_directory(dir: Path, f: Path => Unit): Unit = { val new_dir = dir.ext("new") val old_dir = dir.ext("old") rm_tree(new_dir) rm_tree(old_dir) f(new_dir) if (dir.is_dir) move_file(dir, old_dir) move_file(new_dir, dir) rm_tree(old_dir) } /** external processes **/ /* raw process */ def process(command_line: List[String], cwd: JFile = null, env: Map[String, String] = settings(), redirect: Boolean = false): Process = { val proc = new ProcessBuilder proc.command(command_line:_*) // fragile on Windows if (cwd != null) proc.directory(cwd) if (env != null) { proc.environment.clear() for ((x, y) <- env) proc.environment.put(x, y) } proc.redirectErrorStream(redirect) proc.start } def process_output(proc: Process): (String, Int) = { proc.getOutputStream.close() val output = File.read_stream(proc.getInputStream) val rc = try { proc.waitFor } finally { proc.getInputStream.close() proc.getErrorStream.close() proc.destroy() Exn.Interrupt.dispose() } (output, rc) } def kill(signal: String, group_pid: String): (String, Int) = { val bash = if (Platform.is_windows) List(cygwin_root() + "\\bin\\bash.exe") else List("/usr/bin/env", "bash") process_output(process(bash ::: List("-c", "kill -" + signal + " -" + group_pid))) } /* GNU bash */ def bash(script: String, cwd: JFile = null, env: Map[String, String] = settings(), redirect: Boolean = false, progress_stdout: String => Unit = (_: String) => (), progress_stderr: String => Unit = (_: String) => (), watchdog: Option[Bash.Watchdog] = None, strict: Boolean = true, cleanup: () => Unit = () => ()): Process_Result = { Bash.process(script, cwd = cwd, env = env, redirect = redirect, cleanup = cleanup). result(progress_stdout = progress_stdout, progress_stderr = progress_stderr, watchdog = watchdog, strict = strict) } private lazy val gnutar_check: Boolean = try { bash("tar --version").check.out.containsSlice("GNU tar") || error("") } catch { case ERROR(_) => false } def gnutar( args: String, dir: Path = Path.current, original_owner: Boolean = false, redirect: Boolean = false): Process_Result = { val options = (if (dir.is_current) "" else "-C " + File.bash_path(dir) + " ") + (if (original_owner) "" else "--owner=root --group=staff ") if (gnutar_check) bash("tar " + options + args, redirect = redirect) else error("Expected to find GNU tar executable") } def require_command(cmds: String*): Unit = { for (cmd <- cmds) { if (!bash(Bash.string(cmd) + " --version").ok) error("Missing system command: " + quote(cmd)) } } def hostname(): String = bash("hostname -s").check.out def open(arg: String): Unit = bash("exec \"$ISABELLE_OPEN\" " + Bash.string(arg) + " >/dev/null 2>/dev/null &") def pdf_viewer(arg: Path): Unit = bash("exec \"$PDF_VIEWER\" " + File.bash_path(arg) + " >/dev/null 2>/dev/null &") def open_external_file(name: String): Boolean = { val ext = Library.take_suffix((c: Char) => c != '.', name.toList)._2.mkString val external = ext.nonEmpty && Library.space_explode(':', getenv("ISABELLE_EXTERNAL_FILES")).contains(ext) if (external) { if (ext == "pdf" && Path.is_wellformed(name)) pdf_viewer(Path.explode(name)) else open(name) } external } def export_isabelle_identifier(isabelle_identifier: String): String = if (isabelle_identifier == "") "" else "export ISABELLE_IDENTIFIER=" + Bash.string(isabelle_identifier) + "\n" /** Isabelle resources **/ /* repository clone with Admin */ def admin(): Boolean = Path.explode("~~/Admin").is_dir /* components */ def components(): List[Path] = Path.split(getenv_strict("ISABELLE_COMPONENTS")) /* default logic */ def default_logic(args: String*): String = { args.find(_ != "") match { case Some(logic) => logic case None => getenv_strict("ISABELLE_LOGIC") } } /* download file */ def download(url_name: String, progress: Progress = new Progress): HTTP.Content = { val url = Url(url_name) progress.echo("Getting " + quote(url_name)) try { HTTP.Client.get(url) } catch { case ERROR(msg) => cat_error("Failed to download " + quote(url_name), msg) } } def download_file(url_name: String, file: Path, progress: Progress = new Progress): Unit = Bytes.write(file, download(url_name, progress = progress).bytes) object Download extends Scala.Fun("download", thread = true) { val here = Scala_Project.here override def invoke(args: List[Bytes]): List[Bytes] = args match { case List(url) => List(download(url.text).bytes) } } } diff --git a/src/Pure/library.scala b/src/Pure/library.scala --- a/src/Pure/library.scala +++ b/src/Pure/library.scala @@ -1,309 +1,304 @@ /* Title: Pure/library.scala Author: Makarius Basic library. */ package isabelle import scala.annotation.tailrec import scala.collection.mutable import scala.util.matching.Regex object Library { /* resource management */ def using[A <: AutoCloseable, B](a: A)(f: A => B): B = { try { f(a) } finally { if (a != null) a.close() } } /* integers */ private val small_int = 10000 private lazy val small_int_table = { val array = new Array[String](small_int) for (i <- 0 until small_int) array(i) = i.toString array } def is_small_int(s: String): Boolean = { val len = s.length 1 <= len && len <= 4 && s.forall(c => '0' <= c && c <= '9') && (len == 1 || s(0) != '0') } def signed_string_of_long(i: Long): String = if (0 <= i && i < small_int) small_int_table(i.toInt) else i.toString def signed_string_of_int(i: Int): String = if (0 <= i && i < small_int) small_int_table(i) else i.toString /* separated chunks */ def separate[A](s: A, list: List[A]): List[A] = { val result = new mutable.ListBuffer[A] var first = true for (x <- list) { if (first) { first = false result += x } else { result += s result += x } } result.toList } def separated_chunks(sep: Char => Boolean, source: CharSequence): Iterator[CharSequence] = new Iterator[CharSequence] { private val end = source.length private def next_chunk(i: Int): Option[(CharSequence, Int)] = { if (i < end) { var j = i; do j += 1 while (j < end && !sep(source.charAt(j))) Some((source.subSequence(i + 1, j), j)) } else None } private var state: Option[(CharSequence, Int)] = if (end == 0) None else next_chunk(-1) def hasNext: Boolean = state.isDefined def next(): CharSequence = state match { case Some((s, i)) => state = next_chunk(i); s case None => Iterator.empty.next() } } def space_explode(sep: Char, str: String): List[String] = separated_chunks(_ == sep, str).map(_.toString).toList /* lines */ def terminate_lines(lines: IterableOnce[String]): String = lines.iterator.mkString("", "\n", "\n") def cat_lines(lines: IterableOnce[String]): String = lines.iterator.mkString("\n") def split_lines(str: String): List[String] = space_explode('\n', str) def prefix_lines(prfx: String, str: String): String = if (str == "") str else cat_lines(split_lines(str).map(prfx + _)) def first_line(source: CharSequence): String = { val lines = separated_chunks(_ == '\n', source) if (lines.hasNext) lines.next().toString else "" } def trim_line(s: String): String = if (s.endsWith("\r\n")) s.substring(0, s.length - 2) else if (s.endsWith("\r") || s.endsWith("\n")) s.substring(0, s.length - 1) else s def trim_split_lines(s: String): List[String] = split_lines(trim_line(s)).map(trim_line) def encode_lines(s: String): String = s.replace('\n', '\u000b') def decode_lines(s: String): String = s.replace('\u000b', '\n') /* strings */ - def cat_strings0(strs: IterableOnce[String]): String = - strs.iterator.mkString("\u0000") - - def split_strings0(str: String): List[String] = space_explode('\u0000', str) - def make_string(f: StringBuilder => Unit): String = { val s = new StringBuilder f(s) s.toString } def try_unprefix(prfx: String, s: String): Option[String] = if (s.startsWith(prfx)) Some(s.substring(prfx.length)) else None def try_unsuffix(sffx: String, s: String): Option[String] = if (s.endsWith(sffx)) Some(s.substring(0, s.length - sffx.length)) else None def perhaps_unprefix(prfx: String, s: String): String = try_unprefix(prfx, s) getOrElse s def perhaps_unsuffix(sffx: String, s: String): String = try_unsuffix(sffx, s) getOrElse s def isolate_substring(s: String): String = new String(s.toCharArray) def strip_ansi_color(s: String): String = s.replaceAll("\u001b\\[\\d+m", "") /* quote */ def single_quote(s: String): String = "'" + s + "'" def quote(s: String): String = "\"" + s + "\"" def try_unquote(s: String): Option[String] = if (s.startsWith("\"") && s.endsWith("\"")) Some(s.substring(1, s.length - 1)) else None def perhaps_unquote(s: String): String = try_unquote(s) getOrElse s def commas(ss: Iterable[String]): String = ss.iterator.mkString(", ") def commas_quote(ss: Iterable[String]): String = ss.iterator.map(quote).mkString(", ") /* CharSequence */ class Reverse(text: CharSequence, start: Int, end: Int) extends CharSequence { require(0 <= start && start <= end && end <= text.length, "bad reverse range") def this(text: CharSequence) = this(text, 0, text.length) def length: Int = end - start def charAt(i: Int): Char = text.charAt(end - i - 1) def subSequence(i: Int, j: Int): CharSequence = if (0 <= i && i <= j && j <= length) new Reverse(text, end - j, end - i) else throw new IndexOutOfBoundsException override def toString: String = { val buf = new StringBuilder(length) for (i <- 0 until length) buf.append(charAt(i)) buf.toString } } class Line_Termination(text: CharSequence) extends CharSequence { def length: Int = text.length + 1 def charAt(i: Int): Char = if (i == text.length) '\n' else text.charAt(i) def subSequence(i: Int, j: Int): CharSequence = if (j == text.length + 1) new Line_Termination(text.subSequence(i, j - 1)) else text.subSequence(i, j) override def toString: String = text.toString + "\n" } /* regular expressions */ def make_regex(s: String): Option[Regex] = try { Some(new Regex(s)) } catch { case ERROR(_) => None } def is_regex_meta(c: Char): Boolean = """()[]{}\^$|?*+.<>-=!""".contains(c) def escape_regex(s: String): String = if (s.exists(is_regex_meta)) { (for (c <- s.iterator) yield { if (is_regex_meta(c)) "\\" + c.toString else c.toString }).mkString } else s /* lists */ def take_prefix[A](pred: A => Boolean, xs: List[A]): (List[A], List[A]) = (xs.takeWhile(pred), xs.dropWhile(pred)) def take_suffix[A](pred: A => Boolean, xs: List[A]): (List[A], List[A]) = { val rev_xs = xs.reverse (rev_xs.dropWhile(pred).reverse, rev_xs.takeWhile(pred).reverse) } def trim[A](pred: A => Boolean, xs: List[A]): List[A] = take_suffix(pred, take_prefix(pred, xs)._2)._1 def member[A, B](xs: List[A])(x: B): Boolean = xs.contains(x) def insert[A](x: A)(xs: List[A]): List[A] = if (xs.contains(x)) xs else x :: xs def remove[A, B](x: B)(xs: List[A]): List[A] = if (member(xs)(x)) xs.filterNot(_ == x) else xs def update[A](x: A)(xs: List[A]): List[A] = x :: remove(x)(xs) def merge[A](xs: List[A], ys: List[A]): List[A] = if (xs.eq(ys)) xs else if (xs.isEmpty) ys else ys.foldRight(xs)(Library.insert(_)(_)) def distinct[A](xs: List[A], eq: (A, A) => Boolean = (x: A, y: A) => x == y): List[A] = { val result = new mutable.ListBuffer[A] xs.foreach(x => if (!result.exists(y => eq(x, y))) result += x) result.toList } def duplicates[A](lst: List[A], eq: (A, A) => Boolean = (x: A, y: A) => x == y): List[A] = { val result = new mutable.ListBuffer[A] @tailrec def dups(rest: List[A]): Unit = rest match { case Nil => case x :: xs => if (!result.exists(y => eq(x, y)) && xs.exists(y => eq(x, y))) result += x dups(xs) } dups(lst) result.toList } def replicate[A](n: Int, a: A): List[A] = if (n < 0) throw new IllegalArgumentException else if (n == 0) Nil else { val res = new mutable.ListBuffer[A] (1 to n).foreach(_ => res += a) res.toList } def the_single[A](xs: List[A]): A = xs match { case List(x) => x case _ => error("Single argument expected") } /* proper values */ def proper_string(s: String): Option[String] = if (s == null || s == "") None else Some(s) def proper_list[A](list: List[A]): Option[List[A]] = if (list == null || list.isEmpty) None else Some(list) /* reflection */ def is_subclass[A, B](a: Class[A], b: Class[B]): Boolean = { import scala.language.existentials @tailrec def subclass(c: Class[_]): Boolean = { c == b || { val d = c.getSuperclass d != null && subclass(d) } } subclass(a) } }