tuned signature: more operations;
authorwenzelm
Thu Aug 02 22:24:16 2018 +0200 (11 months ago)
changeset 68712fc51dcb4e6fd
parent 68711 d1d03b7b6696
child 68713 fb44580680c4
tuned signature: more operations;
src/Pure/Thy/export_theory.scala
     1.1 --- a/src/Pure/Thy/export_theory.scala	Thu Aug 02 21:49:31 2018 +0200
     1.2 +++ b/src/Pure/Thy/export_theory.scala	Thu Aug 02 22:24:16 2018 +0200
     1.3 @@ -174,6 +174,8 @@
     1.4  
     1.5    sealed case class Type(entity: Entity, args: List[String], abbrev: Option[Term.Typ])
     1.6    {
     1.7 +    def kind: String = "type"
     1.8 +
     1.9      def cache(cache: Term.Cache): Type =
    1.10        Type(entity.cache(cache),
    1.11          args.map(cache.string(_)),
    1.12 @@ -198,6 +200,8 @@
    1.13    sealed case class Const(
    1.14      entity: Entity, typargs: List[String], typ: Term.Typ, abbrev: Option[Term.Term])
    1.15    {
    1.16 +    def kind: String = "const"
    1.17 +
    1.18      def cache(cache: Term.Cache): Const =
    1.19        Const(entity.cache(cache),
    1.20          typargs.map(cache.string(_)),
    1.21 @@ -234,6 +238,8 @@
    1.22      args: List[(String, Term.Typ)],
    1.23      prop: Term.Term)
    1.24    {
    1.25 +    def kind: String = "axiom"
    1.26 +
    1.27      def cache(cache: Term.Cache): Axiom =
    1.28        Axiom(entity.cache(cache),
    1.29          typargs.map({ case (name, sort) => (cache.string(name), cache.sort(sort)) }),
    1.30 @@ -255,6 +261,8 @@
    1.31      args: List[(String, Term.Typ)],
    1.32      props: List[Term.Term])
    1.33    {
    1.34 +    def kind: String = "fact"
    1.35 +
    1.36      def cache(cache: Term.Cache): Fact =
    1.37        Fact(entity.cache(cache),
    1.38          typargs.map({ case (name, sort) => (cache.string(name), cache.sort(sort)) }),
    1.39 @@ -276,6 +284,8 @@
    1.40    sealed case class Class(
    1.41      entity: Entity, params: List[(String, Term.Typ)], axioms: List[Term.Term])
    1.42    {
    1.43 +    def kind: String = "class"
    1.44 +
    1.45      def cache(cache: Term.Cache): Class =
    1.46        Class(entity.cache(cache),
    1.47          params.map({ case (name, typ) => (cache.string(name), cache.typ(typ)) }),