# HG changeset patch
# User wenzelm
# Date 1724412481 -7200
# Node ID 179a24b4020088f24829c0dd98a1dc79427e070d
# Parent  ec1023a5c54ccb74ace593b83484be333547d913
clarified signature;

diff -r ec1023a5c54c -r 179a24b40200 src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Thu Aug 22 17:12:32 2024 +0200
+++ b/src/Pure/Syntax/syntax.ML	Fri Aug 23 13:28:01 2024 +0200
@@ -77,7 +77,7 @@
   val eq_syntax: syntax * syntax -> bool
   datatype approx = Prefix of string | Infix of {assoc: Printer.assoc, delim: string, pri: int}
   val get_approx: syntax -> string -> approx option
-  val lookup_const: syntax -> string -> string option
+  val get_const: syntax -> string -> string
   val is_const: syntax -> string -> bool
   val is_keyword: syntax -> string -> bool
   val tokenize: syntax -> bool -> Symbol_Pos.T list -> Lexicon.token list
@@ -441,7 +441,6 @@
       | NONE => Printer.get_binder prtabs c)
       |> Option.map Prefix);
 
-fun lookup_const (Syntax ({consts, ...}, _)) = Symtab.lookup consts;
 fun is_const (Syntax ({consts, ...}, _)) = Symtab.defined consts;
 fun is_keyword (Syntax ({lexicon, ...}, _)) = Scan.is_literal lexicon o Symbol.explode;
 fun tokenize (Syntax ({lexicon, ...}, _)) = Lexicon.tokenize lexicon;
@@ -468,6 +467,23 @@
   Synchronized.cache (fn () => Parser.make_gram new_xprods [] NONE);
 
 
+(* syntax consts *)
+
+fun get_const (Syntax ({consts, ...}, _)) =
+  let
+    fun get c =
+      (case Symtab.lookup consts c of
+        NONE => c
+      | SOME "" => c
+      | SOME b => get b);
+  in get end;
+
+fun update_const (c, b) tab =
+  if c = "" orelse (b = "" andalso (Lexicon.is_marked c orelse Symtab.defined tab c))
+  then tab
+  else Symtab.update (c, b) tab;
+
+
 (* empty_syntax *)
 
 val empty_syntax = Syntax
@@ -487,11 +503,6 @@
 
 (* update_syntax *)
 
-fun update_const (c, b) tab =
-  if c = "" orelse (b = "" andalso (Lexicon.is_marked c orelse Symtab.defined tab c))
-  then tab
-  else Symtab.update (c, b) tab;
-
 fun update_syntax (mode, inout) syn_ext (Syntax (tabs, _)) =
   let
     val {input, lexicon, gram, consts = consts1, prmodes, parse_ast_trtab, parse_ruletab,
diff -r ec1023a5c54c -r 179a24b40200 src/Pure/Syntax/syntax_phases.ML
--- a/src/Pure/Syntax/syntax_phases.ML	Thu Aug 22 17:12:32 2024 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML	Fri Aug 23 13:28:01 2024 +0200
@@ -64,15 +64,13 @@
   Markup.bound :: map (fn pos => Position.make_entity_markup def id Markup.boundN (name, pos)) ps;
 
 fun markup_entity ctxt c =
-  (case Syntax.lookup_const (Proof_Context.syntax_of ctxt) c of
-    SOME "" => []
-  | SOME b => markup_entity ctxt b
-  | NONE => c |> Lexicon.unmark
+  Syntax.get_const (Proof_Context.syntax_of ctxt) c
+  |> Lexicon.unmark
      {case_class = markup_class ctxt,
       case_type = markup_type ctxt,
       case_const = markup_const ctxt,
       case_fixed = markup_free ctxt,
-      case_default = K []});
+      case_default = K []};
 
 
 
@@ -738,15 +736,13 @@
     val trf = Syntax.print_ast_translation syn;
 
     fun markup_extern c =
-      (case Syntax.lookup_const syn c of
-        SOME "" => ([], c)
-      | SOME b => markup_extern b
-      | NONE => c |> Lexicon.unmark
+      Syntax.get_const syn c
+      |> Lexicon.unmark
          {case_class = fn x => (markup_class ctxt x, Proof_Context.extern_class ctxt x),
           case_type = fn x => (markup_type ctxt x, Proof_Context.extern_type ctxt x),
           case_const = fn x => (markup_const ctxt x, Proof_Context.extern_const ctxt x),
           case_fixed = fn x => free_or_skolem ctxt x,
-          case_default = fn x => ([], x)});
+          case_default = fn x => ([], x)};
 
     fun token_trans "_tfree" x = SOME (Pretty.mark_str (Markup.tfree, x))
       | token_trans "_tvar" x = SOME (Pretty.mark_str (Markup.tvar, x))