# HG changeset patch
# User wenzelm
# Date 1547319237 -3600
# Node ID 091f57432f057775878297ef6a42a5e496e5290e
# Parent  938b28a998637f6582ff5cfa4506e1c89a8fde12
more robust: jEdit may produce names with trailing "/";

diff -r 938b28a99863 -r 091f57432f05 src/Tools/jEdit/src/isabelle_export.scala
--- a/src/Tools/jEdit/src/isabelle_export.scala	Fri Jan 11 22:59:00 2019 +0100
+++ b/src/Tools/jEdit/src/isabelle_export.scala	Sat Jan 12 19:53:57 2019 +0100
@@ -38,16 +38,11 @@
 
   def explode_url(url: String, component: Component = null): Option[List[String]] =
   {
-    def bad: None.type =
-    {
-      if (component != null) vfs_error(component, url, "ioerror.badurl", url)
-      None
-    }
     Library.try_unprefix(vfs_prefix, url) match {
-      case Some(path) =>
-        val elems = Export.explode_name(path)
-        if (elems.exists(_.isEmpty)) bad else Some(elems)
-      case None => bad
+      case Some(path) => Some(Export.explode_name(path).filter(_.nonEmpty))
+      case None =>
+        if (component != null) vfs_error(component, url, "ioerror.badurl", url)
+        None
     }
   }