# HG changeset patch
# User wenzelm
# Date 1493382235 -7200
# Node ID d2f83588080fe26814aef1471e7939913dc866c4
# Parent  a6447eb6bc38e1b613fbc9d66dd1d3dda5e7f790
tuned;

diff -r a6447eb6bc38 -r d2f83588080f src/Pure/System/isabelle_tool.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)
diff -r a6447eb6bc38 -r d2f83588080f src/Pure/library.scala
--- 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)