Indexname.toString according to string_of_vname' in ML;
authorwenzelm
Thu Aug 15 16:38:55 2019 +0200 (4 days ago)
changeset 7053717160e0a60b6
parent 70536 fe4d545f12e3
child 70538 fc9ba6fe367f
Indexname.toString according to string_of_vname' in ML;
src/Pure/term.scala
     1.1 --- a/src/Pure/term.scala	Thu Aug 15 16:26:50 2019 +0200
     1.2 +++ b/src/Pure/term.scala	Thu Aug 15 16:38:55 2019 +0200
     1.3 @@ -14,6 +14,21 @@
     1.4    /* types and terms */
     1.5  
     1.6    sealed case class Indexname(name: String, index: Int)
     1.7 +  {
     1.8 +    override def toString: String =
     1.9 +      if (index == -1) name
    1.10 +      else {
    1.11 +        val dot =
    1.12 +          Symbol.explode(name).reverse match {
    1.13 +            case _ :: s :: _ if s == Symbol.sub_decoded || s == Symbol.sub => false
    1.14 +            case c :: _ => Symbol.is_digit(c)
    1.15 +            case _ => true
    1.16 +          }
    1.17 +        if (dot) "?" + name + "." + index
    1.18 +        else if (index != 0) "?" + name + index
    1.19 +        else "?" + name
    1.20 +      }
    1.21 +  }
    1.22  
    1.23    type Sort = List[String]
    1.24    val dummyS: Sort = List("")