src/Pure/Thy/export_theory.scala
changeset 68717 54a5043d4cd5
parent 68716 040c6298850b
child 68718 ce18a3924864
equal deleted inserted replaced
68716:040c6298850b 68717:54a5043d4cd5
   156     val CLASS = Value("class")
   156     val CLASS = Value("class")
   157   }
   157   }
   158 
   158 
   159   sealed case class Entity(kind: Kind.Value, name: String, serial: Long, pos: Position.T)
   159   sealed case class Entity(kind: Kind.Value, name: String, serial: Long, pos: Position.T)
   160   {
   160   {
   161     def kind_name: (Kind.Value, String) = (kind, name)
       
   162 
       
   163     override def toString: String = kind.toString + quote(name)
   161     override def toString: String = kind.toString + quote(name)
   164 
   162 
   165     def cache(cache: Term.Cache): Entity =
   163     def cache(cache: Term.Cache): Entity =
   166       Entity(kind, cache.string(name), serial, cache.position(pos))
   164       Entity(kind, cache.string(name), serial, cache.position(pos))
   167   }
   165   }