merged
authorwenzelm
Tue, 17 Nov 2020 22:58:55 +0100
changeset 72875 db5f4572704a
parent 72868 20f70d20e6f8 (current diff)
parent 72874 2a7fc87495e0 (diff)
child 72876 fffad9ad660e
merged
--- a/src/Pure/ML/ml_process.scala	Tue Nov 17 09:57:37 2020 +0000
+++ b/src/Pure/ML/ml_process.scala	Tue Nov 17 22:58:55 2020 +0100
@@ -78,40 +78,16 @@
     val eval_options = if (heaps.isEmpty) Nil else List("Options.load_default ()")
 
     // session base
-    val init_session = Isabelle_System.tmp_file("init_session", ext = "ML")
-    val init_session_name = init_session.getAbsolutePath
+    val init_session = Isabelle_System.tmp_file("init_session")
     Isabelle_System.chmod("600", File.path(init_session))
-    File.write(init_session,
+    val eval_init_session =
       session_base match {
-        case None => ""
+        case None => Nil
         case Some(base) =>
-          def print_symbols: List[(String, Int)] => String =
-            ML_Syntax.print_list(
-              ML_Syntax.print_pair(ML_Syntax.print_string_bytes, ML_Syntax.print_int))
-          def print_table: List[(String, String)] => String =
-            ML_Syntax.print_list(
-              ML_Syntax.print_pair(
-                ML_Syntax.print_string_bytes, ML_Syntax.print_string_bytes))
-          def print_list: List[String] => String =
-            ML_Syntax.print_list(ML_Syntax.print_string_bytes)
-          def print_sessions: List[(String, Position.T)] => String =
-            ML_Syntax.print_list(
-              ML_Syntax.print_pair(ML_Syntax.print_string_bytes, ML_Syntax.print_properties))
-          def print_bibtex_entries: List[(String, List[String])] => String =
-            ML_Syntax.print_list(
-              ML_Syntax.print_pair(ML_Syntax.print_string_bytes,
-                ML_Syntax.print_list(ML_Syntax.print_string_bytes)))
-
-          "Resources.init_session" +
-            "{html_symbols = " + print_symbols(Symbol.codes) +
-            ", session_positions = " + print_sessions(sessions_structure.session_positions) +
-            ", session_directories = " + print_table(sessions_structure.dest_session_directories) +
-            ", session_chapters = " + print_table(sessions_structure.session_chapters) +
-            ", bibtex_entries = " + print_bibtex_entries(sessions_structure.bibtex_entries) +
-            ", docs = " + print_list(base.doc_names) +
-            ", global_theories = " + print_table(base.global_theories.toList) +
-            ", loaded_theories = " + print_list(base.loaded_theories.keys) + "}"
-      })
+          File.write(init_session, new Resources(sessions_structure, base).init_session_yxml)
+          List("Resources.init_session_file (Path.explode " +
+            ML_Syntax.print_string_bytes(File.path(init_session).implode) + ")")
+      }
 
     // process
     val eval_process =
@@ -144,9 +120,7 @@
     // bash
     val bash_args =
       ml_runtime_options :::
-      (eval_init ::: eval_modes ::: eval_options).flatMap(List("--eval", _)) :::
-      List("--use", init_session_name,
-        "--eval", "OS.FileSys.remove " + ML_Syntax.print_string_bytes(init_session_name)) :::
+      (eval_init ::: eval_modes ::: eval_options ::: eval_init_session).flatMap(List("--eval", _)) :::
       use_prelude.flatMap(List("--use", _)) ::: List("--eval", eval_process) ::: args
 
     Bash.process(
--- a/src/Pure/PIDE/protocol.ML	Tue Nov 17 09:57:37 2020 +0000
+++ b/src/Pure/PIDE/protocol.ML	Tue Nov 17 22:58:55 2020 +0100
@@ -25,27 +25,7 @@
 
 val _ =
   Isabelle_Process.protocol_command "Prover.init_session"
-    (fn [html_symbols_yxml, session_positions_yxml, session_directories_yxml, session_chapters_yxml,
-          bibtex_entries_yxml, doc_names_yxml, global_theories_yxml, loaded_theories_yxml] =>
-      let
-        val decode_symbols = YXML.parse_body #> let open XML.Decode in list (pair string int) end;
-        val decode_table = YXML.parse_body #> let open XML.Decode in list (pair string string) end;
-        val decode_list = YXML.parse_body #> let open XML.Decode in list string end;
-        val decode_sessions =
-          YXML.parse_body #> let open XML.Decode in list (pair string properties) end;
-        val decode_bibtex_entries =
-          YXML.parse_body #> let open XML.Decode in list (pair string (list string)) end;
-      in
-        Resources.init_session
-          {html_symbols = decode_symbols html_symbols_yxml,
-           session_positions = decode_sessions session_positions_yxml,
-           session_directories = decode_table session_directories_yxml,
-           session_chapters = decode_table session_chapters_yxml,
-           bibtex_entries = decode_bibtex_entries bibtex_entries_yxml,
-           docs = decode_list doc_names_yxml,
-           global_theories = decode_table global_theories_yxml,
-           loaded_theories = decode_list loaded_theories_yxml}
-      end);
+    (fn [yxml] => Resources.init_session_yxml yxml);
 
 val _ =
   Isabelle_Process.protocol_command "Document.define_blob"
--- a/src/Pure/PIDE/protocol.scala	Tue Nov 17 09:57:37 2020 +0000
+++ b/src/Pure/PIDE/protocol.scala	Tue Nov 17 22:58:55 2020 +0100
@@ -283,33 +283,10 @@
     protocol_command("Prover.options", Symbol.encode_yxml(opts.encode))
 
 
-  /* session base */
-
-  def init_session(resources: Resources)
-  {
-    import XML.Encode._
+  /* resources */
 
-    def encode_symbols(arg: List[(String, Int)]): String =
-      Symbol.encode_yxml(list(pair(string, int))(arg))
-    def encode_table(arg: List[(String, String)]): String =
-      Symbol.encode_yxml(list(pair(string, string))(arg))
-    def encode_list(arg: List[String]): String =
-      Symbol.encode_yxml(list(string)(arg))
-    def encode_sessions(arg: List[(String, Position.T)]): String =
-      Symbol.encode_yxml(list(pair(string, properties))(arg))
-    def encode_bibtex_entries(arg: List[(String, List[String])]): String =
-      Symbol.encode_yxml(list(pair(string, list(string)))(arg))
-
-    protocol_command("Prover.init_session",
-      encode_symbols(Symbol.codes),
-      encode_sessions(resources.sessions_structure.session_positions),
-      encode_table(resources.sessions_structure.dest_session_directories),
-      encode_table(resources.sessions_structure.session_chapters),
-      encode_bibtex_entries(resources.sessions_structure.bibtex_entries),
-      encode_list(resources.session_base.doc_names),
-      encode_table(resources.session_base.global_theories.toList),
-      encode_list(resources.session_base.loaded_theories.keys))
-  }
+  def init_session(resources: Resources): Unit =
+    protocol_command("Prover.init_session", resources.init_session_yxml)
 
 
   /* interned items */
--- a/src/Pure/PIDE/resources.ML	Tue Nov 17 09:57:37 2020 +0000
+++ b/src/Pure/PIDE/resources.ML	Tue Nov 17 22:58:55 2020 +0100
@@ -13,15 +13,19 @@
      session_directories: (string * string) list,
      session_chapters: (string * string) list,
      bibtex_entries: (string * string list) list,
+     command_timings: Properties.T list,
      docs: string list,
      global_theories: (string * string) list,
      loaded_theories: string list} -> unit
+  val init_session_yxml: string -> unit
+  val init_session_file: Path.T -> unit
   val finish_session_base: unit -> unit
   val global_theory: string -> string option
   val loaded_theory: string -> bool
   val html_symbols: unit -> HTML.symbols
   val check_session: Proof.context -> string * Position.T -> string
   val session_chapter: string -> string
+  val last_timing: Toplevel.transition -> Time.time
   val check_doc: Proof.context -> string * Position.T -> string
   val master_directory: theory -> Path.T
   val imports_of: theory -> (string * Position.T) list
@@ -48,6 +52,41 @@
 structure Resources: RESOURCES =
 struct
 
+(* command timings *)
+
+type timings = ((string * Time.time) Inttab.table) Symtab.table;  (*file -> offset -> name, time*)
+
+val empty_timings: timings = Symtab.empty;
+
+fun update_timings props =
+  (case Markup.parse_command_timing_properties props of
+    SOME ({file, offset, name}, time) =>
+      Symtab.map_default (file, Inttab.empty)
+        (Inttab.map_default (offset, (name, time)) (fn (_, t) => (name, t + time)))
+  | NONE => I);
+
+fun make_timings command_timings =
+  fold update_timings command_timings empty_timings;
+
+fun approximative_id name pos =
+  (case (Position.file_of pos, Position.offset_of pos) of
+    (SOME file, SOME offset) =>
+      if name = "" then NONE else SOME {file = file, offset = offset, name = name}
+  | _ => NONE);
+
+fun get_timings timings tr =
+  (case approximative_id (Toplevel.name_of tr) (Toplevel.pos_of tr) of
+    SOME {file, offset, name} =>
+      (case Symtab.lookup timings file of
+        SOME offsets =>
+          (case Inttab.lookup offsets offset of
+            SOME (name', time) => if name = name' then SOME time else NONE
+          | NONE => NONE)
+      | NONE => NONE)
+  | NONE => NONE)
+  |> the_default Time.zeroTime;
+
+
 (* session base *)
 
 val default_qualifier = "Draft";
@@ -63,6 +102,7 @@
    session_directories = Symtab.empty: Path.T list Symtab.table,
    session_chapters = Symtab.empty: string Symtab.table,
    bibtex_entries = Symtab.empty: string list Symtab.table,
+   timings = empty_timings,
    docs = []: (string * entry) list,
    global_theories = Symtab.empty: string Symtab.table,
    loaded_theories = Symtab.empty: unit Symtab.table};
@@ -72,7 +112,7 @@
 
 fun init_session
     {html_symbols, session_positions, session_directories, session_chapters,
-      bibtex_entries, docs, global_theories, loaded_theories} =
+      bibtex_entries, command_timings, docs, global_theories, loaded_theories} =
   Synchronized.change global_session_base
     (fn _ =>
       {html_symbols = HTML.make_symbols html_symbols,
@@ -82,10 +122,39 @@
            session_directories Symtab.empty,
        session_chapters = Symtab.make session_chapters,
        bibtex_entries = Symtab.make bibtex_entries,
+       timings = make_timings command_timings,
        docs = sort_by #1 (map (apsnd make_entry o rpair []) docs),
        global_theories = Symtab.make global_theories,
        loaded_theories = Symtab.make_set loaded_theories});
 
+fun init_session_yxml yxml =
+  let
+    val (html_symbols, (session_positions, (session_directories, (session_chapters,
+          (bibtex_entries, (command_timings, (docs, (global_theories, loaded_theories)))))))) =
+      YXML.parse_body yxml |>
+        let open XML.Decode in
+          pair (list (pair string int))
+            (pair (list (pair string properties))
+              (pair (list (pair string string)) (pair (list (pair string string))
+                (pair (list (pair string (list string))) (pair (list properties)
+                  (pair (list string) (pair (list (pair string string)) (list string))))))))
+        end;
+  in
+    init_session
+      {html_symbols = html_symbols,
+       session_positions = session_positions,
+       session_directories = session_directories,
+       session_chapters = session_chapters,
+       bibtex_entries = bibtex_entries,
+       command_timings = command_timings,
+       docs = docs,
+       global_theories = global_theories,
+       loaded_theories = loaded_theories}
+  end;
+
+fun init_session_file path =
+  init_session_yxml (File.read path) before File.rm path;
+
 fun finish_session_base () =
   Synchronized.change global_session_base
     (fn {global_theories, loaded_theories, ...} =>
@@ -94,6 +163,7 @@
        session_directories = Symtab.empty,
        session_chapters = Symtab.empty,
        bibtex_entries = Symtab.empty,
+       timings = empty_timings,
        docs = [],
        global_theories = global_theories,
        loaded_theories = loaded_theories});
@@ -117,6 +187,8 @@
 fun session_chapter name =
   the_default "Unsorted" (Symtab.lookup (get_session_base #session_chapters) name);
 
+fun last_timing tr = get_timings (get_session_base #timings) tr;
+
 val check_doc = check_name #docs "documentation" (Markup.doc o #1);
 
 
--- a/src/Pure/PIDE/resources.scala	Tue Nov 17 09:57:37 2020 +0000
+++ b/src/Pure/PIDE/resources.scala	Tue Nov 17 22:58:55 2020 +0100
@@ -15,11 +15,39 @@
 class Resources(
   val sessions_structure: Sessions.Structure,
   val session_base: Sessions.Base,
-  val log: Logger = No_Logger)
+  val log: Logger = No_Logger,
+  command_timings: List[Properties.T] = Nil)
 {
   resources =>
 
 
+  /* init session */
+
+  def init_session_yxml: String =
+  {
+    import XML.Encode._
+
+    YXML.string_of_body(
+      pair(list(pair(string, int)),
+      pair(list(pair(string, properties)),
+      pair(list(pair(string, string)),
+      pair(list(pair(string, string)),
+      pair(list(pair(string, list(string))),
+      pair(list(properties),
+      pair(list(string),
+      pair(list(pair(string, string)), list(string)))))))))(
+       (Symbol.codes,
+       (resources.sessions_structure.session_positions,
+       (resources.sessions_structure.dest_session_directories,
+       (resources.sessions_structure.session_chapters,
+       (resources.sessions_structure.bibtex_entries,
+       (command_timings,
+       (resources.session_base.doc_names,
+       (resources.session_base.global_theories.toList,
+        resources.session_base.loaded_theories.keys))))))))))
+  }
+
+
   /* file formats */
 
   def make_theory_name(name: Document.Node.Name): Option[Document.Node.Name] =
--- a/src/Pure/Thy/export.scala	Tue Nov 17 09:57:37 2020 +0000
+++ b/src/Pure/Thy/export.scala	Tue Nov 17 22:58:55 2020 +0100
@@ -75,6 +75,9 @@
 
   def compound_name(a: String, b: String): String = a + ":" + b
 
+  def empty_entry(session_name: String, theory_name: String, name: String): Entry =
+    Entry(session_name, theory_name, name, false, Future.value(false, Bytes.empty))
+
   sealed case class Entry(
     session_name: String,
     theory_name: String,
@@ -182,6 +185,55 @@
   }
 
 
+  /* database context */
+
+  def open_database_context(
+    sessions_structure: Sessions.Structure,
+    store: Sessions.Store): Database_Context =
+  {
+    new Database_Context(sessions_structure, store,
+      if (store.database_server) Some(store.open_database_server()) else None)
+  }
+
+  class Database_Context private[Export](
+    sessions_structure: Sessions.Structure,
+    store: Sessions.Store,
+    database_server: Option[SQL.Database]) extends AutoCloseable
+  {
+    def close { database_server.foreach(_.close) }
+
+    def try_entry(session: String, theory_name: String, name: String): Option[Entry] =
+    {
+      val hierarchy = sessions_structure.build_graph.all_preds(List(session)).view
+      val attempts =
+        database_server match {
+          case Some(db) =>
+            hierarchy.map(session_name => read_entry(db, session_name, theory_name, name))
+          case None =>
+            hierarchy.map(session_name =>
+              store.try_open_database(session_name) match {
+                case Some(db) => using(db)(read_entry(_, session_name, theory_name, name))
+                case None => None
+              })
+        }
+      attempts.collectFirst({ case Some(entry) => entry })
+    }
+
+    def entry(session: String, theory_name: String, name: String): Entry =
+      try_entry(session, theory_name, name) getOrElse empty_entry(session, theory_name, name)
+
+    override def toString: String =
+    {
+      val s =
+        database_server match {
+          case Some(db) => db.toString
+          case None => "input_dirs = " + store.input_dirs.map(_.absolute).mkString(", ")
+        }
+      "Database_Context(" + s + ")"
+    }
+  }
+
+
   /* database consumer thread */
 
   def consumer(db: SQL.Database, cache: XZ.Cache = XZ.cache()): Consumer = new Consumer(db, cache)
@@ -237,6 +289,17 @@
         override def toString: String = "none"
       }
 
+    def database_context(
+        context: Database_Context, session: String, theory_name: String): Provider =
+      new Provider {
+        def apply(export_name: String): Option[Entry] =
+          context.try_entry(session, theory_name, export_name)
+
+        def focus(other_theory: String): Provider = this
+
+        override def toString: String = context.toString
+      }
+
     def database(db: SQL.Database, session_name: String, theory_name: String): Provider =
       new Provider {
         def apply(export_name: String): Option[Entry] =
--- a/src/Pure/Thy/html.ML	Tue Nov 17 09:57:37 2020 +0000
+++ b/src/Pure/Thy/html.ML	Tue Nov 17 22:58:55 2020 +0100
@@ -16,7 +16,6 @@
   val command: symbols -> string -> text
   val href_name: string -> string -> string
   val href_path: Url.T -> string -> string
-  val href_opt_path: Url.T option -> string -> string
   val begin_document: symbols -> string -> text
   val end_document: text
 end;
@@ -120,9 +119,6 @@
 fun href_name s txt = "<a href=" ^ quote s ^ ">" ^ txt ^ "</a>";
 fun href_path path txt = href_name (Url.implode path) txt;
 
-fun href_opt_path NONE txt = txt
-  | href_opt_path (SOME p) txt = href_path p txt;
-
 
 (* document *)
 
--- a/src/Pure/Thy/present.ML	Tue Nov 17 09:57:37 2020 +0000
+++ b/src/Pure/Thy/present.ML	Tue Nov 17 22:58:55 2020 +0100
@@ -41,18 +41,19 @@
     val ((session, chapter), (session', chapter')) = apply2 get_session_chapter (thy, thy');
     val link = html_name thy';
   in
-    if session = session' then SOME link
-    else if chapter = chapter' then SOME (Path.parent + Path.basic session + link)
-    else if chapter = Context.PureN then NONE
-    else SOME (Path.parent + Path.parent + Path.basic chapter + Path.basic session + link)
+    if session = session' then link
+    else if chapter = chapter' then Path.parent + Path.basic session' + link
+    else Path.parent + Path.parent + Path.basic chapter' + Path.basic session' + link
   end;
 
 fun theory_document symbols A Bs body =
   HTML.begin_document symbols ("Theory " ^ A) ^ "\n" ^
   HTML.command symbols "theory" ^ " " ^ HTML.name symbols A ^ "<br/>\n" ^
-  HTML.keyword symbols "imports" ^ " " ^
-    space_implode " " (map (uncurry HTML.href_opt_path o apsnd (HTML.name symbols)) Bs) ^
-  "<br/>\n\n</div>\n<div class=\"source\">\n<pre class=\"source\">" ::
+  (if null Bs then ""
+   else
+    HTML.keyword symbols "imports" ^ " " ^
+      space_implode " " (map (uncurry HTML.href_path o apsnd (HTML.name symbols)) Bs) ^ "<br/>\n") ^
+  "\n</div>\n<div class=\"source\">\n<pre class=\"source\">" ::
   body @ ["</pre>\n", HTML.end_document];
 
 in
@@ -62,7 +63,7 @@
     val name = Context.theory_name thy;
     val parents =
       Theory.parents_of thy |> map (fn thy' =>
-        (Option.map Url.File (theory_link thy thy'), Context.theory_name thy'));
+        (Url.File (theory_link thy thy'), Context.theory_name thy'));
 
     val symbols = Resources.html_symbols ();
     val keywords = Thy_Header.get_keywords thy;
--- a/src/Pure/Thy/present.scala	Tue Nov 17 09:57:37 2020 +0000
+++ b/src/Pure/Thy/present.scala	Tue Nov 17 22:58:55 2020 +0100
@@ -119,10 +119,10 @@
     }
 
     val theories =
-      using(store.open_database(session))(db =>
+      using(Export.open_database_context(deps.sessions_structure, store))(context =>
         for {
           name <- base.session_theories
-          entry <- Export.read_entry(db, session, name.theory, document_html_name(name))
+          entry <- context.try_entry(session, name.theory, document_html_name(name))
         } yield name -> entry.uncompressed(cache = store.xz_cache))
 
     val theories_body =
@@ -265,20 +265,17 @@
     val base = deps(session)
     val graph_pdf = graphview.Graph_File.make_pdf(options, base.session_graph_display)
 
-    def find_tex(name: Document.Node.Name): Option[Bytes] =
-      deps.sessions_structure.build_requirements(List(session)).reverse.view
-        .map(session_name =>
-          using(store.open_database(session_name))(db =>
-            Export.read_entry(db, session_name, name.theory, document_tex_name(name)).
-              map(_.uncompressed(cache = store.xz_cache))))
-        .collectFirst({ case Some(x) => x })
-
 
     /* prepare document directory */
 
     lazy val tex_files =
-      for (name <- base.session_theories ::: base.document_theories)
-        yield Path.basic(tex_name(name)) -> find_tex(name).getOrElse(Bytes.empty)
+      using(Export.open_database_context(deps.sessions_structure, store))(context =>
+        for (name <- base.session_theories ::: base.document_theories)
+        yield {
+          val entry = context.entry(session, name.theory, document_tex_name(name))
+          Path.basic(tex_name(name)) -> entry.uncompressed(cache = store.xz_cache)
+        }
+      )
 
     def prepare_dir(dir: Path, doc_name: String, doc_tags: List[String]): (Path, String) =
     {
--- a/src/Pure/Thy/sessions.scala	Tue Nov 17 09:57:37 2020 +0000
+++ b/src/Pure/Thy/sessions.scala	Tue Nov 17 22:58:55 2020 +0100
@@ -1171,7 +1171,9 @@
 
   class Store private[Sessions](val options: Options)
   {
-    override def toString: String = "Store(output_dir = " + output_dir.expand + ")"
+    store =>
+
+    override def toString: String = "Store(output_dir = " + output_dir.absolute + ")"
 
     val xml_cache: XML.Cache = XML.make_cache()
     val xz_cache: XZ.Cache = XZ.make_cache()
@@ -1227,33 +1229,41 @@
 
     /* database */
 
-    private def database_server: Boolean = options.bool("build_database_server")
+    def database_server: Boolean = options.bool("build_database_server")
 
-    def access_database(name: String, output: Boolean = false): Option[SQL.Database] =
+    def open_database_server(): SQL.Database =
+      PostgreSQL.open_database(
+        user = options.string("build_database_user"),
+        password = options.string("build_database_password"),
+        database = options.string("build_database_name"),
+        host = options.string("build_database_host"),
+        port = options.int("build_database_port"),
+        ssh =
+          options.proper_string("build_database_ssh_host").map(ssh_host =>
+            SSH.open_session(options,
+              host = ssh_host,
+              user = options.string("build_database_ssh_user"),
+              port = options.int("build_database_ssh_port"))),
+        ssh_close = true)
+
+    def try_open_database(name: String, output: Boolean = false): Option[SQL.Database] =
     {
-      if (database_server) {
-        val db =
-          PostgreSQL.open_database(
-            user = options.string("build_database_user"),
-            password = options.string("build_database_password"),
-            database = options.string("build_database_name"),
-            host = options.string("build_database_host"),
-            port = options.int("build_database_port"),
-            ssh =
-              options.proper_string("build_database_ssh_host").map(ssh_host =>
-                SSH.open_session(options,
-                  host = ssh_host,
-                  user = options.string("build_database_ssh_user"),
-                  port = options.int("build_database_ssh_port"))),
-            ssh_close = true)
-        if (output || has_session_info(db, name)) Some(db) else { db.close; None }
+      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)))
+      else {
+        (for {
+          dir <- input_dirs.view
+          path = dir + database(name) if path.is_file
+          db <- check(SQLite.open_database(path))
+        } yield db).headOption
       }
-      else if (output) Some(SQLite.open_database(output_database(name)))
-      else input_dirs.map(_ + database(name)).find(_.is_file).map(SQLite.open_database)
     }
 
     def open_database(name: String, output: Boolean = false): SQL.Database =
-      access_database(name, output = output) getOrElse
+      try_open_database(name, output = output) getOrElse
         error("Missing build database for session " + quote(name))
 
     def clean_output(name: String): (Boolean, Boolean) =
@@ -1261,11 +1271,11 @@
       val relevant_db =
         database_server &&
         {
-          access_database(name) match {
+          try_open_database(name) match {
             case Some(db) =>
               try {
                 db.transaction {
-                  val relevant_db = has_session_info(db, name)
+                  val relevant_db = session_info_defined(db, name)
                   init_session_info(db, name)
                   relevant_db
                 }
@@ -1318,17 +1328,22 @@
       }
     }
 
-    def has_session_info(db: SQL.Database, name: String): 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 {
-        db.tables.contains(Session_Info.table.name) &&
+        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,
--- a/src/Pure/Thy/thy_info.ML	Tue Nov 17 09:57:37 2020 +0000
+++ b/src/Pure/Thy/thy_info.ML	Tue Nov 17 22:58:55 2020 +0100
@@ -18,8 +18,7 @@
   val get_theory: string -> theory
   val master_directory: string -> Path.T
   val remove_thy: string -> unit
-  type context = {options: Options.T, last_timing: Toplevel.transition -> Time.time}
-  val use_theories: context -> string -> (string * Position.T) list -> unit
+  val use_theories: Options.T -> string -> (string * Position.T) list -> unit
   val use_thy: string -> unit
   val script_thy: Position.T -> string -> theory -> theory
   val register_thy: theory -> unit
@@ -180,14 +179,6 @@
 fun update_thy deps theory = change_thys (update deps theory);
 
 
-(* context *)
-
-type context = {options: Options.T, last_timing: Toplevel.transition -> Time.time};
-
-fun default_context (): context =
-  {options = Options.default (), last_timing = K Time.zeroTime};
-
-
 (* scheduling loader tasks *)
 
 datatype result =
@@ -272,12 +263,12 @@
 
 (* eval theory *)
 
-fun excursion keywords master_dir last_timing init elements =
+fun excursion keywords master_dir init elements =
   let
     fun prepare_span st span =
       Command_Span.content span
       |> Command.read keywords (Command.read_thy st) master_dir init ([], ~1)
-      |> (fn tr => Toplevel.timing (last_timing tr) tr);
+      |> (fn tr => Toplevel.timing (Resources.last_timing tr) tr);
 
     fun element_result span_elem (st, _) =
       let
@@ -292,9 +283,8 @@
     val thy = Toplevel.end_theory end_pos end_state;
   in (results, thy) end;
 
-fun eval_thy (context: context) update_time master_dir header text_pos text parents =
+fun eval_thy options update_time master_dir header text_pos text parents =
   let
-    val {options, last_timing} = context;
     val (name, _) = #name header;
     val keywords =
       fold (curry Keyword.merge_keywords o Thy_Header.get_keywords) parents
@@ -306,7 +296,7 @@
     fun init () = Resources.begin_theory master_dir header parents;
     val (results, thy) =
       cond_timeit true ("theory " ^ quote name)
-        (fn () => excursion keywords master_dir last_timing init elements);
+        (fn () => excursion keywords master_dir init elements);
 
     fun present () =
       let
@@ -325,7 +315,7 @@
 fun required_by _ [] = ""
   | required_by s initiators = s ^ "(required by " ^ show_path (rev initiators) ^ ")";
 
-fun load_thy context initiators update_time deps text (name, pos) keywords parents =
+fun load_thy options initiators update_time deps text (name, pos) keywords parents =
   let
     val _ = remove_thy name;
     val _ = writeln ("Loading theory " ^ quote name ^ required_by " " initiators);
@@ -348,7 +338,7 @@
 
     val text_pos = Position.put_id (Document_ID.print exec_id) (Path.position thy_path);
     val (theory, present, weight) =
-      eval_thy context update_time dir header text_pos text
+      eval_thy options update_time dir header text_pos text
         (if name = Context.PureN then [Context.the_global_context ()] else parents);
 
     val timing_result = Timing.result timing_start;
@@ -380,9 +370,9 @@
 
 in
 
-fun require_thys context initiators qualifier dir strs tasks =
-      fold_map (require_thy context initiators qualifier dir) strs tasks |>> forall I
-and require_thy context initiators qualifier dir (s, require_pos) tasks =
+fun require_thys options initiators qualifier dir strs tasks =
+      fold_map (require_thy options initiators qualifier dir) strs tasks |>> forall I
+and require_thy options initiators qualifier dir (s, require_pos) tasks =
   let
     val {master_dir, theory_name, ...} = Resources.import_name qualifier dir s;
   in
@@ -403,7 +393,7 @@
 
           val parents = map (#theory_name o Resources.import_name qualifier' dir' o #1) imports;
           val (parents_current, tasks') =
-            require_thys context (theory_name :: initiators) qualifier' dir' imports tasks;
+            require_thys options (theory_name :: initiators) qualifier' dir' imports tasks;
 
           val all_current = current andalso parents_current;
           val task =
@@ -415,7 +405,7 @@
                   let
                     val update_time = serial ();
                     val load =
-                      load_thy context initiators update_time
+                      load_thy options initiators update_time
                         dep text (theory_name, theory_pos) keywords;
                   in Task (parents, load) end);
 
@@ -428,12 +418,12 @@
 
 (* use theories *)
 
-fun use_theories context qualifier imports =
-  let val (_, tasks) = require_thys context [] qualifier Path.current imports String_Graph.empty
+fun use_theories options qualifier imports =
+  let val (_, tasks) = require_thys options [] qualifier Path.current imports String_Graph.empty
   in if Multithreading.max_threads () > 1 then schedule_futures tasks else schedule_seq tasks end;
 
 fun use_thy name =
-  use_theories (default_context ()) Resources.default_qualifier [(name, Position.none)];
+  use_theories (Options.default ()) Resources.default_qualifier [(name, Position.none)];
 
 
 (* toplevel scripting -- without maintaining database *)
--- a/src/Pure/Tools/build.ML	Tue Nov 17 09:57:37 2020 +0000
+++ b/src/Pure/Tools/build.ML	Tue Nov 17 22:58:55 2020 +0100
@@ -7,38 +7,6 @@
 structure Build: sig end =
 struct
 
-(* command timings *)
-
-type timings = ((string * Time.time) Inttab.table) Symtab.table;  (*file -> offset -> name, time*)
-
-val empty_timings: timings = Symtab.empty;
-
-fun update_timings props =
-  (case Markup.parse_command_timing_properties props of
-    SOME ({file, offset, name}, time) =>
-      Symtab.map_default (file, Inttab.empty)
-        (Inttab.map_default (offset, (name, time)) (fn (_, t) => (name, t + time)))
-  | NONE => I);
-
-fun approximative_id name pos =
-  (case (Position.file_of pos, Position.offset_of pos) of
-    (SOME file, SOME offset) =>
-      if name = "" then NONE else SOME {file = file, offset = offset, name = name}
-  | _ => NONE);
-
-fun get_timings timings tr =
-  (case approximative_id (Toplevel.name_of tr) (Toplevel.pos_of tr) of
-    SOME {file, offset, name} =>
-      (case Symtab.lookup timings file of
-        SOME offsets =>
-          (case Inttab.lookup offsets offset of
-            SOME (name', time) => if name = name' then SOME time else NONE
-          | NONE => NONE)
-      | NONE => NONE)
-  | NONE => NONE)
-  |> the_default Time.zeroTime;
-
-
 (* session timing *)
 
 fun session_timing f x =
@@ -55,9 +23,8 @@
 
 (* build theories *)
 
-fun build_theories last_timing qualifier (options, thys) =
+fun build_theories qualifier (options, thys) =
   let
-    val context = {options = options, last_timing = last_timing};
     val condition = space_explode "," (Options.string options "condition");
     val conds = filter_out (can getenv_strict) condition;
   in
@@ -65,7 +32,7 @@
       (Options.set_default options;
         Isabelle_Process.init_options ();
         Future.fork I;
-        (Thy_Info.use_theories context qualifier
+        (Thy_Info.use_theories options qualifier
         |>
           (case Options.string options "profiling" of
             "" => I
@@ -84,46 +51,26 @@
 
 val _ =
   Isabelle_Process.protocol_command "build_session"
-    (fn [args_yxml] =>
+    (fn [resources_yxml, args_yxml] =>
         let
-          val (html_symbols, (command_timings, (parent_name, (chapter,
-            (session_name, (theories,
-            (session_positions, (session_directories,
-            (session_chapters, (doc_names,
-            (global_theories, (loaded_theories, bibtex_entries)))))))))))) =
+          val _ = Resources.init_session_yxml resources_yxml;
+          val (parent_name, (chapter, (session_name, theories))) =
             YXML.parse_body args_yxml |>
               let
                 open XML.Decode;
                 val position = Position.of_properties o properties;
               in
-                pair (list (pair string int)) (pair (list properties) (pair string (pair string
-                  (pair string (pair (((list (pair Options.decode (list (pair string position))))))
-                    (pair (list (pair string properties)) (pair (list (pair string string))
-                      (pair (list (pair string string)) (pair (list string)
-                        (pair (list (pair string string)) (pair (list string)
-                          (list (pair string (list string))))))))))))))
+                pair string (pair string (pair string
+                  (list (pair Options.decode (list (pair string position))))))
               end;
 
           fun build () =
             let
-              val _ =
-                Resources.init_session
-                  {html_symbols = html_symbols,
-                   session_positions = session_positions,
-                   session_directories = session_directories,
-                   session_chapters = session_chapters,
-                   bibtex_entries = bibtex_entries,
-                   docs = doc_names,
-                   global_theories = global_theories,
-                   loaded_theories = loaded_theories};
-
               val _ = Session.init parent_name (chapter, session_name);
 
-              val last_timing = get_timings (fold update_timings command_timings empty_timings);
-
               val res1 =
                 theories |>
-                  (List.app (build_theories last_timing session_name)
+                  (List.app (build_theories session_name)
                     |> session_timing
                     |> Exn.capture);
               val res2 = Exn.capture Session.finish ();
--- a/src/Pure/Tools/build.scala	Tue Nov 17 09:57:37 2020 +0000
+++ b/src/Pure/Tools/build.scala	Tue Nov 17 22:58:55 2020 +0100
@@ -38,7 +38,7 @@
     {
       val no_timings: Timings = (Nil, 0.0)
 
-      store.access_database(session_name) match {
+      store.try_open_database(session_name) match {
         case None => no_timings
         case Some(db) =>
           def ignore_error(msg: String) =
@@ -170,26 +170,6 @@
       Future.thread("build", uninterruptible = true) {
         val parent = info.parent.getOrElse("")
         val base = deps(parent)
-        val args_yxml =
-          YXML.string_of_body(
-            {
-              import XML.Encode._
-              pair(list(pair(string, int)), pair(list(properties), pair(string, pair(string,
-                pair(string, pair(list(pair(Options.encode, list(pair(string, properties)))),
-                pair(list(pair(string, properties)),
-                pair(list(pair(string, string)),
-                pair(list(pair(string, string)),
-                pair(list(string),
-                pair(list(pair(string, string)),
-                pair(list(string), list(pair(string, list(string)))))))))))))))(
-              (Symbol.codes, (command_timings0, (parent, (info.chapter,
-                (session_name, (info.theories,
-                (sessions_structure.session_positions,
-                (sessions_structure.dest_session_directories,
-                (sessions_structure.session_chapters,
-                (base.doc_names, (base.global_theories.toList,
-                (base.loaded_theories.keys, sessions_structure.bibtex_entries)))))))))))))
-            })
 
         val env =
           Isabelle_System.settings() +
@@ -207,7 +187,7 @@
           }
           else Nil
 
-        val resources = new Resources(sessions_structure, deps(parent))
+        val resources = new Resources(sessions_structure, base, command_timings = command_timings0)
         val session =
           new Session(options, resources) {
             override val xml_cache: XML.Cache = store.xml_cache
@@ -356,7 +336,16 @@
           Isabelle_Thread.interrupt_handler(_ => process.terminate) {
             Exn.capture { process.await_startup } match {
               case Exn.Res(_) =>
-                session.protocol_command("build_session", args_yxml)
+                val resources_yxml = resources.init_session_yxml
+                val args_yxml =
+                  YXML.string_of_body(
+                    {
+                      import XML.Encode._
+                      pair(string, pair(string, pair(string,
+                        list(pair(Options.encode, list(pair(string, properties)))))))(
+                        (parent, (info.chapter, (session_name, info.theories))))
+                    })
+                session.protocol_command("build_session", resources_yxml, args_yxml)
                 Build_Session_Errors.result
               case Exn.Exn(exn) => Exn.Res(List(Exn.message(exn)))
             }
@@ -545,7 +534,7 @@
       if (soft_build && !fresh_build) {
         val outdated =
           deps0.sessions_structure.build_topological_order.flatMap(name =>
-            store.access_database(name) match {
+            store.try_open_database(name) match {
               case Some(db) =>
                 using(db)(store.read_build(_, name)) match {
                   case Some(build)
@@ -702,7 +691,7 @@
 
                 val (current, heap_digest) =
                 {
-                  store.access_database(session_name) match {
+                  store.try_open_database(session_name) match {
                     case Some(db) =>
                       using(db)(store.read_build(_, session_name)) match {
                         case Some(build) =>