diff -r 9bfb6978eb80 -r 70898d016538 src/Pure/Isar/parse.scala --- 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 =>