clarified split_thy_path;
authorwenzelm
Thu Jan 13 17:30:52 2011 +0100 (2011-01-13)
changeset 415350112f14d75ec
parent 41534 f36cb6f233bd
child 41536 47fef6afe756
clarified split_thy_path;
src/Pure/Thy/thy_header.scala
     1.1 --- a/src/Pure/Thy/thy_header.scala	Thu Jan 13 17:27:52 2011 +0100
     1.2 +++ b/src/Pure/Thy/thy_header.scala	Thu Jan 13 17:30:52 2011 +0100
     1.3 @@ -30,7 +30,7 @@
     1.4    /* file name */
     1.5  
     1.6    val Thy_Path1 = new Regex("([^/]*)\\.thy")
     1.7 -  val Thy_Path2 = new Regex("(.*/)([^/]*)\\.thy")
     1.8 +  val Thy_Path2 = new Regex("(.*)/([^/]*)\\.thy")
     1.9  
    1.10    def split_thy_path(path: String): Option[(String, String)] =
    1.11      path match {