clarified use of XML.Cache;
authorwenzelm
Wed May 17 21:24:16 2017 +0200 (2017-05-17)
changeset 658575d29d93766ef
parent 65856 69f4dacd31cf
child 65858 9418a9fad835
clarified use of XML.Cache;
src/Pure/Admin/build_log.scala
src/Pure/Admin/build_status.scala
src/Pure/General/properties.scala
src/Pure/Thy/sessions.scala
     1.1 --- a/src/Pure/Admin/build_log.scala	Wed May 17 21:08:11 2017 +0200
     1.2 +++ b/src/Pure/Admin/build_log.scala	Wed May 17 21:24:16 2017 +0200
     1.3 @@ -747,8 +747,10 @@
     1.4  
     1.5    def store(options: Options): Store = new Store(options)
     1.6  
     1.7 -  class Store private[Build_Log](options: Options) extends Properties.Store
     1.8 +  class Store private[Build_Log](options: Options)
     1.9    {
    1.10 +    val xml_cache: XML.Cache = new XML.Cache()
    1.11 +
    1.12      def open_database(
    1.13        user: String = options.string("build_log_database_user"),
    1.14        password: String = options.string("build_log_database_password"),
    1.15 @@ -889,7 +891,7 @@
    1.16        {
    1.17          val ml_stats: List[(String, Option[Bytes])] =
    1.18            Par_List.map[(String, Session_Entry), (String, Option[Bytes])](
    1.19 -            { case (a, b) => (a, compress_properties(b.ml_statistics).proper) },
    1.20 +            { case (a, b) => (a, Properties.compress(b.ml_statistics).proper) },
    1.21              build_info.sessions.iterator.filter(p => p._2.ml_statistics.nonEmpty).toList)
    1.22          val entries = if (ml_stats.nonEmpty) ml_stats else List("" -> None)
    1.23          for ((session_name, ml_statistics) <- entries) {
    1.24 @@ -1011,7 +1013,8 @@
    1.25                  heap_size = res.get_long(Data.heap_size),
    1.26                  status = res.get_string(Data.status).map(Session_Status.withName(_)),
    1.27                  ml_statistics =
    1.28 -                  if (ml_statistics) uncompress_properties(res.bytes(Data.ml_statistics))
    1.29 +                  if (ml_statistics)
    1.30 +                    Properties.uncompress(res.bytes(Data.ml_statistics), Some(xml_cache))
    1.31                    else Nil)
    1.32              session_name -> session_entry
    1.33            }).toMap
     2.1 --- a/src/Pure/Admin/build_status.scala	Wed May 17 21:08:11 2017 +0200
     2.2 +++ b/src/Pure/Admin/build_status.scala	Wed May 17 21:24:16 2017 +0200
     2.3 @@ -169,7 +169,7 @@
     2.4              val ml_stats =
     2.5                ML_Statistics(
     2.6                  if (ml_statistics)
     2.7 -                    store.uncompress_properties(res.bytes(Build_Log.Data.ml_statistics))
     2.8 +                  Properties.uncompress(res.bytes(Build_Log.Data.ml_statistics))
     2.9                  else Nil, heading = session_name + " (Isabelle/ " + isabelle_version + ")")
    2.10  
    2.11              val entry =
     3.1 --- a/src/Pure/General/properties.scala	Wed May 17 21:08:11 2017 +0200
     3.2 +++ b/src/Pure/General/properties.scala	Wed May 17 21:24:16 2017 +0200
     3.3 @@ -33,6 +33,38 @@
     3.4    }
     3.5  
     3.6  
     3.7 +  /* external storage */
     3.8 +
     3.9 +  def encode(ps: T): Bytes = Bytes(YXML.string_of_body(XML.Encode.properties(ps)))
    3.10 +
    3.11 +  def decode(bs: Bytes, xml_cache: Option[XML.Cache] = None): T =
    3.12 +  {
    3.13 +    val ps = XML.Decode.properties(YXML.parse_body(bs.text))
    3.14 +    xml_cache match {
    3.15 +      case None => ps
    3.16 +      case Some(cache) => cache.props(ps)
    3.17 +    }
    3.18 +  }
    3.19 +
    3.20 +  def compress(ps: List[T], options: XZ.Options = XZ.options()): Bytes =
    3.21 +  {
    3.22 +    if (ps.isEmpty) Bytes.empty
    3.23 +    else Bytes(YXML.string_of_body(XML.Encode.list(XML.Encode.properties)(ps))).compress(options)
    3.24 +  }
    3.25 +
    3.26 +  def uncompress(bs: Bytes, xml_cache: Option[XML.Cache] = None): List[T] =
    3.27 +  {
    3.28 +    if (bs.isEmpty) Nil
    3.29 +    else {
    3.30 +      val ps = XML.Decode.list(XML.Decode.properties)(YXML.parse_body(bs.uncompress().text))
    3.31 +      xml_cache match {
    3.32 +        case None => ps
    3.33 +        case Some(cache) => ps.map(cache.props(_))
    3.34 +      }
    3.35 +    }
    3.36 +  }
    3.37 +
    3.38 +
    3.39    /* multi-line entries */
    3.40  
    3.41    val separator = '\u000b'
    3.42 @@ -95,32 +127,4 @@
    3.43          case Some((_, value)) => Value.Double.unapply(value)
    3.44        }
    3.45    }
    3.46 -
    3.47 -
    3.48 -  /* cached store */
    3.49 -
    3.50 -  trait Store
    3.51 -  {
    3.52 -    val xml_cache: XML.Cache = new XML.Cache()
    3.53 -
    3.54 -    def encode_properties(ps: T): Bytes =
    3.55 -      Bytes(YXML.string_of_body(XML.Encode.properties(ps)))
    3.56 -
    3.57 -    def decode_properties(bs: Bytes): T =
    3.58 -      xml_cache.props(XML.Decode.properties(YXML.parse_body(bs.text)))
    3.59 -
    3.60 -    def compress_properties(ps: List[T], options: XZ.Options = XZ.options()): Bytes =
    3.61 -    {
    3.62 -      if (ps.isEmpty) Bytes.empty
    3.63 -      else Bytes(YXML.string_of_body(XML.Encode.list(XML.Encode.properties)(ps))).compress(options)
    3.64 -    }
    3.65 -
    3.66 -    def uncompress_properties(bs: Bytes): List[T] =
    3.67 -    {
    3.68 -      if (bs.isEmpty) Nil
    3.69 -      else
    3.70 -        XML.Decode.list(XML.Decode.properties)(YXML.parse_body(bs.uncompress().text)).
    3.71 -          map(xml_cache.props(_))
    3.72 -    }
    3.73 -  }
    3.74  }
     4.1 --- a/src/Pure/Thy/sessions.scala	Wed May 17 21:08:11 2017 +0200
     4.2 +++ b/src/Pure/Thy/sessions.scala	Wed May 17 21:24:16 2017 +0200
     4.3 @@ -750,7 +750,7 @@
     4.4  
     4.5    def store(system_mode: Boolean = false): Store = new Store(system_mode)
     4.6  
     4.7 -  class Store private[Sessions](system_mode: Boolean) extends Properties.Store
     4.8 +  class Store private[Sessions](system_mode: Boolean)
     4.9    {
    4.10      /* file names */
    4.11  
    4.12 @@ -761,6 +761,8 @@
    4.13  
    4.14      /* SQL database content */
    4.15  
    4.16 +    val xml_cache = new XML.Cache()
    4.17 +
    4.18      def read_bytes(db: SQL.Database, name: String, column: SQL.Column): Bytes =
    4.19        db.using_statement(Session_Info.table.select(List(column),
    4.20          Session_Info.session_name.where_equal(name)))(stmt =>
    4.21 @@ -770,7 +772,7 @@
    4.22        })
    4.23  
    4.24      def read_properties(db: SQL.Database, name: String, column: SQL.Column): List[Properties.T] =
    4.25 -      uncompress_properties(read_bytes(db, name, column))
    4.26 +      Properties.uncompress(read_bytes(db, name, column), Some(xml_cache))
    4.27  
    4.28  
    4.29      /* output */
    4.30 @@ -825,10 +827,10 @@
    4.31          db.using_statement(Session_Info.table.insert())(stmt =>
    4.32          {
    4.33            stmt.string(1) = name
    4.34 -          stmt.bytes(2) = encode_properties(build_log.session_timing)
    4.35 -          stmt.bytes(3) = compress_properties(build_log.command_timings)
    4.36 -          stmt.bytes(4) = compress_properties(build_log.ml_statistics)
    4.37 -          stmt.bytes(5) = compress_properties(build_log.task_statistics)
    4.38 +          stmt.bytes(2) = Properties.encode(build_log.session_timing)
    4.39 +          stmt.bytes(3) = Properties.compress(build_log.command_timings)
    4.40 +          stmt.bytes(4) = Properties.compress(build_log.ml_statistics)
    4.41 +          stmt.bytes(5) = Properties.compress(build_log.task_statistics)
    4.42            stmt.string(6) = cat_lines(build.sources)
    4.43            stmt.string(7) = cat_lines(build.input_heaps)
    4.44            stmt.string(8) = build.output_heap getOrElse ""
    4.45 @@ -839,7 +841,7 @@
    4.46      }
    4.47  
    4.48      def read_session_timing(db: SQL.Database, name: String): Properties.T =
    4.49 -      decode_properties(read_bytes(db, name, Session_Info.session_timing))
    4.50 +      Properties.decode(read_bytes(db, name, Session_Info.session_timing), Some(xml_cache))
    4.51  
    4.52      def read_command_timings(db: SQL.Database, name: String): List[Properties.T] =
    4.53        read_properties(db, name, Session_Info.command_timings)