equal
deleted
inserted
replaced
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 |