# HG changeset patch
# User wenzelm
# Date 1419006236 -3600
# Node ID 66e6c539a36dc6a96277425615efc38e96a14ab4
# Parent  a012574b78e7581316eb5677f2635f0a5fb930e1
more frugal Local_Syntax.init -- maintain idents within context;

diff -r a012574b78e7 -r 66e6c539a36d src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Fri Dec 19 12:56:06 2014 +0100
+++ b/src/Pure/Isar/proof_context.ML	Fri Dec 19 17:23:56 2014 +0100
@@ -22,7 +22,6 @@
   val restore_mode: Proof.context -> Proof.context -> Proof.context
   val abbrev_mode: Proof.context -> bool
   val set_stmt: bool -> Proof.context -> Proof.context
-  val syntax_of: Proof.context -> Local_Syntax.T
   val syn_of: Proof.context -> Syntax.syntax
   val tsig_of: Proof.context -> Type.tsig
   val set_defsort: sort -> Proof.context -> Proof.context
@@ -249,6 +248,16 @@
   map_data (fn (mode, syntax, tsig, consts, facts, cases) =>
     (mode, f syntax, tsig, consts, facts, cases));
 
+fun map_syntax_idents f ctxt =
+  let
+    val idents = Syntax_Trans.get_idents ctxt;
+    val (opt_idents', syntax') = f (#syntax (rep_data ctxt));
+  in
+    ctxt
+    |> map_syntax (K syntax')
+    |> (case opt_idents' of NONE => I | SOME idents' => Syntax_Trans.put_idents idents')
+  end;
+
 fun map_tsig f =
   map_data (fn (mode, syntax, tsig, consts, facts, cases) =>
     (mode, syntax, f tsig, consts, facts, cases));
@@ -1065,8 +1074,8 @@
   | const_syntax _ _ = NONE;
 
 fun gen_notation syntax add mode args ctxt =
-  ctxt |> map_syntax
-    (Local_Syntax.update_modesyntax (theory_of ctxt) add mode (map_filter (syntax ctxt) args));
+  ctxt |> map_syntax_idents
+    (Local_Syntax.update_modesyntax ctxt add mode (map_filter (syntax ctxt) args));
 
 in
 
@@ -1135,15 +1144,12 @@
 (* fixes *)
 
 fun add_fixes raw_vars ctxt =
-  let
-    val thy = theory_of ctxt;
-    val vars = #1 (cert_vars raw_vars ctxt);
-  in
+  let val vars = #1 (cert_vars raw_vars ctxt) in
     ctxt
     |> Variable.add_fixes_binding (map #1 vars)
     |-> (fn xs =>
       fold_map declare_var (map2 (fn x => fn (_, T, mx) => (x, T, mx)) xs vars)
-      #-> (map_syntax o Local_Syntax.add_syntax thy o map (pair Local_Syntax.Fixed))
+      #-> (map_syntax_idents o Local_Syntax.add_syntax ctxt o map (pair Local_Syntax.Fixed))
       #> pair xs)
   end;
 
@@ -1366,7 +1372,7 @@
       val prt_term = Syntax.pretty_term ctxt;
 
       (*structures*)
-      val {structs, ...} = Local_Syntax.idents_of (syntax_of ctxt);
+      val {structs, ...} = Syntax_Trans.get_idents ctxt;
       val prt_structs =
         if null structs then []
         else [Pretty.block (Pretty.str "structures:" :: Pretty.brk 1 ::
diff -r a012574b78e7 -r 66e6c539a36d src/Pure/Syntax/local_syntax.ML
--- a/src/Pure/Syntax/local_syntax.ML	Fri Dec 19 12:56:06 2014 +0100
+++ b/src/Pure/Syntax/local_syntax.ML	Fri Dec 19 17:23:56 2014 +0100
@@ -9,15 +9,16 @@
 sig
   type T
   val syn_of: T -> Syntax.syntax
-  val idents_of: T -> {structs: string list, fixes: string list}
   val init: theory -> T
   val rebuild: theory -> T -> T
   datatype kind = Type | Const | Fixed
-  val add_syntax: theory -> (kind * (string * typ * mixfix)) list -> T -> T
+  val add_syntax: Proof.context -> (kind * (string * typ * mixfix)) list ->
+    T -> {structs: string list, fixes: string list} option * T
   val set_mode: Syntax.mode -> T -> T
   val restore_mode: T -> T -> T
-  val update_modesyntax: theory -> bool -> Syntax.mode ->
-    (kind * (string * typ * mixfix)) list -> T -> T
+  val update_modesyntax: Proof.context -> bool -> Syntax.mode ->
+    (kind * (string * typ * mixfix)) list ->
+    T -> {structs: string list, fixes: string list} option * T
 end;
 
 structure Local_Syntax: LOCAL_SYNTAX =
@@ -33,26 +34,23 @@
  {thy_syntax: Syntax.syntax,
   local_syntax: Syntax.syntax,
   mode: Syntax.mode,
-  mixfixes: local_mixfix list,
-  idents: string list * string list};
+  mixfixes: local_mixfix list};
 
-fun make_syntax (thy_syntax, local_syntax, mode, mixfixes, idents) =
-  Syntax {thy_syntax = thy_syntax, local_syntax = local_syntax,
-    mode = mode, mixfixes = mixfixes, idents = idents};
+fun make_syntax (thy_syntax, local_syntax, mode, mixfixes) =
+  Syntax {thy_syntax = thy_syntax, local_syntax = local_syntax, mode = mode, mixfixes = mixfixes};
 
-fun map_syntax f (Syntax {thy_syntax, local_syntax, mode, mixfixes, idents}) =
-  make_syntax (f (thy_syntax, local_syntax, mode, mixfixes, idents));
+fun map_syntax f (Syntax {thy_syntax, local_syntax, mode, mixfixes}) =
+  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);
 
 fun syn_of (Syntax {local_syntax, ...}) = local_syntax;
-fun idents_of (Syntax {idents = (structs, fixes), ...}) = {structs = structs, fixes = fixes};
 
 
 (* build syntax *)
 
-fun build_syntax thy mode mixfixes (idents as (structs, _)) =
+fun build_syntax thy mode mixfixes =
   let
     val thy_syntax = Sign.syn_of thy;
     fun update_gram ((true, add, m), decls) = Syntax.update_type_gram add m decls
@@ -60,17 +58,16 @@
           Syntax.update_const_gram add (Sign.is_logtype thy) m decls;
 
     val local_syntax = thy_syntax
-      |> Syntax.update_trfuns
-          ([], [Syntax_Ext.mk_trfun (Syntax_Trans.struct_tr structs)],
-           [], [Syntax_Ext.mk_trfun (Syntax_Trans.struct_ast_tr' structs)])
       |> fold update_gram (AList.coalesce (op =) (rev (map snd mixfixes)));
-  in make_syntax (thy_syntax, local_syntax, mode, mixfixes, idents) end;
+  in make_syntax (thy_syntax, local_syntax, mode, mixfixes) end;
 
-fun init thy = build_syntax thy Syntax.mode_default [] ([], []);
+fun init thy =
+  let val thy_syntax = Sign.syn_of thy
+  in make_syntax (thy_syntax, thy_syntax, Syntax.mode_default, []) end;
 
-fun rebuild thy (syntax as Syntax {mode, mixfixes, idents, ...}) =
+fun rebuild thy (syntax as Syntax {mode, mixfixes, ...}) =
   if is_consistent thy syntax then syntax
-  else build_syntax thy mode mixfixes idents;
+  else build_syntax thy mode mixfixes;
 
 
 (* mixfix declarations *)
@@ -91,34 +88,38 @@
 
 in
 
-fun update_syntax add thy raw_decls
-    (syntax as (Syntax {mode, mixfixes, idents = (structs, _), ...})) =
+fun update_syntax ctxt add raw_decls (syntax as (Syntax {mode, mixfixes, ...})) =
   (case filter_out (fn (_, (_, _, mx)) => mx = NoSyn) raw_decls of
-    [] => syntax
+    [] => (NONE, syntax)
   | decls =>
       let
         val new_mixfixes = map_filter (prep_mixfix add mode) decls;
         val new_structs = map_filter prep_struct decls;
         val mixfixes' = rev new_mixfixes @ mixfixes;
-        val structs' =
-          if add then structs @ new_structs
-          else subtract (op =) new_structs structs;
-        val fixes' = fold (fn ((x, true), _) => cons x | _ => I) mixfixes' [];
-      in build_syntax thy mode mixfixes' (structs', fixes') end);
 
-val add_syntax = update_syntax true;
+        val idents = Syntax_Trans.get_idents ctxt;
+        val idents' =
+          {structs =
+            if add then #structs idents @ new_structs
+            else subtract (op =) new_structs (#structs idents),
+           fixes = fold (fn ((x, true), _) => cons x | _ => I) mixfixes' []};
+
+        val syntax' = build_syntax (Proof_Context.theory_of ctxt) mode mixfixes';
+      in (if idents = idents' then NONE else SOME idents', syntax') end);
+
+fun add_syntax ctxt = update_syntax ctxt true;
 
 end;
 
 
 (* syntax mode *)
 
-fun set_mode mode = map_syntax (fn (thy_syntax, local_syntax, _, mixfixes, idents) =>
-  (thy_syntax, local_syntax, mode, mixfixes, idents));
+fun set_mode mode = map_syntax (fn (thy_syntax, local_syntax, _, mixfixes) =>
+  (thy_syntax, local_syntax, mode, mixfixes));
 
 fun restore_mode (Syntax {mode, ...}) = set_mode mode;
 
-fun update_modesyntax thy add mode args syntax =
-  syntax |> set_mode mode |> update_syntax add thy args |> restore_mode syntax;
+fun update_modesyntax ctxt add mode args syntax =
+  syntax |> set_mode mode |> update_syntax ctxt add args ||> restore_mode syntax;
 
 end;
diff -r a012574b78e7 -r 66e6c539a36d src/Pure/Syntax/syntax_phases.ML
--- a/src/Pure/Syntax/syntax_phases.ML	Fri Dec 19 12:56:06 2014 +0100
+++ b/src/Pure/Syntax/syntax_phases.ML	Fri Dec 19 17:23:56 2014 +0100
@@ -599,8 +599,9 @@
           in (t1' $ t2', seen'') end;
   in #1 (prune (tm, [])) end;
 
-fun mark_atoms {structs, fixes} is_syntax_const ctxt tm =
+fun mark_atoms is_syntax_const ctxt tm =
   let
+    val {structs, fixes} = Syntax_Trans.get_idents ctxt;
     val show_structs = Config.get ctxt show_structs;
 
     fun mark ((t as Const (c, _)) $ u) =
@@ -627,7 +628,7 @@
 
 in
 
-fun term_to_ast idents is_syntax_const ctxt trf tm =
+fun term_to_ast is_syntax_const ctxt trf tm =
   let
     val show_types = Config.get ctxt show_types orelse Config.get ctxt show_sorts;
     val show_markup = Config.get ctxt show_markup;
@@ -670,7 +671,7 @@
     |> mark_aprop
     |> show_types ? prune_types ctxt
     |> Variable.revert_bounds ctxt
-    |> mark_atoms idents is_syntax_const ctxt
+    |> mark_atoms is_syntax_const ctxt
     |> ast_of
   end;
 
@@ -779,9 +780,8 @@
   let
     val thy = Proof_Context.theory_of ctxt;
     val syn = Proof_Context.syn_of ctxt;
-    val idents = Local_Syntax.idents_of (Proof_Context.syntax_of ctxt);
   in
-    unparse_t (term_to_ast idents (is_some o Syntax.lookup_const syn))
+    unparse_t (term_to_ast (is_some o Syntax.lookup_const syn))
       (Printer.pretty_term_ast (not (Pure_Thy.old_appl_syntax thy)))
       (Markup.language_term false) ctxt
   end;
diff -r a012574b78e7 -r 66e6c539a36d src/Pure/Syntax/syntax_trans.ML
--- a/src/Pure/Syntax/syntax_trans.ML	Fri Dec 19 12:56:06 2014 +0100
+++ b/src/Pure/Syntax/syntax_trans.ML	Fri Dec 19 17:23:56 2014 +0100
@@ -47,11 +47,11 @@
   val quote_antiquote_tr': string -> string -> string ->
     string * (Proof.context -> term list -> term)
   val update_name_tr': term -> term
+  val get_idents: Proof.context -> {structs: string list, fixes: string list}
+  val put_idents: {structs: string list, fixes: string list} -> Proof.context -> Proof.context
   val pure_parse_ast_translation: (string * (Proof.context -> Ast.ast list -> Ast.ast)) list
   val pure_parse_translation: (string * (Proof.context -> term list -> term)) list
   val pure_print_ast_translation: (string * (Proof.context -> Ast.ast list -> Ast.ast)) list
-  val struct_tr: string list -> string * (Proof.context -> term list -> term)
-  val struct_ast_tr': string list -> string * (Proof.context -> Ast.ast list -> Ast.ast)
 end;
 
 structure Syntax_Trans: SYNTAX_TRANS =
@@ -225,6 +225,15 @@
 
 (* indexed syntax *)
 
+structure Idents = Proof_Data
+(
+  type T = {structs: string list, fixes: string list};
+  fun init _ : T = {structs = [], fixes = []};
+);
+
+val get_idents = Idents.get;
+val put_idents = Idents.put;
+
 fun indexdefault_ast_tr [] =
       Ast.Appl [Ast.Constant "_index",
         Ast.Appl [Ast.Constant "_struct", Ast.Constant "_indexdefault"]]
@@ -239,13 +248,11 @@
 fun index_tr [t] = t
   | index_tr ts = raise TERM ("index_tr", ts);
 
-fun struct_tr structs =
-  ("_struct", fn _ =>
-    (fn [Const ("_indexdefault", _)] =>
-        (case structs of
-          x :: _ => Syntax.const (Lexicon.mark_fixed x)
-        | _ => error "Illegal reference to implicit structure")
-      | ts => raise TERM ("struct_tr", ts)));
+fun struct_tr ctxt [Const ("_indexdefault", _)] =
+      (case #structs (get_idents ctxt) of
+        x :: _ => Syntax.const (Lexicon.mark_fixed x)
+      | _ => error "Illegal reference to implicit structure")
+  | struct_tr _ ts = raise TERM ("struct_tr", ts);
 
 
 
@@ -457,13 +464,11 @@
 fun index_ast_tr' [Ast.Appl [Ast.Constant "_struct", ast]] = ast
   | index_ast_tr' _ = raise Match;
 
-fun struct_ast_tr' structs =
-  ("_struct", fn _ =>
-    (fn [Ast.Constant "_indexdefault"] =>
-        (case structs of
-          x :: _ => Ast.Appl [Ast.Constant "_free", Ast.Variable x]
-        | _ => raise Match)
-      | _ => raise Match));
+fun struct_ast_tr' ctxt [Ast.Constant "_indexdefault"] =
+      (case #structs (get_idents ctxt) of
+        x :: _ => Ast.Appl [Ast.Constant "_free", Ast.Variable x]
+      | _ => raise Match)
+  | struct_ast_tr' _ _ = raise Match;
 
 
 
@@ -492,7 +497,8 @@
   ("_TYPE", fn _ => type_tr),
   ("_DDDOT", fn _ => dddot_tr),
   ("_update_name", fn _ => update_name_tr),
-  ("_index", fn _ => index_tr)];
+  ("_index", fn _ => index_tr),
+  ("_struct", struct_tr)];
 
 val pure_print_ast_translation =
  [("\\<^type>fun", fn _ => fun_ast_tr'),
@@ -500,7 +506,8 @@
   ("_idts", fn _ => idtyp_ast_tr' "_idts"),
   ("_pttrns", fn _ => idtyp_ast_tr' "_pttrns"),
   ("\\<^const>Pure.imp", fn _ => impl_ast_tr'),
-  ("_index", fn _ => index_ast_tr')];
+  ("_index", fn _ => index_ast_tr'),
+  ("_struct", struct_ast_tr')];
 
 end;