1/* Title: Pure/thm_name.scala 2 Author: Makarius 3 4Systematic naming of individual theorems, as selections from multi-facts. 5*/ 6 7package isabelle 8 9 10import scala.math.Ordering 11 12 13object Thm_Name 14{ 15 object Ordering extends scala.math.Ordering[Thm_Name] 16 { 17 def compare(thm_name1: Thm_Name, thm_name2: Thm_Name): Int = 18 thm_name1.name compare thm_name2.name match { 19 case 0 => thm_name1.index compare thm_name2.index 20 case ord => ord 21 } 22 } 23 24 def graph[A]: Graph[Thm_Name, A] = Graph.empty(Ordering) 25 26 private val Thm_Name_Regex = """^(.)+\((\d+)\)$""".r 27 28 def parse(s: String): Thm_Name = 29 s match { 30 case Thm_Name_Regex(name, Value.Nat(index)) => Thm_Name(name, index) 31 case _ => Thm_Name(s, 0) 32 } 33} 34 35sealed case class Thm_Name(name: String, index: Int) 36{ 37 def print: String = 38 if (name == "" || index == 0) name 39 else name + "(" + index + ")" 40 41 def flatten: String = 42 if (name == "" || index == 0) name 43 else name + "_" + index 44} 45