# HG changeset patch
# User wenzelm
# Date 1507801194 -7200
# Node ID a91b6d80c91104c12aa74fc1434528c4e475c762
# Parent  42311fd08899267d7014f2b388aa023134bb0955
more robust: allow URLs;

diff -r 42311fd08899 -r a91b6d80c911 src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala	Thu Oct 12 11:39:06 2017 +0200
+++ b/src/Pure/PIDE/resources.scala	Thu Oct 12 11:39:54 2017 +0200
@@ -126,12 +126,16 @@
     val s1 =
       if (session_base.loaded_theory(name)) name.theory
       else {
-        session_base.known.get_file(name.path.file) match {
-          case Some(name1) if session_resources.theory_qualifier(name1) != qualifier =>
-            name1.theory
-          case Some(name1) if Thy_Header.is_base_name(s) =>
-            name1.theory_base_name
-          case _ => s
+        (try { Some(name.path) } catch { case ERROR(_) => None }) match {
+          case None => s
+          case Some(path) =>
+            session_base.known.get_file(path.file) match {
+              case Some(name1) if session_resources.theory_qualifier(name1) != qualifier =>
+                name1.theory
+              case Some(name1) if Thy_Header.is_base_name(s) =>
+                name1.theory_base_name
+              case _ => s
+            }
         }
       }
     val name2 = import_name(qualifier, dir, s1)