# HG changeset patch
# User wenzelm
# Date 1636899700 -3600
# Node ID 0a87ea7eb76fd5238895a16013b46c71845d781f
# Parent  ffd64082550523c3ac7a3682f3d56c43cc25568c
clarified signature;

diff -r ffd640825505 -r 0a87ea7eb76f src/Pure/Admin/build_log.scala
--- a/src/Pure/Admin/build_log.scala	Sat Nov 13 20:12:34 2021 +0100
+++ b/src/Pure/Admin/build_log.scala	Sun Nov 14 15:21:40 2021 +0100
@@ -491,7 +491,7 @@
         match {
           case Some((SESSION_NAME, session) :: props) =>
             for (theory <- Markup.Name.unapply(props))
-            yield (session, theory -> Markup.Timing_Properties.parse(props))
+            yield (session, theory -> Markup.Timing_Properties.get(props))
           case _ => None
         }
     }
diff -r ffd640825505 -r 0a87ea7eb76f src/Pure/PIDE/markup.scala
--- a/src/Pure/PIDE/markup.scala	Sat Nov 13 20:12:34 2021 +0100
+++ b/src/Pure/PIDE/markup.scala	Sun Nov 14 15:21:40 2021 +0100
@@ -63,29 +63,32 @@
 
   class Markup_String(val name: String, prop: String)
   {
-    private val Prop = new Properties.String(prop)
+    val Prop: Properties.String = new Properties.String(prop)
 
     def apply(s: String): Markup = Markup(name, Prop(s))
     def unapply(markup: Markup): Option[String] =
       if (markup.name == name) Prop.unapply(markup.properties) else None
+    def get(markup: Markup): String = unapply(markup).getOrElse("")
   }
 
   class Markup_Int(val name: String, prop: String)
   {
-    private val Prop = new Properties.Int(prop)
+    val Prop: Properties.Int = new Properties.Int(prop)
 
     def apply(i: Int): Markup = Markup(name, Prop(i))
     def unapply(markup: Markup): Option[Int] =
       if (markup.name == name) Prop.unapply(markup.properties) else None
+    def get(markup: Markup): Int = unapply(markup).getOrElse(0)
   }
 
   class Markup_Long(val name: String, prop: String)
   {
-    private val Prop = new Properties.Long(prop)
+    val Prop: Properties.Long = new Properties.Long(prop)
 
     def apply(i: Long): Markup = Markup(name, Prop(i))
     def unapply(markup: Markup): Option[Long] =
       if (markup.name == name) Prop.unapply(markup.properties) else None
+    def get(markup: Markup): Long = unapply(markup).getOrElse(0)
   }
 
 
@@ -104,21 +107,11 @@
   val BINDING = "binding"
   val ENTITY = "entity"
 
-  val Def = new Properties.Long("def")
-  val Ref = new Properties.Long("ref")
-
   object Entity
   {
-    object Def
-    {
-      def unapply(markup: Markup): Option[Long] =
-        if (markup.name == ENTITY) Markup.Def.unapply(markup.properties) else None
-    }
-    object Ref
-    {
-      def unapply(markup: Markup): Option[Long] =
-        if (markup.name == ENTITY) Markup.Ref.unapply(markup.properties) else None
-    }
+    val Def = new Markup_Long(ENTITY, "def")
+    val Ref = new Markup_Long(ENTITY, "ref")
+
     object Occ
     {
       def unapply(markup: Markup): Option[Long] =
@@ -127,10 +120,7 @@
 
     def unapply(markup: Markup): Option[(String, String)] =
       markup match {
-        case Markup(ENTITY, props) =>
-          val kind = Kind.unapply(props).getOrElse("")
-          val name = Name.unapply(props).getOrElse("")
-          Some((kind, name))
+        case Markup(ENTITY, props) => Some((Kind.get(props), Name.get(props)))
         case _ => None
       }
   }
@@ -183,8 +173,7 @@
   {
     def unapply(markup: Markup): Option[String] =
       markup match {
-        case Markup(EXPRESSION, Kind(kind)) => Some(kind)
-        case Markup(EXPRESSION, _) => Some("")
+        case Markup(EXPRESSION, props) => Some(Kind.get(props))
         case _ => None
       }
   }
@@ -263,8 +252,8 @@
         (if (i != 0) Indent(i) else Nil))
     def unapply(markup: Markup): Option[(Boolean, Int)] =
       if (markup.name == name) {
-        val c = Consistent.unapply(markup.properties).getOrElse(false)
-        val i = Indent.unapply(markup.properties).getOrElse(0)
+        val c = Consistent.get(markup.properties)
+        val i = Indent.get(markup.properties)
         Some((c, i))
       }
       else None
@@ -279,8 +268,8 @@
         (if (i != 0) Indent(i) else Nil))
     def unapply(markup: Markup): Option[(Int, Int)] =
       if (markup.name == name) {
-        val w = Width.unapply(markup.properties).getOrElse(0)
-        val i = Indent.unapply(markup.properties).getOrElse(0)
+        val w = Width.get(markup.properties)
+        val i = Indent.get(markup.properties)
         Some((w, i))
       }
       else None
@@ -364,17 +353,10 @@
   val PARAGRAPH = "paragraph"
   val TEXT_FOLD = "text_fold"
 
-  object Document_Tag
+  object Document_Tag extends Markup_String("document_tag", NAME)
   {
-    val ELEMENT = "document_tag"
     val IMPORTANT = "important"
     val UNIMPORTANT = "unimportant"
-
-    def unapply(markup: Markup): Option[String] =
-      markup match {
-        case Markup(ELEMENT, Name(name)) => Some(name)
-        case _ => None
-      }
   }
 
   val DOCUMENT_LATEX = "document_latex"
@@ -459,8 +441,8 @@
         case _ => None
       }
 
-    def parse(props: Properties.T): isabelle.Timing =
-      unapply(props) getOrElse isabelle.Timing.zero
+    def get(props: Properties.T): isabelle.Timing =
+      unapply(props).getOrElse(isabelle.Timing.zero)
   }
 
   val TIMING = "timing"
@@ -499,12 +481,7 @@
 
   /* command indentation */
 
-  object Command_Indent
-  {
-    val name = "command_indent"
-    def unapply(markup: Markup): Option[Int] =
-      if (markup.name == name) Indent.unapply(markup.properties) else None
-  }
+  val Command_Indent = new Markup_Int("command_indent", Indent.name)
 
 
   /* goals */
diff -r ffd640825505 -r 0a87ea7eb76f src/Pure/PIDE/rendering.scala
--- a/src/Pure/PIDE/rendering.scala	Sat Nov 13 20:12:34 2021 +0100
+++ b/src/Pure/PIDE/rendering.scala	Sun Nov 14 15:21:40 2021 +0100
@@ -257,7 +257,7 @@
       Markup.META_DATE, Markup.META_DESCRIPTION, Markup.META_LICENSE)
 
   val document_tag_elements =
-    Markup.Elements(Markup.Document_Tag.ELEMENT)
+    Markup.Elements(Markup.Document_Tag.name)
 
   val markdown_elements =
     Markup.Elements(Markup.MARKDOWN_PARAGRAPH, Markup.MARKDOWN_ITEM, Markup.Markdown_List.name,
diff -r ffd640825505 -r 0a87ea7eb76f src/Pure/Thy/presentation.scala
--- a/src/Pure/Thy/presentation.scala	Sat Nov 13 20:12:34 2021 +0100
+++ b/src/Pure/Thy/presentation.scala	Sun Nov 14 15:21:40 2021 +0100
@@ -129,7 +129,8 @@
     {
       def unapply(props: Properties.T): Option[(Path, Option[String], String, String)] =
         (props, props, props, props) match {
-          case (Markup.Ref(_), Position.Def_File(def_file), Markup.Kind(kind), Markup.Name(name)) =>
+          case (Markup.Entity.Ref.Prop(_), Position.Def_File(def_file),
+              Markup.Kind(kind), Markup.Name(name)) =>
             val def_theory = Position.Def_Theory.unapply(props)
             Some((Path.explode(def_file), def_theory, kind, name))
           case _ => None
diff -r ffd640825505 -r 0a87ea7eb76f src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Sat Nov 13 20:12:34 2021 +0100
+++ b/src/Pure/Tools/build.scala	Sun Nov 14 15:21:40 2021 +0100
@@ -161,7 +161,7 @@
   {
     val props = build_log.session_timing
     val threads = Markup.Session_Timing.Threads.unapply(props) getOrElse 1
-    val timing = Markup.Timing_Properties.parse(props)
+    val timing = Markup.Timing_Properties.get(props)
     "Timing " + session_name + " (" + threads + " threads, " + timing.message_factor + ")"
   }
 
diff -r ffd640825505 -r 0a87ea7eb76f src/Tools/jEdit/src/jedit_rendering.scala
--- a/src/Tools/jEdit/src/jedit_rendering.scala	Sat Nov 13 20:12:34 2021 +0100
+++ b/src/Tools/jEdit/src/jedit_rendering.scala	Sun Nov 14 15:21:40 2021 +0100
@@ -228,8 +228,8 @@
   def entity_ref(range: Text.Range, focus: Rendering.Focus): List[Text.Info[Color]] =
     snapshot.select(range, Rendering.entity_elements, _ =>
       {
-        case Text.Info(_, XML.Elem(Markup(Markup.ENTITY, Markup.Ref(i)), _))
-        if focus(i) => Some(entity_ref_color)
+        case Text.Info(_, XML.Elem(Markup.Entity.Ref(i), _)) if focus(i) =>
+          Some(entity_ref_color)
         case _ => None
       })