--- a/src/Pure/System/isabelle_tool.scala Fri Apr 28 14:12:57 2017 +0200
+++ b/src/Pure/System/isabelle_tool.scala Fri Apr 28 14:23:55 2017 +0200
@@ -74,7 +74,7 @@
file_name <- File.read_dir(dir) if is_external(dir, file_name)
} yield {
val source = File.read(dir + Path.explode(file_name))
- val name = Library.try_unsuffix(".scala", file_name) getOrElse file_name
+ val name = Library.perhaps_unsuffix(".scala", file_name)
val description =
split_lines(source).collectFirst({ case Description(s) => s }) getOrElse ""
(name, description)
--- a/src/Pure/library.scala Fri Apr 28 14:12:57 2017 +0200
+++ b/src/Pure/library.scala Fri Apr 28 14:23:55 2017 +0200
@@ -131,6 +131,9 @@
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 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)