--- 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;
--- 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 *)
--- 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, ...}) =
--- 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)))
--- 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 *)
--- 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 =