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