simplified (despite 70898d016538);
authorwenzelm
Tue Mar 18 17:53:40 2014 +0100 (2014-03-18)
changeset 562093c89e21d9be2
parent 56208 06cc31dff138
child 56210 c7c85cdb725d
simplified (despite 70898d016538);
src/Pure/Isar/parse.scala
src/Pure/PIDE/resources.scala
     1.1 --- a/src/Pure/Isar/parse.scala	Tue Mar 18 17:39:03 2014 +0100
     1.2 +++ b/src/Pure/Isar/parse.scala	Tue Mar 18 17:53:40 2014 +0100
     1.3 @@ -64,7 +64,7 @@
     1.4      def path: Parser[String] =
     1.5        atom("file name/path specification", tok => tok.is_name && Path.is_wellformed(tok.content))
     1.6      def theory_name: Parser[String] =
     1.7 -      atom("theory name", tok => tok.is_name && Resources.is_wellformed_thy_path(tok.content))
     1.8 +      atom("theory name", tok => tok.is_name && Path.is_wellformed(tok.content))
     1.9  
    1.10      private def tag_name: Parser[String] =
    1.11        atom("tag name", tok =>
     2.1 --- a/src/Pure/PIDE/resources.scala	Tue Mar 18 17:39:03 2014 +0100
     2.2 +++ b/src/Pure/PIDE/resources.scala	Tue Mar 18 17:53:40 2014 +0100
     2.3 @@ -14,13 +14,7 @@
     2.4  
     2.5  object Resources
     2.6  {
     2.7 -  /* paths */
     2.8 -
     2.9    def thy_path(path: Path): Path = path.ext("thy")
    2.10 -
    2.11 -  def is_wellformed_thy_path(str: String): Boolean =
    2.12 -    try { thy_path(Path.explode(str)); true }
    2.13 -    catch { case ERROR(_) => false }
    2.14  }
    2.15  
    2.16