src/Pure/Thy/export_theory.scala
changeset 70384 8ce08b154aa1
parent 69996 8f2d3a27aff0
child 70534 fb876ebbf5a7
     1.1 --- a/src/Pure/Thy/export_theory.scala	Sat Jul 20 11:48:30 2019 +0200
     1.2 +++ b/src/Pure/Thy/export_theory.scala	Sat Jul 20 12:52:29 2019 +0200
     1.3 @@ -440,10 +440,10 @@
     1.4  
     1.5    /* sort algebra */
     1.6  
     1.7 -  sealed case class Classrel(class_name: String, super_names: List[String])
     1.8 +  sealed case class Classrel(class1: String, class2: String, prop: Prop)
     1.9    {
    1.10      def cache(cache: Term.Cache): Classrel =
    1.11 -      Classrel(cache.string(class_name), super_names.map(cache.string(_)))
    1.12 +      Classrel(cache.string(class1), cache.string(class2), prop.cache(cache))
    1.13    }
    1.14  
    1.15    def read_classrel(provider: Export.Provider): List[Classrel] =
    1.16 @@ -452,15 +452,16 @@
    1.17      val classrel =
    1.18      {
    1.19        import XML.Decode._
    1.20 -      list(pair(string, list(string)))(body)
    1.21 +      list(pair(decode_prop, pair(string, string)))(body)
    1.22      }
    1.23 -    for ((c, cs) <- classrel) yield Classrel(c, cs)
    1.24 +    for ((prop, (c1, c2)) <- classrel) yield Classrel(c1, c2, prop)
    1.25    }
    1.26  
    1.27 -  sealed case class Arity(type_name: String, domain: List[Term.Sort], codomain: String)
    1.28 +  sealed case class Arity(type_name: String, domain: List[Term.Sort], codomain: String, prop: Prop)
    1.29    {
    1.30      def cache(cache: Term.Cache): Arity =
    1.31 -      Arity(cache.string(type_name), domain.map(cache.sort(_)), cache.string(codomain))
    1.32 +      Arity(cache.string(type_name), domain.map(cache.sort(_)), cache.string(codomain),
    1.33 +        prop.cache(cache))
    1.34    }
    1.35  
    1.36    def read_arities(provider: Export.Provider): List[Arity] =
    1.37 @@ -470,9 +471,9 @@
    1.38      {
    1.39        import XML.Decode._
    1.40        import Term_XML.Decode._
    1.41 -      list(triple(string, list(sort), string))(body)
    1.42 +      list(pair(decode_prop, triple(string, list(sort), string)))(body)
    1.43      }
    1.44 -    for ((a, b, c) <- arities) yield Arity(a, b, c)
    1.45 +    for ((prop, (a, b, c)) <- arities) yield Arity(a, b, c, prop)
    1.46    }
    1.47  
    1.48