src/Pure/Thy/sessions.scala

 
 import scala.collection.immutable.{SortedSet, SortedMap}
 import scala.collection.mutable
 
 
-object Sessions
-{
+object Sessions {
   /* session and theory names */
 
   val ROOTS: Path = Path.explode("ROOTS")
   val ROOT: Path = Path.explode("ROOT")
 

     name == root_name || name == "README" || name == "index" || name == "bib"
 
 
   /* ROOTS file format */
 
-  class File_Format extends isabelle.File_Format
-  {
+  class File_Format extends isabelle.File_Format {
     val format_name: String = roots_name
     val file_ext = ""
 
     override def detect(name: String): Boolean =
       Thy_Header.split_file_name(name) match {

     known_loaded_files: Map[String, List[Path]] = Map.empty,
     overall_syntax: Outer_Syntax = Outer_Syntax.empty,
     imported_sources: List[(Path, SHA1.Digest)] = Nil,
     sources: List[(Path, SHA1.Digest)] = Nil,
     session_graph_display: Graph_Display.Graph = Graph_Display.empty_graph,
-    errors: List[String] = Nil)
-  {
+    errors: List[String] = Nil
+  ) {
     override def toString: String =
       "Sessions.Base(loaded_theories = " + loaded_theories.size +
         ", used_theories = " + used_theories.length + ")"
 
     def theory_qualifier(name: String): String =

 
     def node_syntax(nodes: Document.Nodes, name: Document.Node.Name): Outer_Syntax =
       nodes(name).syntax orElse loaded_theory_syntax(name) getOrElse overall_syntax
   }
 
-  sealed case class Deps(sessions_structure: Structure, session_bases: Map[String, Base])
-  {
+  sealed case class Deps(sessions_structure: Structure, session_bases: Map[String, Base]) {
     override def toString: String = "Sessions.Deps(" + sessions_structure + ")"
 
     def is_empty: Boolean = session_bases.isEmpty
     def apply(name: String): Base = session_bases(name)
     def get(name: String): Option[Base] = session_bases.get(name)

         case errs => error(cat_lines(errs))
       }
   }
 
   def deps(sessions_structure: Structure,
-      progress: Progress = new Progress,
-      inlined_files: Boolean = false,
-      verbose: Boolean = false,
-      list_files: Boolean = false,
-      check_keywords: Set[String] = Set.empty): Deps =
-  {
+    progress: Progress = new Progress,
+    inlined_files: Boolean = false,
+    verbose: Boolean = false,
+    list_files: Boolean = false,
+    check_keywords: Set[String] = Set.empty
+  ): Deps = {
     var cache_sources = Map.empty[JFile, SHA1.Digest]
-    def check_sources(paths: List[Path]): List[(Path, SHA1.Digest)] =
-    {
+    def check_sources(paths: List[Path]): List[(Path, SHA1.Digest)] = {
       for {
         path <- paths
         file = path.file
         if cache_sources.isDefinedAt(file) || file.isFile
       }

             if (check_keywords.nonEmpty) {
               Check_Keywords.check_keywords(
                 progress, overall_syntax.keywords, check_keywords, theory_files)
             }
 
-            val session_graph_display: Graph_Display.Graph =
-            {
+            val session_graph_display: Graph_Display.Graph = {
               def session_node(name: String): Graph_Display.Node =
                 Graph_Display.Node("[" + name + "]", "session." + name)
 
-              def node(name: Document.Node.Name): Graph_Display.Node =
-              {
+              def node(name: Document.Node.Name): Graph_Display.Node = {
                 val qualifier = deps_base.theory_qualifier(name)
                 if (qualifier == info.name)
                   Graph_Display.Node(name.theory_base_name, "theory." + name.theory)
                 else session_node(qualifier)
               }

               dependencies.entries.iterator.map(entry => entry.name.theory -> entry).
                 foldLeft(deps_base.known_theories)(_ + _)
 
             val known_loaded_files = deps_base.known_loaded_files ++ loaded_files
 
-            val import_errors =
-            {
+            val import_errors = {
               val known_sessions =
                 sessions_structure.imports_requirements(List(session_name)).toSet
               for {
                 name <- dependencies.theories
                 qualifier = deps_base.theory_qualifier(name)

                   }
               })
             val document_theories =
               info.document_theories.map({ case (thy, _) => known_theories(thy).name })
 
-            val dir_errors =
-            {
+            val dir_errors = {
               val ok = info.dirs.map(_.canonical_file).toSet
               val bad =
                 (for {
                   name <- session_theories.iterator
                   path = name.master_dir_path

   sealed case class Base_Info(
     session: String,
     sessions_structure: Structure,
     errors: List[String],
     base: Base,
-    infos: List[Info])
-  {
+    infos: List[Info]
+  ) {
     def check: Base_Info = if (errors.isEmpty) this else error(cat_lines(errors))
   }
 
   def base_info(options: Options,
     session: String,
     progress: Progress = new Progress,
     dirs: List[Path] = Nil,
     include_sessions: List[String] = Nil,
     session_ancestor: Option[String] = None,
-    session_requirements: Boolean = false): Base_Info =
-  {
+    session_requirements: Boolean = false
+  ): Base_Info = {
     val full_sessions = load_structure(options, dirs = dirs)
 
     val selected_sessions =
       full_sessions.selection(Selection(sessions = session :: session_ancestor.toList))
     val info = selected_sessions(session)

     theories: List[(Options, List[(String, Position.T)])],
     global_theories: List[String],
     document_theories: List[(String, Position.T)],
     document_files: List[(Path, Path)],
     export_files: List[(Path, Int, List[String])],
-    meta_digest: SHA1.Digest)
-  {
+    meta_digest: SHA1.Digest
+  ) {
     def chapter_session: String = chapter + "/" + name
 
     def relative_path(info1: Info): String =
       if (name == info1.name) ""
       else if (chapter == info1.chapter) "../" + info1.name + "/"
       else "../../" + info1.chapter_session + "/"
 
     def deps: List[String] = parent.toList ::: imports
 
-    def deps_base(session_bases: String => Base): Base =
-    {
+    def deps_base(session_bases: String => Base): Base = {
       val parent_base = session_bases(parent.getOrElse(""))
       val imports_bases = imports.map(session_bases)
       parent_base.copy(
         known_theories =
           (for {

         case "" | "false" => false
         case "pdf" | "true" => true
         case doc => error("Bad document specification " + quote(doc))
       }
 
-    def document_variants: List[Document_Build.Document_Variant] =
-    {
+    def document_variants: List[Document_Build.Document_Variant] = {
       val variants =
         Library.space_explode(':', options.string("document_variants")).
           map(Document_Build.Document_Variant.parse)
 
       val dups = Library.duplicates(variants.map(_.name))
       if (dups.nonEmpty) error("Duplicate document variants: " + commas_quote(dups))
 
       variants
     }
 
-    def documents: List[Document_Build.Document_Variant] =
-    {
+    def documents: List[Document_Build.Document_Variant] = {
       val variants = document_variants
       if (!document_enabled || document_files.isEmpty) Nil else variants
     }
 
     def document_output: Option[Path] =

 
     def is_afp: Boolean = chapter == AFP.chapter
     def is_afp_bulky: Boolean = is_afp && groups.exists(AFP.groups_bulky.contains)
   }
 
-  def make_info(options: Options, dir_selected: Boolean, dir: Path, chapter: String,
-    entry: Session_Entry): Info =
-  {
+  def make_info(
+    options: Options,
+    dir_selected: Boolean,
+    dir: Path,
+    chapter: String,
+    entry: Session_Entry
+  ): Info = {
     try {
       val name = entry.name
 
       if (exclude_session(name)) error("Bad session name")
       if (is_pure(name) && entry.parent.isDefined) error("Illegal parent session")

         error(msg + "\nThe error(s) above occurred in session entry " +
           quote(entry.name) + Position.here(entry.pos))
     }
   }
 
-  object Selection
-  {
+  object Selection {
     val empty: Selection = Selection()
     val all: Selection = Selection(all_sessions = true)
     def session(session: String): Selection = Selection(sessions = List(session))
   }
 

     all_sessions: Boolean = false,
     base_sessions: List[String] = Nil,
     exclude_session_groups: List[String] = Nil,
     exclude_sessions: List[String] = Nil,
     session_groups: List[String] = Nil,
-    sessions: List[String] = Nil)
-  {
+    sessions: List[String] = Nil
+  ) {
     def ++ (other: Selection): Selection =
       Selection(
         requirements = requirements || other.requirements,
         all_sessions = all_sessions || other.all_sessions,
         base_sessions = Library.merge(base_sessions, other.base_sessions),

         exclude_sessions = Library.merge(exclude_sessions, other.exclude_sessions),
         session_groups = Library.merge(session_groups, other.session_groups),
         sessions = Library.merge(sessions, other.sessions))
   }
 
-  object Structure
-  {
+  object Structure {
     val empty: Structure = make(Nil)
 
-    def make(infos: List[Info]): Structure =
-    {
-      def add_edges(graph: Graph[String, Info], kind: String, edges: Info => Iterable[String])
-        : Graph[String, Info] =
-      {
-        def add_edge(pos: Position.T, name: String, g: Graph[String, Info], parent: String) =
-        {
+    def make(infos: List[Info]): Structure = {
+      def add_edges(
+        graph: Graph[String, Info],
+        kind: String,
+        edges: Info => Iterable[String]
+      ) : Graph[String, Info] = {
+        def add_edge(pos: Position.T, name: String, g: Graph[String, Info], parent: String) = {
           if (!g.defined(parent))
             error("Bad " + kind + " session " + quote(parent) + " for " +
               quote(name) + Position.here(pos))
 
           try { g.add_edge_acyclic(parent, name) }

         session_positions, session_directories, global_theories, build_graph, imports_graph)
     }
   }
 
   final class Structure private[Sessions](
-      val session_positions: List[(String, Position.T)],
-      val session_directories: Map[JFile, String],
-      val global_theories: Map[String, String],
-      val build_graph: Graph[String, Info],
-      val imports_graph: Graph[String, Info])
-  {
+    val session_positions: List[(String, Position.T)],
+    val session_directories: Map[JFile, String],
+    val global_theories: Map[String, String],
+    val build_graph: Graph[String, Info],
+    val imports_graph: Graph[String, Info]
+  ) {
     sessions_structure =>
 
     def bootstrap: Base =
       Base(
         session_directories = session_directories,

     def get(name: String): Option[Info] = if (defined(name)) Some(apply(name)) else None
 
     def theory_qualifier(name: String): String =
       global_theories.getOrElse(name, Long_Name.qualifier(name))
 
-    def check_sessions(names: List[String]): Unit =
-    {
+    def check_sessions(names: List[String]): Unit = {
       val bad_sessions = SortedSet(names.filterNot(defined): _*).toList
       if (bad_sessions.nonEmpty)
         error("Undefined session(s): " + commas_quote(bad_sessions))
     }
 
     def check_sessions(sel: Selection): Unit =
       check_sessions(sel.base_sessions ::: sel.exclude_sessions ::: sel.sessions)
 
-    private def selected(graph: Graph[String, Info], sel: Selection): List[String] =
-    {
+    private def selected(graph: Graph[String, Info], sel: Selection): List[String] = {
       check_sessions(sel)
 
       val select_group = sel.session_groups.toSet
       val select_session = sel.sessions.toSet ++ imports_graph.all_succs(sel.base_sessions)
 

 
       if (sel.requirements) (graph.all_preds(selected0).toSet -- selected0).toList
       else selected0
     }
 
-    def selection(sel: Selection): Structure =
-    {
+    def selection(sel: Selection): Structure = {
       check_sessions(sel)
 
-      val excluded =
-      {
+      val excluded = {
         val exclude_group = sel.exclude_session_groups.toSet
         val exclude_group_sessions =
           (for {
             (name, (info, _)) <- imports_graph.iterator
             if imports_graph.get_node(name).groups.exists(exclude_group)
           } yield name).toList
         imports_graph.all_succs(exclude_group_sessions ::: sel.exclude_sessions).toSet
       }
 
-      def restrict(graph: Graph[String, Info]): Graph[String, Info] =
-      {
+      def restrict(graph: Graph[String, Info]): Graph[String, Info] = {
         val sessions = graph.all_preds(selected(graph, sel)).filterNot(excluded)
         graph.restrict(graph.all_preds(sessions).toSet)
       }
 
       new Structure(

     def selection_deps(
       selection: Selection,
       progress: Progress = new Progress,
       loading_sessions: Boolean = false,
       inlined_files: Boolean = false,
-      verbose: Boolean = false): Deps =
-    {
+      verbose: Boolean = false
+    ): Deps = {
       val deps =
         Sessions.deps(sessions_structure.selection(selection),
           progress = progress, inlined_files = inlined_files, verbose = verbose)
 
       if (loading_sessions) {

     imports: List[String],
     directories: List[String],
     theories: List[(List[Options.Spec], List[((String, Position.T), Boolean)])],
     document_theories: List[(String, Position.T)],
     document_files: List[(String, String)],
-    export_files: List[(String, Int, List[String])]) extends Entry
-  {
+    export_files: List[(String, Int, List[String])]
+  ) extends Entry {
     def theories_no_position: List[(List[Options.Spec], List[(String, Boolean)])] =
       theories.map({ case (a, b) => (a, b.map({ case ((c, _), d) => (c, d) })) })
     def document_theories_no_position: List[String] =
       document_theories.map(_._1)
   }
 
-  private object Parser extends Options.Parser
-  {
-    private val chapter: Parser[Chapter] =
-    {
+  private object Parser extends Options.Parser {
+    private val chapter: Parser[Chapter] = {
       val chapter_name = atom("chapter name", _.is_name)
 
       command(CHAPTER) ~! chapter_name ^^ { case _ ~ a => Chapter(a) }
     }
 
-    private val session_entry: Parser[Session_Entry] =
-    {
+    private val session_entry: Parser[Session_Entry] = {
       val option =
         option_name ~ opt($$$("=") ~! option_value ^^ { case _ ~ x => x }) ^^
           { case x ~ y => (x, y) }
       val options = $$$("[") ~> rep1sep(option, $$$(",")) <~ $$$("]")
 

               rep(export_files)))) ^^
         { case _ ~ ((a, pos) ~ b ~ c ~ (_ ~ (d ~ e ~ f ~ g ~ h ~ i ~ j ~ k ~ l))) =>
             Session_Entry(pos, a, b, c, d, e, f, g, h, i, j, k, l) }
     }
 
-    def parse_root(path: Path): List[Entry] =
-    {
+    def parse_root(path: Path): List[Entry] = {
       val toks = Token.explode(root_syntax.keywords, File.read(path))
       val start = Token.Pos.file(path.implode)
 
       parse_all(rep(chapter | session_entry), Token.reader(toks, start)) match {
         case Success(result, _) => result

 
   def parse_root_entries(path: Path): List[Session_Entry] =
     for (entry <- Parser.parse_root(path) if entry.isInstanceOf[Session_Entry])
     yield entry.asInstanceOf[Session_Entry]
 
-  def read_root(options: Options, select: Boolean, path: Path): List[Info] =
-  {
+  def read_root(options: Options, select: Boolean, path: Path): List[Info] = {
     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(options, select, path.dir, entry_chapter, entry)
     }
     infos.toList
   }
 
-  def parse_roots(roots: Path): List[String] =
-  {
+  def parse_roots(roots: Path): List[String] = {
     for {
       line <- split_lines(File.read(roots))
       if !(line == "" || line.startsWith("#"))
     } yield line
   }

 
   def check_session_dir(dir: Path): Path =
     if (is_session_dir(dir)) File.pwd() + dir.expand
     else error("Bad session root directory (missing ROOT or ROOTS): " + dir.expand.toString)
 
-  def directories(dirs: List[Path], select_dirs: List[Path]): List[(Boolean, Path)] =
-  {
+  def directories(dirs: List[Path], select_dirs: List[Path]): List[(Boolean, Path)] = {
     val default_dirs = Components.directories().filter(is_session_dir)
     for { (select, dir) <- (default_dirs ::: dirs).map((false, _)) ::: select_dirs.map((true, _)) }
     yield (select, dir.canonical)
   }
 
-  def load_structure(options: Options,
+  def load_structure(
+    options: Options,
     dirs: List[Path] = Nil,
     select_dirs: List[Path] = Nil,
-    infos: List[Info] = Nil): Structure =
-  {
+    infos: List[Info] = Nil
+  ): Structure = {
     def load_dir(select: Boolean, dir: Path): List[(Boolean, Path)] =
       load_root(select, dir) ::: load_roots(select, dir)
 
-    def load_root(select: Boolean, dir: Path): List[(Boolean, Path)] =
-    {
+    def load_root(select: Boolean, dir: Path): List[(Boolean, Path)] = {
       val root = dir + ROOT
       if (root.is_file) List((select, root)) else Nil
     }
 
-    def load_roots(select: Boolean, dir: Path): List[(Boolean, Path)] =
-    {
+    def load_roots(select: Boolean, dir: Path): List[(Boolean, Path)] = {
       val roots = dir + ROOTS
       if (roots.is_file) {
         for {
           entry <- parse_roots(roots)
           dir1 =

 
 
   /* Isabelle tool wrapper */
 
   val isabelle_tool = Isabelle_Tool("sessions", "explore structure of Isabelle sessions",
-    Scala_Project.here, args =>
-  {
+    Scala_Project.here, args => {
     var base_sessions: List[String] = Nil
     var select_dirs: List[Path] = Nil
     var requirements = false
     var exclude_session_groups: List[String] = Nil
     var all_sessions = false

 
   /** heap file with SHA1 digest **/
 
   private val sha1_prefix = "SHA1:"
 
-  def read_heap_digest(heap: Path): Option[String] =
-  {
+  def read_heap_digest(heap: Path): Option[String] = {
     if (heap.is_file) {
-      using(FileChannel.open(heap.java_path, StandardOpenOption.READ))(file =>
-      {
+      using(FileChannel.open(heap.java_path, StandardOpenOption.READ))(file => {
         val len = file.size
         val n = sha1_prefix.length + SHA1.digest_length
         if (len >= n) {
           file.position(len - n)
 

 
 
 
   /** persistent store **/
 
-  object Session_Info
-  {
+  object Session_Info {
     val session_name = SQL.Column.string("session_name").make_primary_key
 
     // Build_Log.Session_Info
     val session_timing = SQL.Column.bytes("session_timing")
     val command_timings = SQL.Column.bytes("command_timings")

     val table = SQL.Table("isabelle_session_info", build_log_columns ::: build_columns)
   }
 
   class Database_Context private[Sessions](
     val store: Sessions.Store,
-    database_server: Option[SQL.Database]) extends AutoCloseable
-  {
+    database_server: Option[SQL.Database]
+  ) extends AutoCloseable {
     def cache: Term.Cache = store.cache
 
     def close(): Unit = database_server.foreach(_.close())
 
     def output_database[A](session: String)(f: SQL.Database => A): A =

             case None => None
           }
       }
 
     def read_export(
-      sessions: List[String], theory_name: String, name: String): Option[Export.Entry] =
-    {
+      sessions: List[String],
+      theory_name: String,
+      name: String
+    ): Option[Export.Entry] = {
       val attempts =
         database_server match {
           case Some(db) =>
             sessions.view.map(session_name =>
               Export.read_entry(db, store.cache, session_name, theory_name, name))

     def get_export(
         session_hierarchy: List[String], theory_name: String, name: String): Export.Entry =
       read_export(session_hierarchy, theory_name, name) getOrElse
         Export.empty_entry(theory_name, name)
 
-    override def toString: String =
-    {
+    override def toString: String = {
       val s =
         database_server match {
           case Some(db) => db.toString
           case None => "input_dirs = " + store.input_dirs.map(_.absolute).mkString(", ")
         }

   }
 
   def store(options: Options, cache: Term.Cache = Term.Cache.make()): Store =
     new Store(options, cache)
 
-  class Store private[Sessions](val options: Options, val cache: Term.Cache)
-  {
+  class Store private[Sessions](val options: Options, val cache: Term.Cache) {
     store =>
 
     override def toString: String = "Store(output_dir = " + output_dir.absolute + ")"
 
 

         ssh_close = true)
 
     def open_database_context(): Database_Context =
       new Database_Context(store, if (database_server) Some(open_database_server()) else None)
 
-    def try_open_database(name: String, output: Boolean = false): Option[SQL.Database] =
-    {
+    def try_open_database(name: String, output: Boolean = false): Option[SQL.Database] = {
       def check(db: SQL.Database): Option[SQL.Database] =
         if (output || session_info_exists(db)) Some(db) else { db.close(); None }
 
       if (database_server) check(open_database_server())
       else if (output) Some(SQLite.open_database(output_database(name)))

 
     def open_database(name: String, output: Boolean = false): SQL.Database =
       try_open_database(name, output = output) getOrElse
         error("Missing build database for session " + quote(name))
 
-    def clean_output(name: String): (Boolean, Boolean) =
-    {
+    def clean_output(name: String): (Boolean, Boolean) = {
       val relevant_db =
-        database_server &&
-        {
+        database_server && {
           try_open_database(name) match {
             case Some(db) =>
               try {
                 db.transaction {
                   val relevant_db = session_info_defined(db, name)

 
     /* SQL database content */
 
     def read_bytes(db: SQL.Database, name: String, column: SQL.Column): Bytes =
       db.using_statement(Session_Info.table.select(List(column),
-        Session_Info.session_name.where_equal(name)))(stmt =>
-      {
+        Session_Info.session_name.where_equal(name)))(stmt => {
         val res = stmt.execute_query()
         if (!res.next()) Bytes.empty else res.bytes(column)
       })
 
     def read_properties(db: SQL.Database, name: String, column: SQL.Column): List[Properties.T] =
       Properties.uncompress(read_bytes(db, name, column), cache = cache)
 
 
     /* session info */
 
-    def init_session_info(db: SQL.Database, name: String): Unit =
-    {
+    def init_session_info(db: SQL.Database, name: String): Unit = {
       db.transaction {
         db.create_table(Session_Info.table)
         db.using_statement(
           Session_Info.table.delete(Session_Info.session_name.where_equal(name)))(_.execute())
 

           Document_Build.Data.table.delete(
             Document_Build.Data.session_name.where_equal(name)))(_.execute())
       }
     }
 
-    def session_info_exists(db: SQL.Database): Boolean =
-    {
+    def session_info_exists(db: SQL.Database): Boolean = {
       val tables = db.tables
       tables.contains(Session_Info.table.name) &&
       tables.contains(Export.Data.table.name)
     }
 
     def session_info_defined(db: SQL.Database, name: String): Boolean =
       db.transaction {
-        session_info_exists(db) &&
-        {
+        session_info_exists(db) && {
           db.using_statement(
             Session_Info.table.select(List(Session_Info.session_name),
               Session_Info.session_name.where_equal(name)))(stmt => stmt.execute_query().next())
         }
       }
 
     def write_session_info(
       db: SQL.Database,
       name: String,
       build_log: Build_Log.Session_Info,
-      build: Build.Session_Info): Unit =
-    {
+      build: Build.Session_Info
+    ): Unit = {
       db.transaction {
-        db.using_statement(Session_Info.table.insert())(stmt =>
-        {
+        db.using_statement(Session_Info.table.insert())(stmt => {
           stmt.string(1) = name
           stmt.bytes(2) = Properties.encode(build_log.session_timing)
           stmt.bytes(3) = Properties.compress(build_log.command_timings, cache = cache.xz)
           stmt.bytes(4) = Properties.compress(build_log.theory_timings, cache = cache.xz)
           stmt.bytes(5) = Properties.compress(build_log.ml_statistics, cache = cache.xz)

       read_theory_timings(db, name).flatMap(Markup.Name.unapply)
 
     def read_errors(db: SQL.Database, name: String): List[String] =
       Build_Log.uncompress_errors(read_bytes(db, name, Session_Info.errors), cache = cache)
 
-    def read_build(db: SQL.Database, name: String): Option[Build.Session_Info] =
-    {
+    def read_build(db: SQL.Database, name: String): Option[Build.Session_Info] = {
       if (db.tables.contains(Session_Info.table.name)) {
         db.using_statement(Session_Info.table.select(Session_Info.build_columns,
-          Session_Info.session_name.where_equal(name)))(stmt =>
-        {
+          Session_Info.session_name.where_equal(name)))(stmt => {
           val res = stmt.execute_query()
           if (!res.next()) None
           else {
             Some(
               Build.Session_Info(