merged
authorwenzelm
Mon Jun 11 21:10:03 2018 +0200 (11 months ago)
changeset 68419a1f43b4f984d
parent 68415 d74ba11680d4
parent 68418 366e43cddd20
child 68421 e082a36dc35d
merged
     1.1 --- a/src/Pure/PIDE/document.scala	Mon Jun 11 20:45:51 2018 +0200
     1.2 +++ b/src/Pure/PIDE/document.scala	Mon Jun 11 21:10:03 2018 +0200
     1.3 @@ -539,6 +539,7 @@
     1.4      def markup_to_XML(range: Text.Range, elements: Markup.Elements): XML.Body
     1.5      def messages: List[(XML.Tree, Position.T)]
     1.6      def exports: List[Export.Entry]
     1.7 +    def exports_map: Map[String, Export.Entry]
     1.8  
     1.9      def find_command(id: Document_ID.Generic): Option[(Node, Command)]
    1.10      def find_command_position(id: Document_ID.Generic, offset: Symbol.Offset)
    1.11 @@ -1030,7 +1031,7 @@
    1.12          def markup_to_XML(range: Text.Range, elements: Markup.Elements): XML.Body =
    1.13            state.markup_to_XML(version, node_name, range, elements)
    1.14  
    1.15 -        def messages: List[(XML.Tree, Position.T)] =
    1.16 +        lazy val messages: List[(XML.Tree, Position.T)] =
    1.17            (for {
    1.18              (command, start) <-
    1.19                Document.Node.Commands.starts_pos(
    1.20 @@ -1039,13 +1040,16 @@
    1.21              (_, tree) <- state.command_results(version, command).iterator
    1.22             } yield (tree, pos)).toList
    1.23  
    1.24 -        def exports: List[Export.Entry] =
    1.25 +        lazy val exports: List[Export.Entry] =
    1.26            Command.Exports.merge(
    1.27              for {
    1.28                command <- node.commands.iterator
    1.29                st <- state.command_states(version, command).iterator
    1.30              } yield st.exports).iterator.map(_._2).toList
    1.31  
    1.32 +        lazy val exports_map: Map[String, Export.Entry] =
    1.33 +          (for (entry <- exports.iterator) yield (entry.name, entry)).toMap
    1.34 +
    1.35  
    1.36          /* find command */
    1.37  
     2.1 --- a/src/Pure/Thy/export.scala	Mon Jun 11 20:45:51 2018 +0200
     2.2 +++ b/src/Pure/Thy/export.scala	Mon Jun 11 21:10:03 2018 +0200
     2.3 @@ -185,6 +185,35 @@
     2.4    }
     2.5  
     2.6  
     2.7 +  /* abstract provider */
     2.8 +
     2.9 +  object Provider
    2.10 +  {
    2.11 +    def database(db: SQL.Database, session_name: String, theory_name: String): Provider =
    2.12 +      new Provider {
    2.13 +        def apply(export_name: String): Option[Entry] =
    2.14 +          read_entry(db, session_name, theory_name, export_name)
    2.15 +      }
    2.16 +
    2.17 +    def snapshot(snapshot: Document.Snapshot): Provider =
    2.18 +      new Provider {
    2.19 +        def apply(export_name: String): Option[Entry] =
    2.20 +          snapshot.exports_map.get(export_name)
    2.21 +      }
    2.22 +  }
    2.23 +
    2.24 +  trait Provider
    2.25 +  {
    2.26 +    def apply(export_name: String): Option[Entry]
    2.27 +
    2.28 +    def uncompressed_yxml(export_name: String, cache: XZ.Cache = XZ.cache()): XML.Body =
    2.29 +      apply(export_name) match {
    2.30 +        case Some(entry) => entry.uncompressed_yxml(cache = cache)
    2.31 +        case None => Nil
    2.32 +      }
    2.33 +  }
    2.34 +
    2.35 +
    2.36    /* export to file-system */
    2.37  
    2.38    def export_files(
     3.1 --- a/src/Pure/Thy/export_theory.scala	Mon Jun 11 20:45:51 2018 +0200
     3.2 +++ b/src/Pure/Thy/export_theory.scala	Mon Jun 11 21:10:03 2018 +0200
     3.3 @@ -40,7 +40,8 @@
     3.4        {
     3.5          db.transaction {
     3.6            Export.read_theory_names(db, session_name).map((theory_name: String) =>
     3.7 -            read_theory(db, session_name, theory_name, types = types, consts = consts,
     3.8 +            read_theory(Export.Provider.database(db, session_name, theory_name),
     3.9 +              session_name, theory_name, types = types, consts = consts,
    3.10                axioms = axioms, facts = facts, classes = classes, typedefs = typedefs,
    3.11                cache = Some(cache)))
    3.12          }
    3.13 @@ -90,7 +91,7 @@
    3.14    def empty_theory(name: String): Theory =
    3.15      Theory(name, Nil, Nil, Nil, Nil, Nil, Nil, Nil, Nil, Nil)
    3.16  
    3.17 -  def read_theory(db: SQL.Database, session_name: String, theory_name: String,
    3.18 +  def read_theory(provider: Export.Provider, session_name: String, theory_name: String,
    3.19      types: Boolean = true,
    3.20      consts: Boolean = true,
    3.21      axioms: Boolean = true,
    3.22 @@ -102,7 +103,7 @@
    3.23      cache: Option[Term.Cache] = None): Theory =
    3.24    {
    3.25      val parents =
    3.26 -      Export.read_entry(db, session_name, theory_name, export_prefix + "parents") match {
    3.27 +      provider(export_prefix + "parents") match {
    3.28          case Some(entry) => split_lines(entry.uncompressed().text)
    3.29          case None =>
    3.30            error("Missing theory export in session " + quote(session_name) + ": " +
    3.31 @@ -110,14 +111,14 @@
    3.32        }
    3.33      val theory =
    3.34        Theory(theory_name, parents,
    3.35 -        if (types) read_types(db, session_name, theory_name) else Nil,
    3.36 -        if (consts) read_consts(db, session_name, theory_name) else Nil,
    3.37 -        if (axioms) read_axioms(db, session_name, theory_name) else Nil,
    3.38 -        if (facts) read_facts(db, session_name, theory_name) else Nil,
    3.39 -        if (classes) read_classes(db, session_name, theory_name) else Nil,
    3.40 -        if (typedefs) read_typedefs(db, session_name, theory_name) else Nil,
    3.41 -        if (classrel) read_classrel(db, session_name, theory_name) else Nil,
    3.42 -        if (arities) read_arities(db, session_name, theory_name) else Nil)
    3.43 +        if (types) read_types(provider) else Nil,
    3.44 +        if (consts) read_consts(provider) else Nil,
    3.45 +        if (axioms) read_axioms(provider) else Nil,
    3.46 +        if (facts) read_facts(provider) else Nil,
    3.47 +        if (classes) read_classes(provider) else Nil,
    3.48 +        if (typedefs) read_typedefs(provider) else Nil,
    3.49 +        if (classrel) read_classrel(provider) else Nil,
    3.50 +        if (arities) read_arities(provider) else Nil)
    3.51      if (cache.isDefined) theory.cache(cache.get) else theory
    3.52    }
    3.53  
    3.54 @@ -146,22 +147,6 @@
    3.55      }
    3.56    }
    3.57  
    3.58 -  def read_export[A](db: SQL.Database, session_name: String, theory_name: String,
    3.59 -    export_name: String, decode: XML.Body => List[A]): List[A] =
    3.60 -  {
    3.61 -    Export.read_entry(db, session_name, theory_name, export_prefix + export_name) match {
    3.62 -      case Some(entry) => decode(entry.uncompressed_yxml())
    3.63 -      case None => Nil
    3.64 -    }
    3.65 -  }
    3.66 -
    3.67 -  def read_entities[A](db: SQL.Database, session_name: String, theory_name: String,
    3.68 -    export_name: String, decode: XML.Tree => A): List[A] =
    3.69 -  {
    3.70 -    read_export(db, session_name, theory_name, export_name,
    3.71 -      (body: XML.Body) => body.map(decode(_)))
    3.72 -  }
    3.73 -
    3.74  
    3.75    /* types */
    3.76  
    3.77 @@ -173,18 +158,17 @@
    3.78          abbrev.map(cache.typ(_)))
    3.79    }
    3.80  
    3.81 -  def read_types(db: SQL.Database, session_name: String, theory_name: String): List[Type] =
    3.82 -    read_entities(db, session_name, theory_name, "types",
    3.83 -      (tree: XML.Tree) =>
    3.84 +  def read_types(provider: Export.Provider): List[Type] =
    3.85 +    provider.uncompressed_yxml(export_prefix + "types").map((tree: XML.Tree) =>
    3.86 +      {
    3.87 +        val (entity, body) = decode_entity(tree)
    3.88 +        val (args, abbrev) =
    3.89          {
    3.90 -          val (entity, body) = decode_entity(tree)
    3.91 -          val (args, abbrev) =
    3.92 -          {
    3.93 -            import XML.Decode._
    3.94 -            pair(list(string), option(Term_XML.Decode.typ))(body)
    3.95 -          }
    3.96 -          Type(entity, args, abbrev)
    3.97 -        })
    3.98 +          import XML.Decode._
    3.99 +          pair(list(string), option(Term_XML.Decode.typ))(body)
   3.100 +        }
   3.101 +        Type(entity, args, abbrev)
   3.102 +      })
   3.103  
   3.104  
   3.105    /* consts */
   3.106 @@ -199,18 +183,17 @@
   3.107          abbrev.map(cache.term(_)))
   3.108    }
   3.109  
   3.110 -  def read_consts(db: SQL.Database, session_name: String, theory_name: String): List[Const] =
   3.111 -    read_entities(db, session_name, theory_name, "consts",
   3.112 -      (tree: XML.Tree) =>
   3.113 +  def read_consts(provider: Export.Provider): List[Const] =
   3.114 +    provider.uncompressed_yxml(export_prefix + "consts").map((tree: XML.Tree) =>
   3.115 +      {
   3.116 +        val (entity, body) = decode_entity(tree)
   3.117 +        val (args, typ, abbrev) =
   3.118          {
   3.119 -          val (entity, body) = decode_entity(tree)
   3.120 -          val (args, typ, abbrev) =
   3.121 -          {
   3.122 -            import XML.Decode._
   3.123 -            triple(list(string), Term_XML.Decode.typ, option(Term_XML.Decode.term))(body)
   3.124 -          }
   3.125 -          Const(entity, args, typ, abbrev)
   3.126 -        })
   3.127 +          import XML.Decode._
   3.128 +          triple(list(string), Term_XML.Decode.typ, option(Term_XML.Decode.term))(body)
   3.129 +        }
   3.130 +        Const(entity, args, typ, abbrev)
   3.131 +      })
   3.132  
   3.133  
   3.134    /* axioms and facts */
   3.135 @@ -236,14 +219,13 @@
   3.136          cache.term(prop))
   3.137    }
   3.138  
   3.139 -  def read_axioms(db: SQL.Database, session_name: String, theory_name: String): List[Axiom] =
   3.140 -    read_entities(db, session_name, theory_name, "axioms",
   3.141 -      (tree: XML.Tree) =>
   3.142 -        {
   3.143 -          val (entity, body) = decode_entity(tree)
   3.144 -          val (typargs, args, List(prop)) = decode_props(body)
   3.145 -          Axiom(entity, typargs, args, prop)
   3.146 -        })
   3.147 +  def read_axioms(provider: Export.Provider): List[Axiom] =
   3.148 +    provider.uncompressed_yxml(export_prefix + "axioms").map((tree: XML.Tree) =>
   3.149 +      {
   3.150 +        val (entity, body) = decode_entity(tree)
   3.151 +        val (typargs, args, List(prop)) = decode_props(body)
   3.152 +        Axiom(entity, typargs, args, prop)
   3.153 +      })
   3.154  
   3.155    sealed case class Fact(
   3.156      entity: Entity,
   3.157 @@ -258,14 +240,13 @@
   3.158          props.map(cache.term(_)))
   3.159    }
   3.160  
   3.161 -  def read_facts(db: SQL.Database, session_name: String, theory_name: String): List[Fact] =
   3.162 -    read_entities(db, session_name, theory_name, "facts",
   3.163 -      (tree: XML.Tree) =>
   3.164 -        {
   3.165 -          val (entity, body) = decode_entity(tree)
   3.166 -          val (typargs, args, props) = decode_props(body)
   3.167 -          Fact(entity, typargs, args, props)
   3.168 -        })
   3.169 +  def read_facts(provider: Export.Provider): List[Fact] =
   3.170 +    provider.uncompressed_yxml(export_prefix + "facts").map((tree: XML.Tree) =>
   3.171 +      {
   3.172 +        val (entity, body) = decode_entity(tree)
   3.173 +        val (typargs, args, props) = decode_props(body)
   3.174 +        Fact(entity, typargs, args, props)
   3.175 +      })
   3.176  
   3.177  
   3.178    /* type classes */
   3.179 @@ -279,19 +260,18 @@
   3.180          axioms.map(cache.term(_)))
   3.181    }
   3.182  
   3.183 -  def read_classes(db: SQL.Database, session_name: String, theory_name: String): List[Class] =
   3.184 -    read_entities(db, session_name, theory_name, "classes",
   3.185 -      (tree: XML.Tree) =>
   3.186 +  def read_classes(provider: Export.Provider): List[Class] =
   3.187 +    provider.uncompressed_yxml(export_prefix + "classes").map((tree: XML.Tree) =>
   3.188 +      {
   3.189 +        val (entity, body) = decode_entity(tree)
   3.190 +        val (params, axioms) =
   3.191          {
   3.192 -          val (entity, body) = decode_entity(tree)
   3.193 -          val (params, axioms) =
   3.194 -          {
   3.195 -            import XML.Decode._
   3.196 -            import Term_XML.Decode._
   3.197 -            pair(list(pair(string, typ)), list(term))(body)
   3.198 -          }
   3.199 -          Class(entity, params, axioms)
   3.200 -        })
   3.201 +          import XML.Decode._
   3.202 +          import Term_XML.Decode._
   3.203 +          pair(list(pair(string, typ)), list(term))(body)
   3.204 +        }
   3.205 +        Class(entity, params, axioms)
   3.206 +      })
   3.207  
   3.208  
   3.209    /* sort algebra */
   3.210 @@ -302,17 +282,16 @@
   3.211        Classrel(cache.string(class_name), super_names.map(cache.string(_)))
   3.212    }
   3.213  
   3.214 -  def read_classrel(db: SQL.Database, session_name: String, theory_name: String): List[Classrel] =
   3.215 -    read_export(db, session_name, theory_name, "classrel",
   3.216 -      (body: XML.Body) =>
   3.217 -        {
   3.218 -          val classrel =
   3.219 -          {
   3.220 -            import XML.Decode._
   3.221 -            list(pair(string, list(string)))(body)
   3.222 -          }
   3.223 -          for ((c, cs) <- classrel) yield Classrel(c, cs)
   3.224 -        })
   3.225 +  def read_classrel(provider: Export.Provider): List[Classrel] =
   3.226 +  {
   3.227 +    val body = provider.uncompressed_yxml(export_prefix + "classrel")
   3.228 +    val classrel =
   3.229 +    {
   3.230 +      import XML.Decode._
   3.231 +      list(pair(string, list(string)))(body)
   3.232 +    }
   3.233 +    for ((c, cs) <- classrel) yield Classrel(c, cs)
   3.234 +  }
   3.235  
   3.236    sealed case class Arity(type_name: String, domain: List[Term.Sort], codomain: String)
   3.237    {
   3.238 @@ -320,18 +299,17 @@
   3.239        Arity(cache.string(type_name), domain.map(cache.sort(_)), cache.string(codomain))
   3.240    }
   3.241  
   3.242 -  def read_arities(db: SQL.Database, session_name: String, theory_name: String): List[Arity] =
   3.243 -    read_export(db, session_name, theory_name, "arities",
   3.244 -      (body: XML.Body) =>
   3.245 -        {
   3.246 -          val arities =
   3.247 -          {
   3.248 -            import XML.Decode._
   3.249 -            import Term_XML.Decode._
   3.250 -            list(triple(string, list(sort), string))(body)
   3.251 -          }
   3.252 -          for ((a, b, c) <- arities) yield Arity(a, b, c)
   3.253 -        })
   3.254 +  def read_arities(provider: Export.Provider): List[Arity] =
   3.255 +  {
   3.256 +    val body = provider.uncompressed_yxml(export_prefix + "arities")
   3.257 +    val arities =
   3.258 +    {
   3.259 +      import XML.Decode._
   3.260 +      import Term_XML.Decode._
   3.261 +      list(triple(string, list(sort), string))(body)
   3.262 +    }
   3.263 +    for ((a, b, c) <- arities) yield Arity(a, b, c)
   3.264 +  }
   3.265  
   3.266  
   3.267    /* HOL typedefs */
   3.268 @@ -348,17 +326,16 @@
   3.269          cache.string(axiom_name))
   3.270    }
   3.271  
   3.272 -  def read_typedefs(db: SQL.Database, session_name: String, theory_name: String): List[Typedef] =
   3.273 -    read_export(db, session_name, theory_name, "typedefs",
   3.274 -      (body: XML.Body) =>
   3.275 -        {
   3.276 -          val typedefs =
   3.277 -          {
   3.278 -            import XML.Decode._
   3.279 -            import Term_XML.Decode._
   3.280 -            list(pair(string, pair(typ, pair(typ, pair(string, pair(string, string))))))(body)
   3.281 -          }
   3.282 -          for { (name, (rep_type, (abs_type, (rep_name, (abs_name, axiom_name))))) <- typedefs }
   3.283 -          yield Typedef(name, rep_type, abs_type, rep_name, abs_name, axiom_name)
   3.284 -        })
   3.285 +  def read_typedefs(provider: Export.Provider): List[Typedef] =
   3.286 +  {
   3.287 +    val body = provider.uncompressed_yxml(export_prefix + "typedefs")
   3.288 +    val typedefs =
   3.289 +    {
   3.290 +      import XML.Decode._
   3.291 +      import Term_XML.Decode._
   3.292 +      list(pair(string, pair(typ, pair(typ, pair(string, pair(string, string))))))(body)
   3.293 +    }
   3.294 +    for { (name, (rep_type, (abs_type, (rep_name, (abs_name, axiom_name))))) <- typedefs }
   3.295 +    yield Typedef(name, rep_type, abs_type, rep_name, abs_name, axiom_name)
   3.296 +  }
   3.297  }
     4.1 --- a/src/Pure/Tools/dump.scala	Mon Jun 11 20:45:51 2018 +0200
     4.2 +++ b/src/Pure/Tools/dump.scala	Mon Jun 11 21:10:03 2018 +0200
     4.3 @@ -78,6 +78,10 @@
     4.4  
     4.5    val default_output_dir = Path.explode("dump")
     4.6  
     4.7 +  def make_options(options: Options, aspects: List[Aspect]): Options =
     4.8 +    (options.int.update("completion_limit", 0).bool.update("ML_statistics", false) /: aspects)(
     4.9 +      { case (opts, aspect) => (opts /: aspect.options)(_ + _) })
    4.10 +
    4.11    def dump(options: Options, logic: String,
    4.12      aspects: List[Aspect] = Nil,
    4.13      progress: Progress = No_Progress,
    4.14 @@ -92,9 +96,7 @@
    4.15      if (Build.build_logic(options, logic, progress = progress, dirs = dirs,
    4.16        system_mode = system_mode) != 0) error(logic + " FAILED")
    4.17  
    4.18 -    val dump_options =
    4.19 -      (options.int.update("completion_limit", 0).bool.update("ML_statistics", false) /: aspects)(
    4.20 -        { case (opts, aspect) => (opts /: aspect.options)(_ + _) })
    4.21 +    val dump_options = make_options(options, aspects)
    4.22  
    4.23  
    4.24      /* dependencies */