# HG changeset patch # User wenzelm # Date 1566243114 -7200 # Node ID e6101f131d0d75987bad539a51083e8759db4306 # Parent 5a8e3e4b37604daa18491110950cf9c41245e5f3 clarified signature; diff -r 5a8e3e4b3760 -r e6101f131d0d src/Pure/thm_name.scala --- a/src/Pure/thm_name.scala Mon Aug 19 21:23:13 2019 +0200 +++ b/src/Pure/thm_name.scala Mon Aug 19 21:31:54 2019 +0200 @@ -22,11 +22,19 @@ } def graph[A]: Graph[Thm_Name, A] = Graph.empty(Ordering) + + private val Thm_Name_Regex = """^(.)+\((\d+)\)$""".r + + def parse(s: String): Thm_Name = + s match { + case Thm_Name_Regex(name, Value.Nat(index)) => Thm_Name(name, index) + case _ => Thm_Name(s, 0) + } } sealed case class Thm_Name(name: String, index: Int) { - override def toString: String = + def print: String = if (name == "" || index == 0) name else name + "(" + index + ")"