src/Pure/Thy/sessions.scala
changeset 70693 0fec12eabad0
parent 70687 086575316fd5
child 70712 a3cfe859d915
equal deleted inserted replaced
70692:41b5e515c238 70693:0fec12eabad0
   382                 for { (path1, name) <- bad }
   382                 for { (path1, name) <- bad }
   383                 yield "Implicit use of directory " + path1 + " for theory " + quote(name.toString)
   383                 yield "Implicit use of directory " + path1 + " for theory " + quote(name.toString)
   384               val errs2 =
   384               val errs2 =
   385                 if (bad_dirs.isEmpty) Nil
   385                 if (bad_dirs.isEmpty) Nil
   386                 else List("Implicit use of session directories: " + commas(bad_dirs))
   386                 else List("Implicit use of session directories: " + commas(bad_dirs))
   387               errs1 ::: errs2
   387               val errs3 = for (p <- info.dirs if !p.is_dir) yield "No such directory: " + p
       
   388 
       
   389               errs1 ::: errs2 ::: errs3
   388             }
   390             }
   389 
   391 
   390             val sources_errors =
   392             val sources_errors =
   391               for (p <- session_files if !p.is_file) yield "No such file: " + p
   393               for (p <- session_files if !p.is_file) yield "No such file: " + p
   392 
   394