# HG changeset patch
# User wenzelm
# Date 1343156178 -7200
# Node ID 70898d01653847676508547a3cecd51b46c88c6a
# Parent  9bfb6978eb80dbdb578e24872d1f79cce1123e2b
more explicit checks during parsing;

diff -r 9bfb6978eb80 -r 70898d016538 src/Pure/General/path.scala
--- a/src/Pure/General/path.scala	Tue Jul 24 20:42:34 2012 +0200
+++ b/src/Pure/General/path.scala	Tue Jul 24 20:56:18 2012 +0200
@@ -96,6 +96,9 @@
     new Path(norm_elems(explode_elems(raw_elems) ++ roots))
   }
 
+  def is_ok(str: String): Boolean =
+    try { explode(str); true } catch { case ERROR(_) => false }
+
   def split(str: String): List[Path] =
     space_explode(':', str).filterNot(_.isEmpty).map(explode)
 
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 =>
diff -r 9bfb6978eb80 -r 70898d016538 src/Pure/System/build.scala
--- a/src/Pure/System/build.scala	Tue Jul 24 20:42:34 2012 +0200
+++ b/src/Pure/System/build.scala	Tue Jul 24 20:56:18 2012 +0200
@@ -142,7 +142,6 @@
     val session_entry: Parser[Session_Entry] =
     {
       val session_name = atom("session name", _.is_name)
-      val theory_name = atom("theory name", _.is_name)
 
       val option =
         name ~ opt(keyword("=") ~! name ^^ { case _ ~ x => x }) ^^ { case x ~ y => (x, y) }
diff -r 9bfb6978eb80 -r 70898d016538 src/Pure/Thy/thy_header.scala
--- a/src/Pure/Thy/thy_header.scala	Tue Jul 24 20:42:34 2012 +0200
+++ b/src/Pure/Thy/thy_header.scala	Tue Jul 24 20:56:18 2012 +0200
@@ -46,7 +46,6 @@
   val header: Parser[Thy_Header] =
   {
     val file_name = atom("file name", _.is_name)
-    val theory_name = atom("theory name", _.is_name)
 
     val keyword_kind =
       atom("outer syntax keyword kind", _.is_name) ~ tags ^^ { case x ~ y => (x, y) }
diff -r 9bfb6978eb80 -r 70898d016538 src/Pure/Thy/thy_load.scala
--- a/src/Pure/Thy/thy_load.scala	Tue Jul 24 20:42:34 2012 +0200
+++ b/src/Pure/Thy/thy_load.scala	Tue Jul 24 20:56:18 2012 +0200
@@ -13,6 +13,10 @@
 object Thy_Load
 {
   def thy_path(path: Path): Path = path.ext("thy")
+
+  def is_ok(str: String): Boolean =
+    try { thy_path(Path.explode(str)); true }
+    catch { case ERROR(_) => false }
 }