# HG changeset patch
# User wenzelm
# Date 1629805177 -7200
# Node ID 72bb7e9143f794fb238e955568a539d58a512865
# Parent  4ae14c2e7cdd252c3269f7bd9ed5fafa82441188
minor performance tuning;

diff -r 4ae14c2e7cdd -r 72bb7e9143f7 src/Pure/General/position.ML
--- a/src/Pure/General/position.ML	Tue Aug 24 12:37:05 2021 +0200
+++ b/src/Pure/General/position.ML	Tue Aug 24 13:39:37 2021 +0200
@@ -210,7 +210,7 @@
   int_entry Markup.offsetN j @
   int_entry Markup.end_offsetN k;
 
-val def_properties_of = properties_of #> map (fn (x, y) => ("def_" ^ x, y));
+val def_properties_of = properties_of #> map (apfst Markup.def_name);
 
 fun entity_markup kind (name, pos) =
   Markup.entity kind name |> Markup.properties (def_properties_of pos);
diff -r 4ae14c2e7cdd -r 72bb7e9143f7 src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Tue Aug 24 12:37:05 2021 +0200
+++ b/src/Pure/PIDE/markup.ML	Tue Aug 24 13:39:37 2021 +0200
@@ -60,9 +60,10 @@
   val end_offsetN: string
   val fileN: string
   val idN: string
+  val positionN: string val position: T
   val position_properties: string list
   val position_property: Properties.entry -> bool
-  val positionN: string val position: T
+  val def_name: string -> string
   val expressionN: string val expression: string -> T
   val citationN: string val citation: string -> T
   val pathN: string val path: string -> T
@@ -394,10 +395,22 @@
 val fileN = "file";
 val idN = "id";
 
+val (positionN, position) = markup_elem "position";
+
 val position_properties = [lineN, offsetN, end_offsetN, fileN, idN];
 fun position_property (entry: Properties.entry) = member (op =) position_properties (#1 entry);
 
-val (positionN, position) = markup_elem "position";
+
+(* position "def" names *)
+
+fun make_def a = "def_" ^ a;
+
+val def_names = Symtab.make (map (fn a => (a, make_def a)) position_properties);
+
+fun def_name a =
+  (case Symtab.lookup def_names a of
+    SOME b => b
+  | NONE => make_def a);
 
 
 (* expression *)
diff -r 4ae14c2e7cdd -r 72bb7e9143f7 src/Pure/PIDE/markup.scala
--- a/src/Pure/PIDE/markup.scala	Tue Aug 24 12:37:05 2021 +0200
+++ b/src/Pure/PIDE/markup.scala	Tue Aug 24 13:39:37 2021 +0200
@@ -159,10 +159,19 @@
   val DEF_FILE = "def_file"
   val DEF_ID = "def_id"
 
+  val POSITION = "position"
+
   val POSITION_PROPERTIES = Set(LINE, OFFSET, END_OFFSET, FILE, ID)
   def position_property(entry: Properties.Entry): Boolean = POSITION_PROPERTIES(entry._1)
 
-  val POSITION = "position"
+
+  /* position "def" name */
+
+  private val def_names: Map[String, String] =
+    Map(LINE -> DEF_LINE, OFFSET -> DEF_OFFSET, END_OFFSET -> DEF_END_OFFSET,
+      FILE -> DEF_FILE, ID -> DEF_ID)
+
+  def def_name(a: String): String = def_names.getOrElse(a, a + "def_")
 
 
   /* expression */
diff -r 4ae14c2e7cdd -r 72bb7e9143f7 src/Tools/Haskell/Haskell.thy
--- a/src/Tools/Haskell/Haskell.thy	Tue Aug 24 12:37:05 2021 +0200
+++ b/src/Tools/Haskell/Haskell.thy	Tue Aug 24 13:39:37 2021 +0200
@@ -672,6 +672,7 @@
   completionN, completion, no_completionN, no_completion,
 
   lineN, end_lineN, offsetN, end_offsetN, fileN, idN, positionN, position,
+  position_properties, def_name,
 
   expressionN, expression,
 
@@ -711,6 +712,8 @@
 where
 
 import Prelude hiding (words, error, break)
+import Data.Map.Strict (Map)
+import qualified Data.Map.Strict as Map
 
 import Isabelle.Library
 import qualified Isabelle.Properties as Properties
@@ -813,6 +816,24 @@
 position :: T
 position = markup_elem positionN
 
+position_properties :: [Bytes]
+position_properties = [lineN, offsetN, end_offsetN, fileN, idN]
+
+
+{- position "def" names -}
+
+make_def :: Bytes -> Bytes
+make_def a = "def_" <> a
+
+def_names :: Map Bytes Bytes
+def_names = Map.fromList $ map (\a -> (a, make_def a)) position_properties
+
+def_name :: Bytes -> Bytes
+def_name a =
+  case Map.lookup a def_names of
+    Just b -> b
+    Nothing -> make_def a
+
 
 {- expression -}
 
@@ -1191,6 +1212,7 @@
 ) where
 
 import Data.Maybe (isJust, fromMaybe)
+import Data.Bifunctor (first)
 import qualified Isabelle.Properties as Properties
 import qualified Isabelle.Bytes as Bytes
 import qualified Isabelle.Value as Value
@@ -1331,7 +1353,7 @@
   string_entry Markup.idN (_id pos)
 
 def_properties_of :: T -> Properties.T
-def_properties_of = properties_of #> map (\(a, b) -> ("def_" <> a, b))
+def_properties_of = properties_of #> map (first Markup.def_name)
 
 entity_markup :: Bytes -> (Bytes, T) -> Markup.T
 entity_markup kind (name, pos) =