# HG changeset patch
# User wenzelm
# Date 1729424516 -7200
# Node ID 20d7631b37d7e820b0a95003822d0649f8f3c363
# Parent  893b056542e7915c3278b12623fe24552496b866
more operations;

diff -r 893b056542e7 -r 20d7631b37d7 src/Pure/Syntax/lexicon.ML
--- a/src/Pure/Syntax/lexicon.ML	Sun Oct 20 13:27:17 2024 +0200
+++ b/src/Pure/Syntax/lexicon.ML	Sun Oct 20 13:41:56 2024 +0200
@@ -60,10 +60,10 @@
   val read_int: string -> int option
   val read_num: string -> {radix: int, leading_zeros: int, value: int}
   val read_float: string -> {mant: int, exp: int}
-  val mark_class: string -> string val unmark_class: string -> string
-  val mark_type: string -> string val unmark_type: string -> string
-  val mark_const: string -> string val unmark_const: string -> string
-  val mark_fixed: string -> string val unmark_fixed: string -> string
+  val mark_class: string -> string val unmark_class: string -> string val is_class: string -> bool
+  val mark_type: string -> string val unmark_type: string -> string val is_type: string -> bool
+  val mark_const: string -> string val unmark_const: string -> string val is_const: string -> bool
+  val mark_fixed: string -> string val unmark_fixed: string -> string val is_fixed: string -> bool
   val unmark:
    {case_class: string -> 'a,
     case_type: string -> 'a,
@@ -476,12 +476,12 @@
 
 (* marked logical entities *)
 
-fun marker s = (prefix s, unprefix s);
+fun marker s = (prefix s, unprefix s, String.isPrefix s);
 
-val (mark_class, unmark_class) = marker "\<^class>";
-val (mark_type, unmark_type) = marker "\<^type>";
-val (mark_const, unmark_const) = marker "\<^const>";
-val (mark_fixed, unmark_fixed) = marker "\<^fixed>";
+val (mark_class, unmark_class, is_class) = marker "\<^class>";
+val (mark_type, unmark_type, is_type) = marker "\<^type>";
+val (mark_const, unmark_const, is_const) = marker "\<^const>";
+val (mark_fixed, unmark_fixed, is_fixed) = marker "\<^fixed>";
 
 fun unmark {case_class, case_type, case_const, case_fixed, case_default} s =
   (case try unmark_class s of