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