src/Pure/Isar/parse.scala
changeset 64471 c40c2975fb02
parent 63446 19162a9ef7e3
child 66914 fb3f13a9c756
--- 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))