Indexname.toString according to string_of_vname' in ML;
authorwenzelm
Thu, 15 Aug 2019 16:38:55 +0200
changeset 70537 17160e0a60b6
parent 70536 fe4d545f12e3
child 70538 fc9ba6fe367f
Indexname.toString according to string_of_vname' in ML;
src/Pure/term.scala
--- a/src/Pure/term.scala	Thu Aug 15 16:26:50 2019 +0200
+++ b/src/Pure/term.scala	Thu Aug 15 16:38:55 2019 +0200
@@ -14,6 +14,21 @@
   /* types and terms */
 
   sealed case class Indexname(name: String, index: Int)
+  {
+    override def toString: String =
+      if (index == -1) name
+      else {
+        val dot =
+          Symbol.explode(name).reverse match {
+            case _ :: s :: _ if s == Symbol.sub_decoded || s == Symbol.sub => false
+            case c :: _ => Symbol.is_digit(c)
+            case _ => true
+          }
+        if (dot) "?" + name + "." + index
+        else if (index != 0) "?" + name + index
+        else "?" + name
+      }
+  }
 
   type Sort = List[String]
   val dummyS: Sort = List("")