src/Pure/Isar/parse.scala
changeset 48484 70898d016538
parent 48349 a78e5d399599
child 48599 5e64b7770f35
--- a/src/Pure/Isar/parse.scala	Tue Jul 24 20:42:34 2012 +0200
+++ b/src/Pure/Isar/parse.scala	Tue Jul 24 20:56:18 2012 +0200
@@ -60,7 +60,10 @@
     def text: Parser[String] = atom("text", _.is_text)
     def ML_source: Parser[String] = atom("ML source", _.is_text)
     def doc_source: Parser[String] = atom("document source", _.is_text)
-    def path: Parser[String] = atom("file name/path specification", _.is_name)
+    def path: Parser[String] =
+      atom("file name/path specification", tok => tok.is_name && Path.is_ok(tok.content))
+    def theory_name: Parser[String] =
+      atom("theory name", tok => tok.is_name && Thy_Load.is_ok(tok.content))
 
     private def tag_name: Parser[String] =
       atom("tag name", tok =>