more uniform path syntax, as in ML (see 5a7c919a4ada);

--- a/src/Pure/Isar/parse.scala	Mon Nov 07 19:07:30 2016 +0100
+++ b/src/Pure/Isar/parse.scala	Mon Nov 07 19:09:10 2016 +0100
@@ -64,12 +64,13 @@
     def string: Parser[String] = atom("string", _.is_string)
     def nat: Parser[Int] = atom("natural number", _.is_nat) ^^ (s => Integer.parseInt(s))
     def name: Parser[String] = atom("name", _.is_name)
+    def embedded: Parser[String] = atom("embedded content", _.is_embedded)
     def text: Parser[String] = atom("text", _.is_text)
     def ML_source: Parser[String] = atom("ML source", _.is_text)
     def document_source: Parser[String] = atom("document source", _.is_text)
 
     def path: Parser[String] =
-      atom("file name/path specification", tok => tok.is_name && Path.is_wellformed(tok.content))
+      atom("file name/path specification", tok => tok.is_embedded && Path.is_wellformed(tok.content))
 
     def theory_name: Parser[String] =
       atom("theory name", tok => tok.is_name && Path.is_wellformed(tok.content))

--- a/src/Pure/Isar/token.scala	Mon Nov 07 19:07:30 2016 +0100
+++ b/src/Pure/Isar/token.scala	Mon Nov 07 19:09:10 2016 +0100
@@ -242,6 +242,11 @@
     kind == Token.Kind.SYM_IDENT ||
     kind == Token.Kind.STRING ||
     kind == Token.Kind.NAT
+  def is_embedded: Boolean = is_name ||
+    kind == Token.Kind.CARTOUCHE ||
+    kind == Token.Kind.VAR ||
+    kind == Token.Kind.TYPE_IDENT ||
+    kind == Token.Kind.TYPE_VAR
   def is_text: Boolean = is_name || kind == Token.Kind.VERBATIM || kind == Token.Kind.CARTOUCHE
   def is_space: Boolean = kind == Token.Kind.SPACE
   def is_comment: Boolean = kind == Token.Kind.COMMENT

--- 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