persistent storage of imported_sources;
authorwenzelm
Sun Oct 01 20:50:26 2017 +0200 (18 months ago)
changeset 66744fec1504e5f03
parent 66743 ff05d922bc34
child 66745 e7ac579b883c
persistent storage of imported_sources;
src/Pure/Thy/sessions.scala
src/Pure/Tools/build.scala
     1.1 --- a/src/Pure/Thy/sessions.scala	Sun Oct 01 17:59:26 2017 +0200
     1.2 +++ b/src/Pure/Thy/sessions.scala	Sun Oct 01 20:50:26 2017 +0200
     1.3 @@ -114,8 +114,8 @@
     1.4      loaded_theories: Graph[String, Outer_Syntax] = Graph.string,
     1.5      known: Known = Known.empty,
     1.6      overall_syntax: Outer_Syntax = Outer_Syntax.empty,
     1.7 +    imported_sources: List[(Path, SHA1.Digest)] = Nil,
     1.8      sources: List[(Path, SHA1.Digest)] = Nil,
     1.9 -    imported_sources: List[(Path, SHA1.Digest)] = Nil,
    1.10      session_graph: Graph_Display.Graph = Graph_Display.empty_graph,
    1.11      errors: List[String] = Nil,
    1.12      imports: Option[Base] = None)
    1.13 @@ -148,7 +148,12 @@
    1.14    {
    1.15      def is_empty: Boolean = session_bases.isEmpty
    1.16      def apply(name: String): Base = session_bases(name)
    1.17 -    def sources(name: String): List[SHA1.Digest] = session_bases(name).sources.map(_._2)
    1.18 +
    1.19 +    def imported_sources(name: String): List[SHA1.Digest] =
    1.20 +      session_bases(name).imported_sources.map(_._2)
    1.21 +
    1.22 +    def sources(name: String): List[SHA1.Digest] =
    1.23 +      session_bases(name).sources.map(_._2)
    1.24  
    1.25      def errors: List[String] =
    1.26        (for {
    1.27 @@ -297,8 +302,8 @@
    1.28                  loaded_theories = thy_deps.loaded_theories,
    1.29                  known = known,
    1.30                  overall_syntax = overall_syntax,
    1.31 +                imported_sources = check_sources(imported_files),
    1.32                  sources = check_sources(session_files),
    1.33 -                imported_sources = check_sources(imported_files),
    1.34                  session_graph = session_graph,
    1.35                  errors = thy_deps.errors ::: sources_errors,
    1.36                  imports = Some(imports_base))
    1.37 @@ -810,11 +815,12 @@
    1.38        List(session_name, session_timing, command_timings, ml_statistics, task_statistics, errors)
    1.39  
    1.40      // Build.Session_Info
    1.41 +    val imported_sources = SQL.Column.string("imported_sources")
    1.42      val sources = SQL.Column.string("sources")
    1.43      val input_heaps = SQL.Column.string("input_heaps")
    1.44      val output_heap = SQL.Column.string("output_heap")
    1.45      val return_code = SQL.Column.int("return_code")
    1.46 -    val build_columns = List(sources, input_heaps, output_heap, return_code)
    1.47 +    val build_columns = List(imported_sources, sources, input_heaps, output_heap, return_code)
    1.48  
    1.49      val table = SQL.Table("isabelle_session_info", build_log_columns ::: build_columns)
    1.50    }
    1.51 @@ -903,10 +909,11 @@
    1.52            stmt.bytes(4) = Properties.compress(build_log.ml_statistics)
    1.53            stmt.bytes(5) = Properties.compress(build_log.task_statistics)
    1.54            stmt.bytes(6) = Build_Log.compress_errors(build_log.errors)
    1.55 -          stmt.string(7) = cat_lines(build.sources)
    1.56 -          stmt.string(8) = cat_lines(build.input_heaps)
    1.57 -          stmt.string(9) = build.output_heap getOrElse ""
    1.58 -          stmt.int(10) = build.return_code
    1.59 +          stmt.string(7) = cat_lines(build.imported_sources)
    1.60 +          stmt.string(8) = cat_lines(build.sources)
    1.61 +          stmt.string(9) = cat_lines(build.input_heaps)
    1.62 +          stmt.string(10) = build.output_heap getOrElse ""
    1.63 +          stmt.int(11) = build.return_code
    1.64            stmt.execute()
    1.65          })
    1.66        }
    1.67 @@ -928,19 +935,35 @@
    1.68        Build_Log.uncompress_errors(read_bytes(db, name, Session_Info.errors))
    1.69  
    1.70      def read_build(db: SQL.Database, name: String): Option[Build.Session_Info] =
    1.71 -      db.using_statement(Session_Info.table.select(Session_Info.build_columns,
    1.72 -        Session_Info.session_name.where_equal(name)))(stmt =>
    1.73 -      {
    1.74 -        val res = stmt.execute_query()
    1.75 -        if (!res.next()) None
    1.76 -        else {
    1.77 -          Some(
    1.78 -            Build.Session_Info(
    1.79 -              split_lines(res.string(Session_Info.sources)),
    1.80 -              split_lines(res.string(Session_Info.input_heaps)),
    1.81 -              res.string(Session_Info.output_heap) match { case "" => None case s => Some(s) },
    1.82 -              res.int(Session_Info.return_code)))
    1.83 -        }
    1.84 -      })
    1.85 +    {
    1.86 +      val result0 =
    1.87 +        db.using_statement(Session_Info.table.select(Session_Info.build_columns.tail,
    1.88 +          Session_Info.session_name.where_equal(name)))(stmt =>
    1.89 +        {
    1.90 +          val res = stmt.execute_query()
    1.91 +          if (!res.next()) None
    1.92 +          else {
    1.93 +            Some(
    1.94 +              Build.Session_Info(Nil,
    1.95 +                split_lines(res.string(Session_Info.sources)),
    1.96 +                split_lines(res.string(Session_Info.input_heaps)),
    1.97 +                res.string(Session_Info.output_heap) match { case "" => None case s => Some(s) },
    1.98 +                res.int(Session_Info.return_code)))
    1.99 +          }
   1.100 +        })
   1.101 +      result0.map(info =>
   1.102 +        info.copy(imported_sources =
   1.103 +          try {
   1.104 +            db.using_statement(Session_Info.table.select(List(Session_Info.imported_sources),
   1.105 +              Session_Info.session_name.where_equal(name)))(stmt =>
   1.106 +            {
   1.107 +              val res = stmt.execute_query()
   1.108 +              if (!res.next) Nil else split_lines(res.string(Session_Info.imported_sources))
   1.109 +            })
   1.110 +          } // column "imported_sources" could be missing
   1.111 +          catch { case _: java.sql.SQLException => Nil }
   1.112 +        )
   1.113 +      )
   1.114 +    }
   1.115    }
   1.116  }
     2.1 --- a/src/Pure/Tools/build.scala	Sun Oct 01 17:59:26 2017 +0200
     2.2 +++ b/src/Pure/Tools/build.scala	Sun Oct 01 20:50:26 2017 +0200
     2.3 @@ -24,6 +24,7 @@
     2.4    /* persistent build info */
     2.5  
     2.6    sealed case class Session_Info(
     2.7 +    imported_sources: List[String],
     2.8      sources: List[String],
     2.9      input_heaps: List[String],
    2.10      output_heap: Option[String],
    2.11 @@ -380,6 +381,9 @@
    2.12          verbose = verbose, list_files = list_files, check_keywords = check_keywords,
    2.13          global_theories = full_sessions.global_theories).check_errors
    2.14  
    2.15 +    def imported_sources_stamp(name: String): List[String] =
    2.16 +      deps.imported_sources(name).map(_.toString).sorted
    2.17 +
    2.18      def sources_stamp(name: String): List[String] =
    2.19        (selected_sessions(name).meta_digest :: deps.sources(name)).map(_.toString).sorted
    2.20  
    2.21 @@ -501,7 +505,12 @@
    2.22                        parse_session_info(
    2.23                          command_timings = true, ml_statistics = true, task_statistics = true),
    2.24                    build =
    2.25 -                    Session_Info(sources_stamp(name), input_heaps, heap_stamp, process_result.rc)))
    2.26 +                    Session_Info(
    2.27 +                      imported_sources_stamp(name),
    2.28 +                      sources_stamp(name),
    2.29 +                      input_heaps,
    2.30 +                      heap_stamp,
    2.31 +                      process_result.rc)))
    2.32              }
    2.33  
    2.34              // messages