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