module Thm_Name for Isabelle/Scala;

--- a/src/Pure/build-jars	Mon Aug 19 19:24:18 2019 +0200
+++ b/src/Pure/build-jars	Mon Aug 19 19:31:31 2019 +0200
@@ -171,6 +171,7 @@
   pure_thy.scala
   term.scala
   term_xml.scala
+  thm_name.scala
   ../Tools/Graphview/graph_file.scala
   ../Tools/Graphview/graph_panel.scala
   ../Tools/Graphview/graphview.scala

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/thm_name.scala	Mon Aug 19 19:31:31 2019 +0200
@@ -0,0 +1,36 @@
+/*  Title:      Pure/thm_name.scala
+    Author:     Makarius
+
+Systematic naming of individual theorems, as selections from multi-facts.
+*/
+
+package isabelle
+
+
+import scala.math.Ordering
+
+
+object Thm_Name
+{
+  object Ordering extends scala.math.Ordering[Thm_Name]
+  {
+    def compare(thm_name1: Thm_Name, thm_name2: Thm_Name): Int =
+      thm_name1.name compare thm_name2.name match {
+        case 0 => thm_name1.index compare thm_name2.index
+        case ord => ord
+      }
+  }
+
+  def graph[A]: Graph[Thm_Name, A] = Graph.empty(Ordering)
+}
+
+sealed case class Thm_Name(name: String, index: Int)
+{
+  override def toString: String =
+    if (name == "" || index == 0) name
+    else name + "(" + index + ")"
+
+  def flatten: String =
+    if (name == "" || index == 0) name
+    else name + "_" + index
+}