src/Pure/Thy/sessions.scala
changeset 70684 60b1eda998f3
parent 70683 8c7706b053c7
child 70685 c1597167563e
equal deleted inserted replaced
70683:8c7706b053c7 70684:60b1eda998f3
   689           dir <- info.dirs.iterator
   689           dir <- info.dirs.iterator
   690         } yield (info, dir)))({ case (dirs, (info, dir)) =>
   690         } yield (info, dir)))({ case (dirs, (info, dir)) =>
   691             val session = info.name
   691             val session = info.name
   692             val canonical_dir = dir.canonical_file
   692             val canonical_dir = dir.canonical_file
   693             dirs.get(canonical_dir) match {
   693             dirs.get(canonical_dir) match {
   694               case Some(session1) if session1 != session =>
   694               case Some(session1) =>
   695                 val info1 = info_graph.get_node(session1)
   695                 val info1 = info_graph.get_node(session1)
   696                 error("Duplicate use of directory " + dir +
   696                 error("Duplicate use of directory " + dir +
   697                   "\n  for session " + quote(session1) + Position.here(info1.pos) +
   697                   "\n  for session " + quote(session1) + Position.here(info1.pos) +
   698                   "\n  vs. session " + quote(session) + Position.here(info.pos))
   698                   "\n  vs. session " + quote(session) + Position.here(info.pos))
   699               case None => dirs + (canonical_dir -> session)
   699               case None => dirs + (canonical_dir -> session)