tuned;
authorwenzelm
Fri, 28 Apr 2017 14:23:55 +0200
changeset 65606 d2f83588080f
parent 65605 a6447eb6bc38
child 65607 c937984c70e9
tuned;
src/Pure/System/isabelle_tool.scala
src/Pure/library.scala
--- 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)