--- 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
}
}
--- 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 */
--- 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,
--- 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
--- 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 + ")"
}
--- 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
})