# HG changeset patch # User wenzelm # Date 1506883826 -7200 # Node ID fec1504e5f031a743486bb444030303acaf13449 # Parent ff05d922bc3435efa84412669f46a022b89b070f persistent storage of imported_sources; diff -r ff05d922bc34 -r fec1504e5f03 src/Pure/Thy/sessions.scala --- a/src/Pure/Thy/sessions.scala Sun Oct 01 17:59:26 2017 +0200 +++ b/src/Pure/Thy/sessions.scala Sun Oct 01 20:50:26 2017 +0200 @@ -114,8 +114,8 @@ loaded_theories: Graph[String, Outer_Syntax] = Graph.string, known: Known = Known.empty, overall_syntax: Outer_Syntax = Outer_Syntax.empty, + imported_sources: List[(Path, SHA1.Digest)] = Nil, sources: List[(Path, SHA1.Digest)] = Nil, - imported_sources: List[(Path, SHA1.Digest)] = Nil, session_graph: Graph_Display.Graph = Graph_Display.empty_graph, errors: List[String] = Nil, imports: Option[Base] = None) @@ -148,7 +148,12 @@ { def is_empty: Boolean = session_bases.isEmpty def apply(name: String): Base = session_bases(name) - def sources(name: String): List[SHA1.Digest] = session_bases(name).sources.map(_._2) + + def imported_sources(name: String): List[SHA1.Digest] = + session_bases(name).imported_sources.map(_._2) + + def sources(name: String): List[SHA1.Digest] = + session_bases(name).sources.map(_._2) def errors: List[String] = (for { @@ -297,8 +302,8 @@ loaded_theories = thy_deps.loaded_theories, known = known, overall_syntax = overall_syntax, + imported_sources = check_sources(imported_files), sources = check_sources(session_files), - imported_sources = check_sources(imported_files), session_graph = session_graph, errors = thy_deps.errors ::: sources_errors, imports = Some(imports_base)) @@ -810,11 +815,12 @@ List(session_name, session_timing, command_timings, ml_statistics, task_statistics, errors) // Build.Session_Info + val imported_sources = SQL.Column.string("imported_sources") val sources = SQL.Column.string("sources") val input_heaps = SQL.Column.string("input_heaps") val output_heap = SQL.Column.string("output_heap") val return_code = SQL.Column.int("return_code") - val build_columns = List(sources, input_heaps, output_heap, return_code) + val build_columns = List(imported_sources, sources, input_heaps, output_heap, return_code) val table = SQL.Table("isabelle_session_info", build_log_columns ::: build_columns) } @@ -903,10 +909,11 @@ stmt.bytes(4) = Properties.compress(build_log.ml_statistics) stmt.bytes(5) = Properties.compress(build_log.task_statistics) stmt.bytes(6) = Build_Log.compress_errors(build_log.errors) - stmt.string(7) = cat_lines(build.sources) - stmt.string(8) = cat_lines(build.input_heaps) - stmt.string(9) = build.output_heap getOrElse "" - stmt.int(10) = build.return_code + stmt.string(7) = cat_lines(build.imported_sources) + stmt.string(8) = cat_lines(build.sources) + stmt.string(9) = cat_lines(build.input_heaps) + stmt.string(10) = build.output_heap getOrElse "" + stmt.int(11) = build.return_code stmt.execute() }) } @@ -928,19 +935,35 @@ Build_Log.uncompress_errors(read_bytes(db, name, Session_Info.errors)) def read_build(db: SQL.Database, name: String): Option[Build.Session_Info] = - db.using_statement(Session_Info.table.select(Session_Info.build_columns, - Session_Info.session_name.where_equal(name)))(stmt => - { - val res = stmt.execute_query() - if (!res.next()) None - else { - Some( - Build.Session_Info( - split_lines(res.string(Session_Info.sources)), - split_lines(res.string(Session_Info.input_heaps)), - res.string(Session_Info.output_heap) match { case "" => None case s => Some(s) }, - res.int(Session_Info.return_code))) - } - }) + { + val result0 = + db.using_statement(Session_Info.table.select(Session_Info.build_columns.tail, + Session_Info.session_name.where_equal(name)))(stmt => + { + val res = stmt.execute_query() + if (!res.next()) None + else { + Some( + Build.Session_Info(Nil, + split_lines(res.string(Session_Info.sources)), + split_lines(res.string(Session_Info.input_heaps)), + res.string(Session_Info.output_heap) match { case "" => None case s => Some(s) }, + res.int(Session_Info.return_code))) + } + }) + result0.map(info => + info.copy(imported_sources = + try { + db.using_statement(Session_Info.table.select(List(Session_Info.imported_sources), + Session_Info.session_name.where_equal(name)))(stmt => + { + val res = stmt.execute_query() + if (!res.next) Nil else split_lines(res.string(Session_Info.imported_sources)) + }) + } // column "imported_sources" could be missing + catch { case _: java.sql.SQLException => Nil } + ) + ) + } } } diff -r ff05d922bc34 -r fec1504e5f03 src/Pure/Tools/build.scala --- a/src/Pure/Tools/build.scala Sun Oct 01 17:59:26 2017 +0200 +++ b/src/Pure/Tools/build.scala Sun Oct 01 20:50:26 2017 +0200 @@ -24,6 +24,7 @@ /* persistent build info */ sealed case class Session_Info( + imported_sources: List[String], sources: List[String], input_heaps: List[String], output_heap: Option[String], @@ -380,6 +381,9 @@ verbose = verbose, list_files = list_files, check_keywords = check_keywords, global_theories = full_sessions.global_theories).check_errors + def imported_sources_stamp(name: String): List[String] = + deps.imported_sources(name).map(_.toString).sorted + def sources_stamp(name: String): List[String] = (selected_sessions(name).meta_digest :: deps.sources(name)).map(_.toString).sorted @@ -501,7 +505,12 @@ parse_session_info( command_timings = true, ml_statistics = true, task_statistics = true), build = - Session_Info(sources_stamp(name), input_heaps, heap_stamp, process_result.rc))) + Session_Info( + imported_sources_stamp(name), + sources_stamp(name), + input_heaps, + heap_stamp, + process_result.rc))) } // messages