src/Pure/PIDE/command.scala
changeset 62965 5bf08c9aa036
parent 61579 634cd44bb1d3
child 62969 9f394a16c557
--- a/src/Pure/PIDE/command.scala	Wed Apr 13 11:26:52 2016 +0200
+++ b/src/Pure/PIDE/command.scala	Wed Apr 13 11:31:13 2016 +0200
@@ -322,7 +322,7 @@
   private def find_file(tokens: List[(Token, Int)]): Option[(String, Int)] =
     if (tokens.exists({ case (t, _) => t.is_command })) {
       tokens.dropWhile({ case (t, _) => !t.is_command }).
-        collectFirst({ case (t, i) if t.is_name => (t.content, i) })
+        collectFirst({ case (t, i) if t.is_xname => (t.content, i) })
     }
     else None