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