# HG changeset patch # User wenzelm # Date 1509479864 -3600 # Node ID e365c91c72a9e3ff80443f950d1b30d6ab47bbf5 # Parent f3f9a492bee66b504ecb03ca63e43164986e63bc synthesize session with all required theories from other session imports; diff -r f3f9a492bee6 -r e365c91c72a9 src/Pure/Thy/sessions.scala --- a/src/Pure/Thy/sessions.scala Tue Oct 31 19:29:24 2017 +0100 +++ b/src/Pure/Thy/sessions.scala Tue Oct 31 20:57:44 2017 +0100 @@ -123,8 +123,9 @@ def platform_path: Base = copy(known = known.platform_path) def standard_path: Base = copy(known = known.standard_path) - def theory_qualifier(name: Document.Node.Name): String = - global_theories.getOrElse(name.theory, Long_Name.qualifier(name.theory)) + def theory_qualifier(name: String): String = + global_theories.getOrElse(name, Long_Name.qualifier(name)) + def theory_qualifier(name: Document.Node.Name): String = theory_qualifier(name.theory) def loaded_theory(name: String): Boolean = loaded_theories.defined(name) def loaded_theory(name: Document.Node.Name): Boolean = loaded_theory(name.theory) @@ -349,6 +350,42 @@ def errors: List[String] = deps.errors def check_base: Base = if (errors.isEmpty) base else error(cat_lines(errors)) + + def imported_session: Option[Info] = + { + val info = sessions(session) + + val parent_loaded = + info.parent match { + case Some(parent) => deps(parent).loaded_theories.defined(_) + case None => (_: String) => false + } + val imported_theories = + for { + thy <- base.loaded_theories.keys + if !parent_loaded(thy) && base.theory_qualifier(thy) != session + } + yield (List.empty[Options.Spec], List(((thy, Position.none), false))) + + if (imported_theories.isEmpty) None + else + Some( + make_info(info.options, + dir_selected = false, + dir = info.dir, + chapter = info.chapter, + Session_Entry( + pos = info.pos, + name = info.name + "(base)", + groups = info.groups, + path = ".", + parent = info.parent, + description = "All required theories from other session imports", + options = Nil, + imports = info.imports, + theories = imported_theories, + document_files = Nil))) + } } @@ -375,6 +412,53 @@ def timeout: Time = Time.seconds(options.real("timeout") * options.real("timeout_scale")) } + def make_info(options: Options, dir_selected: Boolean, dir: Path, chapter: String, + entry: Session_Entry): Info = + { + try { + val name = entry.name + + if (name == "" || name == DRAFT) error("Bad session name") + if (is_pure(name) && entry.parent.isDefined) error("Illegal parent session") + if (!is_pure(name) && !entry.parent.isDefined) error("Missing parent session") + + val session_options = options ++ entry.options + + val theories = + entry.theories.map({ case (opts, thys) => (session_options ++ opts, thys.map(_._1)) }) + + val global_theories = + for { (_, thys) <- entry.theories; ((thy, pos), global) <- thys if global } + yield { + val thy_name = Path.explode(thy).expand.base_name + if (Long_Name.is_qualified(thy_name)) + error("Bad qualified name for global theory " + + quote(thy_name) + Position.here(pos)) + else thy_name + } + + val conditions = + theories.flatMap(thys => space_explode(',', thys._1.string("condition"))).distinct.sorted. + map(x => (x, Isabelle_System.getenv(x) != "")) + + val document_files = + entry.document_files.map({ case (s1, s2) => (Path.explode(s1), Path.explode(s2)) }) + + val meta_digest = + SHA1.digest((name, chapter, entry.parent, entry.options, entry.imports, + entry.theories_no_position, conditions, entry.document_files).toString) + + Info(name, chapter, dir_selected, entry.pos, entry.groups, + dir + Path.explode(entry.path), entry.parent, entry.description, session_options, + entry.imports, theories, global_theories, document_files, meta_digest) + } + catch { + case ERROR(msg) => + error(msg + "\nThe error(s) above occurred in session entry " + + quote(entry.name) + Position.here(entry.pos)) + } + } + object Selection { val empty: Selection = Selection() @@ -641,57 +725,12 @@ def read_root(options: Options, select: Boolean, path: Path): List[Info] = { - def make_info(entry_chapter: String, entry: Session_Entry): Info = - { - try { - val name = entry.name - - if (name == "" || name == DRAFT) error("Bad session name") - if (is_pure(name) && entry.parent.isDefined) error("Illegal parent session") - if (!is_pure(name) && !entry.parent.isDefined) error("Missing parent session") - - val session_options = options ++ entry.options - - val theories = - entry.theories.map({ case (opts, thys) => (session_options ++ opts, thys.map(_._1)) }) - - val global_theories = - for { (_, thys) <- entry.theories; ((thy, pos), global) <- thys if global } - yield { - val thy_name = Path.explode(thy).expand.base_name - if (Long_Name.is_qualified(thy_name)) - error("Bad qualified name for global theory " + - quote(thy_name) + Position.here(pos)) - else thy_name - } - - val conditions = - theories.flatMap(thys => space_explode(',', thys._1.string("condition"))).distinct.sorted. - map(x => (x, Isabelle_System.getenv(x) != "")) - - val document_files = - entry.document_files.map({ case (s1, s2) => (Path.explode(s1), Path.explode(s2)) }) - - val meta_digest = - SHA1.digest((entry_chapter, name, entry.parent, entry.options, entry.imports, - entry.theories_no_position, conditions, entry.document_files).toString) - - Info(name, entry_chapter, select, entry.pos, entry.groups, - path.dir + Path.explode(entry.path), entry.parent, entry.description, session_options, - entry.imports, theories, global_theories, document_files, meta_digest) - } - catch { - case ERROR(msg) => - error(msg + "\nThe error(s) above occurred in session entry " + - quote(entry.name) + Position.here(entry.pos)) - } - } - var entry_chapter = "Unsorted" val infos = new mutable.ListBuffer[Info] parse_root(path).foreach { case Chapter(name) => entry_chapter = name - case entry: Session_Entry => infos += make_info(entry_chapter, entry) + case entry: Session_Entry => + infos += make_info(options, select, path.dir, entry_chapter, entry) } infos.toList }