tuned signature;
authorwenzelm
Tue Oct 31 16:42:20 2017 +0100 (18 months ago)
changeset 66960d62f1f03868a
parent 66959 015d47486fc8
child 66961 f855f9aed72f
tuned signature;
src/Pure/Thy/sessions.scala
     1.1 --- a/src/Pure/Thy/sessions.scala	Tue Oct 31 15:55:50 2017 +0100
     1.2 +++ b/src/Pure/Thy/sessions.scala	Tue Oct 31 16:42:20 2017 +0100
     1.3 @@ -438,7 +438,7 @@
     1.4      }
     1.5    }
     1.6  
     1.7 -  def make(infos: Traversable[(String, Info)]): T =
     1.8 +  def make(infos: List[Info]): T =
     1.9    {
    1.10      def add_edges(graph: Graph[String, Info], kind: String, edges: Info => Traversable[String])
    1.11        : Graph[String, Info] =
    1.12 @@ -464,11 +464,11 @@
    1.13  
    1.14      val graph0 =
    1.15        (Graph.string[Info] /: infos) {
    1.16 -        case (graph, (name, info)) =>
    1.17 -          if (graph.defined(name))
    1.18 -            error("Duplicate session " + quote(name) + Position.here(info.pos) +
    1.19 -              Position.here(graph.get_node(name).pos))
    1.20 -          else graph.new_node(name, info)
    1.21 +        case (graph, info) =>
    1.22 +          if (graph.defined(info.name))
    1.23 +            error("Duplicate session " + quote(info.name) + Position.here(info.pos) +
    1.24 +              Position.here(graph.get_node(info.name).pos))
    1.25 +          else graph.new_node(info.name, info)
    1.26        }
    1.27      val graph1 = add_edges(graph0, "parent", _.parent)
    1.28      val graph2 = add_edges(graph1, "imports", _.imports)
    1.29 @@ -637,9 +637,9 @@
    1.30      for (entry <- Parser.parse_root(path) if entry.isInstanceOf[Session_Entry])
    1.31      yield entry.asInstanceOf[Session_Entry]
    1.32  
    1.33 -  def read_root(options: Options, select: Boolean, path: Path): List[(String, Info)] =
    1.34 +  def read_root(options: Options, select: Boolean, path: Path): List[Info] =
    1.35    {
    1.36 -    def make_info(entry_chapter: String, entry: Session_Entry): (String, Info) =
    1.37 +    def make_info(entry_chapter: String, entry: Session_Entry): Info =
    1.38      {
    1.39        try {
    1.40          val name = entry.name
    1.41 @@ -674,12 +674,9 @@
    1.42            SHA1.digest((entry_chapter, name, entry.parent, entry.options, entry.imports,
    1.43              entry.theories_no_position, conditions, entry.document_files).toString)
    1.44  
    1.45 -        val info =
    1.46 -          Info(name, entry_chapter, select, entry.pos, entry.groups,
    1.47 -            path.dir + Path.explode(entry.path), entry.parent, entry.description, session_options,
    1.48 -            entry.imports, theories, global_theories, document_files, meta_digest)
    1.49 -
    1.50 -        (name, info)
    1.51 +        Info(name, entry_chapter, select, entry.pos, entry.groups,
    1.52 +          path.dir + Path.explode(entry.path), entry.parent, entry.description, session_options,
    1.53 +          entry.imports, theories, global_theories, document_files, meta_digest)
    1.54        }
    1.55        catch {
    1.56          case ERROR(msg) =>
    1.57 @@ -689,7 +686,7 @@
    1.58      }
    1.59  
    1.60      var entry_chapter = "Unsorted"
    1.61 -    val infos = new mutable.ListBuffer[(String, Info)]
    1.62 +    val infos = new mutable.ListBuffer[Info]
    1.63      parse_root(path).foreach {
    1.64        case Chapter(name) => entry_chapter = name
    1.65        case entry: Session_Entry => infos += make_info(entry_chapter, entry)