# HG changeset patch
# User wenzelm
# Date 1733684954 -3600
# Node ID bf19ea589f9974f5438d0c7a486cf5a066642bcf
# Parent  56075edacb1082255fd7b029fde13b190ea02093
more markup (without rendering): class, type constructor, term constant --- similar to free, bound, etc.;

diff -r 56075edacb10 -r bf19ea589f99 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Sun Dec 08 19:05:05 2024 +0100
+++ b/src/Pure/Isar/proof_context.ML	Sun Dec 08 20:09:14 2024 +0100
@@ -529,7 +529,7 @@
             [Name_Space.completion (Context.Proof ctxt) class_space (K true) (xname, pos)]);
     val reports =
       if Context_Position.is_reported ctxt pos
-      then [(pos, Name_Space.markup class_space name)] else [];
+      then [(pos, Name_Space.markup class_space name), (pos, Markup.tclass)] else [];
   in (name, reports) end;
 
 fun read_class ctxt text =
@@ -589,10 +589,13 @@
   else
     let
       val ((d, reports), decl) = Type.check_decl (Context.Proof ctxt) (tsig_of ctxt) (c, pos);
+      val reports' =
+        if Context_Position.is_reported ctxt pos
+        then reports @ [(pos, Markup.tconst)] else reports;
       val _ =
         if strict andalso not (Type.decl_logical decl)
         then error ("Bad type name: " ^ quote d ^ Position.here pos) else ();
-    in (Type (d, replicate (Type.decl_args decl) dummyT), reports) end;
+    in (Type (d, replicate (Type.decl_args decl) dummyT), reports') end;
 
 fun read_type_name flags ctxt text =
   let
@@ -620,23 +623,32 @@
     val const = Variable.lookup_const ctxt c;
     val consts = consts_of ctxt;
 
+    val is_reported = Context_Position.is_reported ctxt;
     val (t, reports) =
       if is_some fixed andalso is_none const then
         let
           val x = the fixed;
-          val reports = ps
-            |> filter (Context_Position.is_reported ctxt)
-            |> map (fn pos => (pos, Markup.name x (Variable.markup ctxt x)));
+          val reports =
+            ps |> maps (fn pos =>
+              if is_reported pos then [(pos, Markup.name x (Variable.markup ctxt x))]
+              else []);
         in (Free (x, infer_type ctxt (x, dummyT)), reports) end
       else if is_some const then
         let
           val d = the const;
           val T = Consts.type_scheme consts d handle TYPE (msg, _, _) => err msg;
-          val reports = ps
-            |> filter (Context_Position.is_reported ctxt)
-            |> map (fn pos => (pos, Name_Space.markup (Consts.space_of consts) d));
+          val reports =
+            ps |> maps (fn pos =>
+              if is_reported pos then
+                [(pos, Name_Space.markup (Consts.space_of consts) d), (pos, Markup.const)]
+              else []);
         in (Const (d, T), reports) end
-      else Consts.check_const (Context.Proof ctxt) consts (c, ps);
+      else
+        let
+          val (d, reports1) = Consts.check_const (Context.Proof ctxt) consts (c, ps);
+          val reports2 =
+            ps |> maps (fn pos => if is_reported pos then [(pos, Markup.const)] else []);
+        in (d, reports1 @ reports2) end;
     val _ =
       (case (strict, t) of
         (true, Const (d, _)) =>
diff -r 56075edacb10 -r bf19ea589f99 src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Sun Dec 08 19:05:05 2024 +0100
+++ b/src/Pure/PIDE/markup.ML	Sun Dec 08 20:09:14 2024 +0100
@@ -114,8 +114,11 @@
   val attributeN: string
   val methodN: string
   val method_modifierN: string
+  val tclassN: string val tclass: T
+  val tconstN: string val tconst: T
   val tfreeN: string val tfree: T
   val tvarN: string val tvar: T
+  val constN: string val const: T
   val freeN: string val free: T
   val skolemN: string val skolem: T
   val boundN: string val bound: T
@@ -542,8 +545,11 @@
 
 (* inner syntax *)
 
+val (tclassN, tclass) = markup_elem "tclass";
+val (tconstN, tconst) = markup_elem "tconst";
 val (tfreeN, tfree) = markup_elem "tfree";
 val (tvarN, tvar) = markup_elem "tvar";
+val (constN, const) = markup_elem "const";
 val (freeN, free) = markup_elem "free";
 val (skolemN, skolem) = markup_elem "skolem";
 val (boundN, bound) = markup_elem "bound";
@@ -681,7 +687,7 @@
 
 val syntaxN = "syntax";
 
-val syntax_elements = [improperN, freeN, skolemN];
+val syntax_elements = [tclassN, tconstN, improperN, constN, freeN, skolemN];
 
 fun syntax_properties syntax (m as (elem, props): T) =
   if syntax andalso member (op =) syntax_elements elem
diff -r 56075edacb10 -r bf19ea589f99 src/Pure/PIDE/markup.scala
--- a/src/Pure/PIDE/markup.scala	Sun Dec 08 19:05:05 2024 +0100
+++ b/src/Pure/PIDE/markup.scala	Sun Dec 08 20:09:14 2024 +0100
@@ -334,8 +334,11 @@
 
   /* inner syntax */
 
+  val TCLASS = "tclass"
+  val TCONST = "tconst"
   val TFREE = "tfree"
   val TVAR = "tvar"
+  val CONST = "const"
   val FREE = "free"
   val SKOLEM = "skolem"
   val BOUND = "bound"
diff -r 56075edacb10 -r bf19ea589f99 src/Pure/Syntax/syntax_phases.ML
--- a/src/Pure/Syntax/syntax_phases.ML	Sun Dec 08 19:05:05 2024 +0100
+++ b/src/Pure/Syntax/syntax_phases.ML	Sun Dec 08 20:09:14 2024 +0100
@@ -44,13 +44,13 @@
 (** markup logical entities **)
 
 fun markup_class ctxt c =
-  [Name_Space.markup (Type.class_space (Proof_Context.tsig_of ctxt)) c];
+  [Name_Space.markup (Type.class_space (Proof_Context.tsig_of ctxt)) c, Markup.tclass];
 
 fun markup_type ctxt c =
-  [Name_Space.markup (Type.type_space (Proof_Context.tsig_of ctxt)) c];
+  [Name_Space.markup (Type.type_space (Proof_Context.tsig_of ctxt)) c, Markup.tconst];
 
 fun markup_const ctxt c =
-  [Name_Space.markup (Consts.space_of (Proof_Context.consts_of ctxt)) c];
+  [Name_Space.markup (Consts.space_of (Proof_Context.consts_of ctxt)) c, Markup.const];
 
 fun markup_free ctxt x =
   let