process ROOT files only once, which allows duplicate (or overlapping) session root directories;
authorwenzelm
Wed Oct 04 20:16:53 2017 +0200 (20 months ago)
changeset 66764006deaf5c3dc
parent 66763 0b3fa8e22f22
child 66765 c1dfa973b269
child 66766 19f8385ddfd3
process ROOT files only once, which allows duplicate (or overlapping) session root directories;
NEWS
src/Pure/Thy/sessions.scala
     1.1 --- a/NEWS	Tue Oct 03 20:32:58 2017 +0200
     1.2 +++ b/NEWS	Wed Oct 04 20:16:53 2017 +0200
     1.3 @@ -22,6 +22,13 @@
     1.4  INCOMPATIBILITY, use command 'external_file' within a proper theory
     1.5  context.
     1.6  
     1.7 +* Session root directories may be specified multiple times: each
     1.8 +accessible ROOT file is processed only once. This facilitates
     1.9 +specification of $ISABELLE_HOME_USER/ROOTS or command-line options like
    1.10 +-d or -D for "isabelle build" and "isabelle jedit". Example:
    1.11 +
    1.12 +  isabelle build -D '~~/src/ZF'
    1.13 +
    1.14  
    1.15  *** HOL ***
    1.16  
     2.1 --- a/src/Pure/Thy/sessions.scala	Tue Oct 03 20:32:58 2017 +0200
     2.2 +++ b/src/Pure/Thy/sessions.scala	Wed Oct 04 20:16:53 2017 +0200
     2.3 @@ -624,7 +624,7 @@
     2.4              Session_Entry(pos, a, b, c, d, e, f, g, h, i) }
     2.5      }
     2.6  
     2.7 -    def parse(options: Options, select: Boolean, dir: Path): List[(String, Info)] =
     2.8 +    def parse_root(options: Options, select: Boolean, path: Path): List[(String, Info)] =
     2.9      {
    2.10        def make_info(entry_chapter: String, entry: Session_Entry): (String, Info) =
    2.11        {
    2.12 @@ -659,7 +659,7 @@
    2.13  
    2.14            val info =
    2.15              Info(name, entry_chapter, select, entry.pos, entry.groups,
    2.16 -              dir + Path.explode(entry.path), entry.parent, entry.description, session_options,
    2.17 +              path.dir + Path.explode(entry.path), entry.parent, entry.description, session_options,
    2.18                entry.imports, theories, global_theories, document_files, meta_digest)
    2.19  
    2.20            (name, info)
    2.21 @@ -671,24 +671,20 @@
    2.22          }
    2.23        }
    2.24  
    2.25 -      val root = dir + ROOT
    2.26 -      if (root.is_file) {
    2.27 -        val toks = Token.explode(root_syntax.keywords, File.read(root))
    2.28 -        val start = Token.Pos.file(root.implode)
    2.29 +      val toks = Token.explode(root_syntax.keywords, File.read(path))
    2.30 +      val start = Token.Pos.file(path.implode)
    2.31  
    2.32 -        parse_all(rep(chapter | session_entry), Token.reader(toks, start)) match {
    2.33 -          case Success(result, _) =>
    2.34 -            var entry_chapter = "Unsorted"
    2.35 -            val infos = new mutable.ListBuffer[(String, Info)]
    2.36 -            result.foreach {
    2.37 -              case Chapter(name) => entry_chapter = name
    2.38 -              case entry: Session_Entry => infos += make_info(entry_chapter, entry)
    2.39 -            }
    2.40 -            infos.toList
    2.41 -          case bad => error(bad.toString)
    2.42 -        }
    2.43 +      parse_all(rep(chapter | session_entry), Token.reader(toks, start)) match {
    2.44 +        case Success(result, _) =>
    2.45 +          var entry_chapter = "Unsorted"
    2.46 +          val infos = new mutable.ListBuffer[(String, Info)]
    2.47 +          result.foreach {
    2.48 +            case Chapter(name) => entry_chapter = name
    2.49 +            case entry: Session_Entry => infos += make_info(entry_chapter, entry)
    2.50 +          }
    2.51 +          infos.toList
    2.52 +        case bad => error(bad.toString)
    2.53        }
    2.54 -      else Nil
    2.55      }
    2.56    }
    2.57  
    2.58 @@ -710,13 +706,16 @@
    2.59  
    2.60    def load(options: Options, dirs: List[Path] = Nil, select_dirs: List[Path] = Nil): T =
    2.61    {
    2.62 -    def load_dir(select: Boolean, dir: Path): List[(String, Info)] =
    2.63 +    def load_dir(select: Boolean, dir: Path): List[(Boolean, Path)] =
    2.64        load_root(select, dir) ::: load_roots(select, dir)
    2.65  
    2.66 -    def load_root(select: Boolean, dir: Path): List[(String, Info)] =
    2.67 -      Parser.parse(options, select, dir)
    2.68 +    def load_root(select: Boolean, dir: Path): List[(Boolean, Path)] =
    2.69 +    {
    2.70 +      val root = dir + ROOT
    2.71 +      if (root.is_file) List((select, root)) else Nil
    2.72 +    }
    2.73  
    2.74 -    def load_roots(select: Boolean, dir: Path): List[(String, Info)] =
    2.75 +    def load_roots(select: Boolean, dir: Path): List[(Boolean, Path)] =
    2.76      {
    2.77        val roots = dir + ROOTS
    2.78        if (roots.is_file) {
    2.79 @@ -729,17 +728,28 @@
    2.80                case ERROR(msg) =>
    2.81                  error(msg + "\nThe error(s) above occurred in session catalog " + roots.toString)
    2.82              }
    2.83 -          info <- load_dir(select, dir1)
    2.84 -        } yield info
    2.85 +          res <- load_dir(select, dir1)
    2.86 +        } yield res
    2.87        }
    2.88        else Nil
    2.89      }
    2.90  
    2.91 -    make(
    2.92 +    val roots =
    2.93        for {
    2.94          (select, dir) <- directories(dirs, select_dirs)
    2.95 -        info <- load_dir(select, check_session_dir(dir))
    2.96 -      } yield info)
    2.97 +        res <- load_dir(select, check_session_dir(dir))
    2.98 +      } yield res
    2.99 +
   2.100 +    val unique_roots =
   2.101 +      ((Map.empty[JFile, (Boolean, Path)] /: roots) { case (m, (select, path)) =>
   2.102 +        val file = path.canonical_file
   2.103 +        m.get(file) match {
   2.104 +          case None => m + (file -> (select, path))
   2.105 +          case Some((select1, path1)) => m + (file -> (select1 || select, path1))
   2.106 +        }
   2.107 +      }).toList.map(_._2)
   2.108 +
   2.109 +    make(unique_roots.flatMap(p => Parser.parse_root(options, p._1, p._2)))
   2.110    }
   2.111  
   2.112