src/Pure/Thy/sessions.scala
changeset 66764 006deaf5c3dc
parent 66759 918f15c9367a
child 66770 122df1fde073
     1.1 --- a/src/Pure/Thy/sessions.scala	Tue Oct 03 20:32:58 2017 +0200
     1.2 +++ b/src/Pure/Thy/sessions.scala	Wed Oct 04 20:16:53 2017 +0200
     1.3 @@ -624,7 +624,7 @@
     1.4              Session_Entry(pos, a, b, c, d, e, f, g, h, i) }
     1.5      }
     1.6  
     1.7 -    def parse(options: Options, select: Boolean, dir: Path): List[(String, Info)] =
     1.8 +    def parse_root(options: Options, select: Boolean, path: Path): List[(String, Info)] =
     1.9      {
    1.10        def make_info(entry_chapter: String, entry: Session_Entry): (String, Info) =
    1.11        {
    1.12 @@ -659,7 +659,7 @@
    1.13  
    1.14            val info =
    1.15              Info(name, entry_chapter, select, entry.pos, entry.groups,
    1.16 -              dir + Path.explode(entry.path), entry.parent, entry.description, session_options,
    1.17 +              path.dir + Path.explode(entry.path), entry.parent, entry.description, session_options,
    1.18                entry.imports, theories, global_theories, document_files, meta_digest)
    1.19  
    1.20            (name, info)
    1.21 @@ -671,24 +671,20 @@
    1.22          }
    1.23        }
    1.24  
    1.25 -      val root = dir + ROOT
    1.26 -      if (root.is_file) {
    1.27 -        val toks = Token.explode(root_syntax.keywords, File.read(root))
    1.28 -        val start = Token.Pos.file(root.implode)
    1.29 +      val toks = Token.explode(root_syntax.keywords, File.read(path))
    1.30 +      val start = Token.Pos.file(path.implode)
    1.31  
    1.32 -        parse_all(rep(chapter | session_entry), Token.reader(toks, start)) match {
    1.33 -          case Success(result, _) =>
    1.34 -            var entry_chapter = "Unsorted"
    1.35 -            val infos = new mutable.ListBuffer[(String, Info)]
    1.36 -            result.foreach {
    1.37 -              case Chapter(name) => entry_chapter = name
    1.38 -              case entry: Session_Entry => infos += make_info(entry_chapter, entry)
    1.39 -            }
    1.40 -            infos.toList
    1.41 -          case bad => error(bad.toString)
    1.42 -        }
    1.43 +      parse_all(rep(chapter | session_entry), Token.reader(toks, start)) match {
    1.44 +        case Success(result, _) =>
    1.45 +          var entry_chapter = "Unsorted"
    1.46 +          val infos = new mutable.ListBuffer[(String, Info)]
    1.47 +          result.foreach {
    1.48 +            case Chapter(name) => entry_chapter = name
    1.49 +            case entry: Session_Entry => infos += make_info(entry_chapter, entry)
    1.50 +          }
    1.51 +          infos.toList
    1.52 +        case bad => error(bad.toString)
    1.53        }
    1.54 -      else Nil
    1.55      }
    1.56    }
    1.57  
    1.58 @@ -710,13 +706,16 @@
    1.59  
    1.60    def load(options: Options, dirs: List[Path] = Nil, select_dirs: List[Path] = Nil): T =
    1.61    {
    1.62 -    def load_dir(select: Boolean, dir: Path): List[(String, Info)] =
    1.63 +    def load_dir(select: Boolean, dir: Path): List[(Boolean, Path)] =
    1.64        load_root(select, dir) ::: load_roots(select, dir)
    1.65  
    1.66 -    def load_root(select: Boolean, dir: Path): List[(String, Info)] =
    1.67 -      Parser.parse(options, select, dir)
    1.68 +    def load_root(select: Boolean, dir: Path): List[(Boolean, Path)] =
    1.69 +    {
    1.70 +      val root = dir + ROOT
    1.71 +      if (root.is_file) List((select, root)) else Nil
    1.72 +    }
    1.73  
    1.74 -    def load_roots(select: Boolean, dir: Path): List[(String, Info)] =
    1.75 +    def load_roots(select: Boolean, dir: Path): List[(Boolean, Path)] =
    1.76      {
    1.77        val roots = dir + ROOTS
    1.78        if (roots.is_file) {
    1.79 @@ -729,17 +728,28 @@
    1.80                case ERROR(msg) =>
    1.81                  error(msg + "\nThe error(s) above occurred in session catalog " + roots.toString)
    1.82              }
    1.83 -          info <- load_dir(select, dir1)
    1.84 -        } yield info
    1.85 +          res <- load_dir(select, dir1)
    1.86 +        } yield res
    1.87        }
    1.88        else Nil
    1.89      }
    1.90  
    1.91 -    make(
    1.92 +    val roots =
    1.93        for {
    1.94          (select, dir) <- directories(dirs, select_dirs)
    1.95 -        info <- load_dir(select, check_session_dir(dir))
    1.96 -      } yield info)
    1.97 +        res <- load_dir(select, check_session_dir(dir))
    1.98 +      } yield res
    1.99 +
   1.100 +    val unique_roots =
   1.101 +      ((Map.empty[JFile, (Boolean, Path)] /: roots) { case (m, (select, path)) =>
   1.102 +        val file = path.canonical_file
   1.103 +        m.get(file) match {
   1.104 +          case None => m + (file -> (select, path))
   1.105 +          case Some((select1, path1)) => m + (file -> (select1 || select, path1))
   1.106 +        }
   1.107 +      }).toList.map(_._2)
   1.108 +
   1.109 +    make(unique_roots.flatMap(p => Parser.parse_root(options, p._1, p._2)))
   1.110    }
   1.111  
   1.112