src/Pure/PIDE/command.scala
changeset 64471 c40c2975fb02
parent 63584 68751fe1c036
child 64802 adc4c84b692c
--- a/src/Pure/PIDE/command.scala	Mon Nov 07 19:07:30 2016 +0100
+++ b/src/Pure/PIDE/command.scala	Mon Nov 07 19:09:10 2016 +0100
@@ -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_embedded => (t.content, i) })
     }
     else None