# 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 } }