support Export_Theory.read_proof, based on theory_name and serial;
authorwenzelm
Thu Aug 15 18:21:12 2019 +0200 (4 days ago)
changeset 7053930b3c58a1933
parent 70538 fc9ba6fe367f
child 70540 04ef5ee3dd4d
support Export_Theory.read_proof, based on theory_name and serial;
src/Pure/PIDE/document.scala
src/Pure/Thy/export.scala
src/Pure/Thy/export_theory.scala
     1.1 --- a/src/Pure/PIDE/document.scala	Thu Aug 15 16:57:09 2019 +0200
     1.2 +++ b/src/Pure/PIDE/document.scala	Thu Aug 15 18:21:12 2019 +0200
     1.3 @@ -390,6 +390,9 @@
     1.4      def iterator: Iterator[(Node.Name, Node)] =
     1.5        graph.iterator.map({ case (name, (node, _)) => (name, node) })
     1.6  
     1.7 +    def theory_name(theory: String): Option[Node.Name] =
     1.8 +      graph.keys_iterator.find(name => name.theory == theory)
     1.9 +
    1.10      def commands_loading(file_name: Node.Name): List[Command] =
    1.11        (for {
    1.12          (_, node) <- iterator
     2.1 --- a/src/Pure/Thy/export.scala	Thu Aug 15 16:57:09 2019 +0200
     2.2 +++ b/src/Pure/Thy/export.scala	Thu Aug 15 18:21:12 2019 +0200
     2.3 @@ -226,6 +226,10 @@
     2.4          def apply(export_name: String): Option[Entry] =
     2.5            read_entry(db, session_name, theory_name, export_name)
     2.6  
     2.7 +        def focus(other_theory: String): Provider =
     2.8 +          if (other_theory == theory_name) this
     2.9 +          else Provider.database(db, session_name, other_theory)
    2.10 +
    2.11          override def toString: String = db.toString
    2.12        }
    2.13  
    2.14 @@ -234,6 +238,15 @@
    2.15          def apply(export_name: String): Option[Entry] =
    2.16            snapshot.exports_map.get(export_name)
    2.17  
    2.18 +        def focus(other_theory: String): Provider =
    2.19 +          if (other_theory == snapshot.node_name.theory) this
    2.20 +          else {
    2.21 +            val node_name =
    2.22 +              snapshot.version.nodes.theory_name(other_theory) getOrElse
    2.23 +                error("Bad theory " + quote(other_theory))
    2.24 +            Provider.snapshot(snapshot.state.snapshot(node_name))
    2.25 +          }
    2.26 +
    2.27          override def toString: String = snapshot.toString
    2.28        }
    2.29  
    2.30 @@ -242,6 +255,10 @@
    2.31          def apply(export_name: String): Option[Entry] =
    2.32            read_entry(dir, session_name, theory_name, export_name)
    2.33  
    2.34 +        def focus(other_theory: String): Provider =
    2.35 +          if (other_theory == theory_name) this
    2.36 +          else Provider.directory(dir, session_name, other_theory)
    2.37 +
    2.38          override def toString: String = dir.toString
    2.39        }
    2.40    }
    2.41 @@ -255,6 +272,8 @@
    2.42          case Some(entry) => entry.uncompressed_yxml(cache = cache)
    2.43          case None => Nil
    2.44        }
    2.45 +
    2.46 +    def focus(other_theory: String): Provider
    2.47    }
    2.48  
    2.49  
     3.1 --- a/src/Pure/Thy/export_theory.scala	Thu Aug 15 16:57:09 2019 +0200
     3.2 +++ b/src/Pure/Thy/export_theory.scala	Thu Aug 15 18:21:12 2019 +0200
     3.3 @@ -65,6 +65,7 @@
     3.4    /** theory content **/
     3.5  
     3.6    val export_prefix: String = "theory/"
     3.7 +  val export_prefix_proofs: String = "proofs/"
     3.8  
     3.9    sealed case class Theory(name: String, parents: List[String],
    3.10      types: List[Type],
    3.11 @@ -367,6 +368,21 @@
    3.12          Fact_Multi(entity, facts)
    3.13        })
    3.14  
    3.15 +  def read_proof(
    3.16 +    provider: Export.Provider,
    3.17 +    theory_name: String,
    3.18 +    serial: Long,
    3.19 +    cache: Option[Term.Cache] = None): (Term.Term, Term.Proof) =
    3.20 +  {
    3.21 +    val body = provider.focus(theory_name).uncompressed_yxml(export_prefix_proofs + serial)
    3.22 +    if (body.isEmpty) error("Bad proof export " + serial)
    3.23 +    val (prop, proof) = XML.Decode.pair(Term_XML.Decode.term, Term_XML.Decode.proof)(body)
    3.24 +    cache match {
    3.25 +      case None => (prop, proof)
    3.26 +      case Some(cache) => (cache.term(prop), cache.proof(proof))
    3.27 +    }
    3.28 +  }
    3.29 +
    3.30  
    3.31    /* type classes */
    3.32