# HG changeset patch
# User wenzelm
# Date 1712075354 -7200
# Node ID 951c371c1cd96b8f49051e336bce1242dbbe9f69
# Parent  40f5ddeda2b4b9f8ec0fe204aebfe0337d459ffc
clarified names: discontinue odd convention from 3 decades ago;

diff -r 40f5ddeda2b4 -r 951c371c1cd9 src/Pure/Build/export_theory.ML
--- a/src/Pure/Build/export_theory.ML	Tue Apr 02 17:20:09 2024 +0200
+++ b/src/Pure/Build/export_theory.ML	Tue Apr 02 18:29:14 2024 +0200
@@ -38,7 +38,7 @@
 
 (* approximative syntax *)
 
-val get_syntax = Syntax.get_approx o Proof_Context.syn_of;
+val get_syntax = Syntax.get_approx o Proof_Context.syntax_of;
 fun get_syntax_type ctxt = get_syntax ctxt o Lexicon.mark_type;
 fun get_syntax_const ctxt = get_syntax ctxt o Lexicon.mark_const;
 fun get_syntax_fixed ctxt = get_syntax ctxt o Lexicon.mark_fixed;
diff -r 40f5ddeda2b4 -r 951c371c1cd9 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Tue Apr 02 17:20:09 2024 +0200
+++ b/src/Pure/Isar/proof_context.ML	Tue Apr 02 18:29:14 2024 +0200
@@ -20,7 +20,7 @@
   val get_mode: Proof.context -> mode
   val restore_mode: Proof.context -> Proof.context -> Proof.context
   val abbrev_mode: Proof.context -> bool
-  val syn_of: Proof.context -> Syntax.syntax
+  val syntax_of: Proof.context -> Syntax.syntax
   val tsig_of: Proof.context -> Type.tsig
   val set_defsort: sort -> Proof.context -> Proof.context
   val default_sort: Proof.context -> indexname -> sort
@@ -312,10 +312,9 @@
 val restore_mode = set_mode o get_mode;
 val abbrev_mode = get_mode #> (fn Mode {abbrev, ...} => abbrev);
 
-val syntax_of = #syntax o rep_data;
-val syn_of = Local_Syntax.syn_of o syntax_of;
+val syntax_of = Local_Syntax.syntax_of o #syntax o rep_data;
 val set_syntax_mode = map_syntax o Local_Syntax.set_mode;
-val restore_syntax_mode = map_syntax o Local_Syntax.restore_mode o syntax_of;
+val restore_syntax_mode = map_syntax o Local_Syntax.restore_mode o #syntax o rep_data;
 
 val tsig_of = #1 o #tsig o rep_data;
 val set_defsort = map_tsig o apfst o Type.set_defsort;
@@ -1124,7 +1123,7 @@
 (* syntax *)
 
 fun check_syntax_const ctxt (c, pos) =
-  if is_some (Syntax.lookup_const (syn_of ctxt) c) then c
+  if is_some (Syntax.lookup_const (syntax_of ctxt) c) then c
   else error ("Unknown syntax const: " ^ quote c ^ Position.here pos);
 
 fun syntax add mode args ctxt =
@@ -1438,7 +1437,7 @@
 
 (* local syntax *)
 
-val print_syntax = Syntax.print_syntax o syn_of;
+val print_syntax = Syntax.print_syntax o syntax_of;
 
 
 (* abbreviations *)
diff -r 40f5ddeda2b4 -r 951c371c1cd9 src/Pure/Syntax/local_syntax.ML
--- a/src/Pure/Syntax/local_syntax.ML	Tue Apr 02 17:20:09 2024 +0200
+++ b/src/Pure/Syntax/local_syntax.ML	Tue Apr 02 18:29:14 2024 +0200
@@ -8,7 +8,7 @@
 signature LOCAL_SYNTAX =
 sig
   type T
-  val syn_of: T -> Syntax.syntax
+  val syntax_of: T -> Syntax.syntax
   val init: theory -> T
   val rebuild: theory -> T -> T
   datatype kind = Type | Const | Fixed
@@ -43,16 +43,16 @@
   make_syntax (f (thy_syntax, local_syntax, mode, mixfixes));
 
 fun is_consistent thy (Syntax {thy_syntax, ...}) =
-  Syntax.eq_syntax (Sign.syn_of thy, thy_syntax);
+  Syntax.eq_syntax (Sign.syntax_of thy, thy_syntax);
 
-fun syn_of (Syntax {local_syntax, ...}) = local_syntax;
+fun syntax_of (Syntax {local_syntax, ...}) = local_syntax;
 
 
 (* build syntax *)
 
 fun build_syntax thy mode mixfixes =
   let
-    val thy_syntax = Sign.syn_of thy;
+    val thy_syntax = Sign.syntax_of thy;
     fun update_gram ((true, add, m), decls) = Syntax.update_type_gram add m decls
       | update_gram ((false, add, m), decls) =
           Syntax.update_const_gram add (Sign.logical_types thy) m decls;
@@ -62,7 +62,7 @@
   in make_syntax (thy_syntax, local_syntax, mode, mixfixes) end;
 
 fun init thy =
-  let val thy_syntax = Sign.syn_of thy
+  let val thy_syntax = Sign.syntax_of thy
   in make_syntax (thy_syntax, thy_syntax, Syntax.mode_default, []) end;
 
 fun rebuild thy (syntax as Syntax {mode, mixfixes, ...}) =
diff -r 40f5ddeda2b4 -r 951c371c1cd9 src/Pure/Syntax/syntax_phases.ML
--- a/src/Pure/Syntax/syntax_phases.ML	Tue Apr 02 17:20:09 2024 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML	Tue Apr 02 18:29:14 2024 +0200
@@ -64,7 +64,7 @@
   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.syn_of ctxt) c of
+  (case Syntax.lookup_const (Proof_Context.syntax_of ctxt) c of
     SOME "" => []
   | SOME b => markup_entity ctxt b
   | NONE => c |> Lexicon.unmark
@@ -338,7 +338,7 @@
 
 fun parse_asts ctxt raw root (syms, pos) =
   let
-    val syn = Proof_Context.syn_of ctxt;
+    val syn = Proof_Context.syntax_of ctxt;
     val ast_tr = Syntax.parse_ast_translation syn;
 
     val toks = Syntax.tokenize syn raw syms;
@@ -364,7 +364,7 @@
 
 fun parse_tree ctxt root input =
   let
-    val syn = Proof_Context.syn_of ctxt;
+    val syn = Proof_Context.syntax_of ctxt;
     val tr = Syntax.parse_translation syn;
     val parse_rules = Syntax.parse_rules syn;
     val (ambig_msgs, asts) = parse_asts ctxt false root input;
@@ -458,7 +458,7 @@
 
 fun parse_ast_pattern ctxt (root, str) =
   let
-    val syn = Proof_Context.syn_of ctxt;
+    val syn = Proof_Context.syntax_of ctxt;
 
     val reports = Unsynchronized.ref ([]: Position.report_text list);
     fun report ps = Position.store_reports reports ps;
@@ -731,7 +731,7 @@
     val show_sorts = Config.get ctxt show_sorts;
     val show_types = Config.get ctxt show_types orelse show_sorts;
 
-    val syn = Proof_Context.syn_of ctxt;
+    val syn = Proof_Context.syntax_of ctxt;
     val prtabs = Syntax.prtabs syn;
     val trf = Syntax.print_ast_translation syn;
 
@@ -801,7 +801,7 @@
 fun unparse_term ctxt =
   let
     val thy = Proof_Context.theory_of ctxt;
-    val syn = Proof_Context.syn_of ctxt;
+    val syn = Proof_Context.syntax_of ctxt;
   in
     unparse_t (term_to_ast (is_some o Syntax.lookup_const syn))
       (Printer.pretty_term_ast (not (Pure_Thy.old_appl_syntax thy)))
diff -r 40f5ddeda2b4 -r 951c371c1cd9 src/Pure/sign.ML
--- a/src/Pure/sign.ML	Tue Apr 02 17:20:09 2024 +0200
+++ b/src/Pure/sign.ML	Tue Apr 02 18:29:14 2024 +0200
@@ -11,7 +11,7 @@
   val change_end: theory -> theory
   val change_end_local: Proof.context -> Proof.context
   val change_check: theory -> theory
-  val syn_of: theory -> Syntax.syntax
+  val syntax_of: theory -> Syntax.syntax
   val tsig_of: theory -> Type.tsig
   val classes_of: theory -> Sorts.algebra
   val all_classes: theory -> class list
@@ -176,7 +176,7 @@
 
 (* syntax *)
 
-val syn_of = #syn o rep_sg;
+val syntax_of = #syn o rep_sg;
 
 
 (* type signature *)
diff -r 40f5ddeda2b4 -r 951c371c1cd9 src/Pure/theory.ML
--- a/src/Pure/theory.ML	Tue Apr 02 17:20:09 2024 +0200
+++ b/src/Pure/theory.ML	Tue Apr 02 18:29:14 2024 +0200
@@ -201,7 +201,7 @@
       |> Sign.init_naming
       |> Sign.local_path
       |> apply_wrappers wrappers
-      |> tap (Syntax.cache_syntax o Sign.syn_of)
+      |> tap (Syntax.cache_syntax o Sign.syntax_of)
     end;
 
 fun end_theory thy =