# HG changeset patch
# User wenzelm
# Date 1724335050 -7200
# Node ID 60801e5fae26140ec351be2defbfaed1a0b4b50d
# Parent  0c406b9469ab15678d44e8648a40a9c838b9bb0f
tuned signature: more operations;

diff -r 0c406b9469ab -r 60801e5fae26 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Wed Aug 21 20:41:16 2024 +0200
+++ b/src/Pure/Isar/proof_context.ML	Thu Aug 22 15:57:30 2024 +0200
@@ -1127,7 +1127,7 @@
 (* syntax *)
 
 fun check_syntax_const ctxt (c, pos) =
-  if is_some (Syntax.lookup_const (syntax_of ctxt) c) then c
+  if Syntax.is_const (syntax_of ctxt) c then c
   else error ("Unknown syntax const: " ^ quote c ^ Position.here pos);
 
 fun syntax add mode args ctxt =
diff -r 0c406b9469ab -r 60801e5fae26 src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Wed Aug 21 20:41:16 2024 +0200
+++ b/src/Pure/Syntax/syntax.ML	Thu Aug 22 15:57:30 2024 +0200
@@ -78,6 +78,7 @@
   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 is_const: syntax -> string -> bool
   val is_keyword: syntax -> string -> bool
   val tokenize: syntax -> bool -> Symbol_Pos.T list -> Lexicon.token list
   val parse: syntax -> string -> Lexicon.token list -> Parser.parsetree list
@@ -441,6 +442,7 @@
       |> 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;
 fun parse (Syntax ({gram, ...}, _)) = Parser.parse (cache_eval gram);
diff -r 0c406b9469ab -r 60801e5fae26 src/Pure/Syntax/syntax_phases.ML
--- a/src/Pure/Syntax/syntax_phases.ML	Wed Aug 21 20:41:16 2024 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML	Thu Aug 22 15:57:30 2024 +0200
@@ -468,7 +468,7 @@
     fun decode_appl ps asts = Ast.Appl (map (decode ps) asts)
     and decode ps (Ast.Constant c) = decode_const ps c
       | decode ps (Ast.Variable x) =
-          if is_some (Syntax.lookup_const syn x) orelse Long_Name.is_qualified x
+          if Syntax.is_const syn x orelse Long_Name.is_qualified x
           then decode_const ps x
           else decode_var ps x
       | decode ps (Ast.Appl (asts as (Ast.Constant c :: ast :: Ast.Variable x :: args))) =
@@ -803,7 +803,7 @@
     val thy = Proof_Context.theory_of ctxt;
     val syn = Proof_Context.syntax_of ctxt;
   in
-    unparse_t (term_to_ast (is_some o Syntax.lookup_const syn))
+    unparse_t (term_to_ast (Syntax.is_const syn))
       (Printer.pretty_term_ast (not (Pure_Thy.old_appl_syntax thy)))
       (Markup.language_term false) ctxt
   end;