1.1 --- a/src/Pure/IsaMakefile Tue Apr 05 15:15:33 2011 +0200
1.2 +++ b/src/Pure/IsaMakefile Tue Apr 05 15:46:35 2011 +0200
1.3 @@ -121,7 +121,6 @@
1.4 Isar/isar_syn.ML \
1.5 Isar/keyword.ML \
1.6 Isar/local_defs.ML \
1.7 - Isar/local_syntax.ML \
1.8 Isar/local_theory.ML \
1.9 Isar/locale.ML \
1.10 Isar/method.ML \
1.11 @@ -180,6 +179,7 @@
1.12 ROOT.ML \
1.13 Syntax/ast.ML \
1.14 Syntax/lexicon.ML \
1.15 + Syntax/local_syntax.ML \
1.16 Syntax/mixfix.ML \
1.17 Syntax/parser.ML \
1.18 Syntax/printer.ML \
2.1 --- a/src/Pure/Isar/local_syntax.ML Tue Apr 05 15:15:33 2011 +0200
2.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
2.3 @@ -1,124 +0,0 @@
2.4 -(* Title: Pure/Isar/local_syntax.ML
2.5 - Author: Makarius
2.6 -
2.7 -Local syntax depending on theory syntax.
2.8 -*)
2.9 -
2.10 -signature LOCAL_SYNTAX =
2.11 -sig
2.12 - type T
2.13 - val syn_of: T -> Syntax.syntax
2.14 - val idents_of: T -> {structs: string list, fixes: string list}
2.15 - val init: theory -> T
2.16 - val rebuild: theory -> T -> T
2.17 - datatype kind = Type | Const | Fixed
2.18 - val add_syntax: theory -> (kind * (string * typ * mixfix)) list -> T -> T
2.19 - val set_mode: Syntax.mode -> T -> T
2.20 - val restore_mode: T -> T -> T
2.21 - val update_modesyntax: theory -> bool -> Syntax.mode ->
2.22 - (kind * (string * typ * mixfix)) list -> T -> T
2.23 -end;
2.24 -
2.25 -structure Local_Syntax: LOCAL_SYNTAX =
2.26 -struct
2.27 -
2.28 -(* datatype T *)
2.29 -
2.30 -type local_mixfix =
2.31 - (string * bool) * (*name, fixed?*)
2.32 - ((bool * bool * Syntax.mode) * (string * typ * mixfix)); (*type?, add?, mode, declaration*)
2.33 -
2.34 -datatype T = Syntax of
2.35 - {thy_syntax: Syntax.syntax,
2.36 - local_syntax: Syntax.syntax,
2.37 - mode: Syntax.mode,
2.38 - mixfixes: local_mixfix list,
2.39 - idents: string list * string list};
2.40 -
2.41 -fun make_syntax (thy_syntax, local_syntax, mode, mixfixes, idents) =
2.42 - Syntax {thy_syntax = thy_syntax, local_syntax = local_syntax,
2.43 - mode = mode, mixfixes = mixfixes, idents = idents};
2.44 -
2.45 -fun map_syntax f (Syntax {thy_syntax, local_syntax, mode, mixfixes, idents}) =
2.46 - make_syntax (f (thy_syntax, local_syntax, mode, mixfixes, idents));
2.47 -
2.48 -fun is_consistent thy (Syntax {thy_syntax, ...}) =
2.49 - Syntax.eq_syntax (Sign.syn_of thy, thy_syntax);
2.50 -
2.51 -fun syn_of (Syntax {local_syntax, ...}) = local_syntax;
2.52 -fun idents_of (Syntax {idents = (structs, fixes), ...}) = {structs = structs, fixes = fixes};
2.53 -
2.54 -
2.55 -(* build syntax *)
2.56 -
2.57 -fun build_syntax thy mode mixfixes (idents as (structs, _)) =
2.58 - let
2.59 - val thy_syntax = Sign.syn_of thy;
2.60 - fun update_gram ((true, add, m), decls) = Syntax.update_type_gram add m decls
2.61 - | update_gram ((false, add, m), decls) =
2.62 - Syntax.update_const_gram add (Sign.is_logtype thy) m decls;
2.63 -
2.64 - val (atrs, trs, trs', atrs') = Syntax.struct_trfuns structs;
2.65 - val local_syntax = thy_syntax
2.66 - |> Syntax.update_trfuns
2.67 - (map Syntax.mk_trfun atrs, map Syntax.mk_trfun trs,
2.68 - map Syntax.mk_trfun trs', map Syntax.mk_trfun atrs')
2.69 - |> fold update_gram (AList.coalesce (op =) (rev (map snd mixfixes)));
2.70 - in make_syntax (thy_syntax, local_syntax, mode, mixfixes, idents) end;
2.71 -
2.72 -fun init thy = build_syntax thy Syntax.mode_default [] ([], []);
2.73 -
2.74 -fun rebuild thy (syntax as Syntax {mode, mixfixes, idents, ...}) =
2.75 - if is_consistent thy syntax then syntax
2.76 - else build_syntax thy mode mixfixes idents;
2.77 -
2.78 -
2.79 -(* mixfix declarations *)
2.80 -
2.81 -datatype kind = Type | Const | Fixed;
2.82 -
2.83 -local
2.84 -
2.85 -fun prep_mixfix _ _ (_, (_, _, Structure)) = NONE
2.86 - | prep_mixfix add mode (Type, decl as (x, _, _)) = SOME ((x, false), ((true, add, mode), decl))
2.87 - | prep_mixfix add mode (Const, decl as (x, _, _)) = SOME ((x, false), ((false, add, mode), decl))
2.88 - | prep_mixfix add mode (Fixed, (x, T, mx)) =
2.89 - SOME ((x, true), ((false, add, mode), (Syntax.mark_fixed x, T, mx)));
2.90 -
2.91 -fun prep_struct (Fixed, (c, _, Structure)) = SOME c
2.92 - | prep_struct (_, (c, _, Structure)) = error ("Bad mixfix declaration for " ^ quote c)
2.93 - | prep_struct _ = NONE;
2.94 -
2.95 -in
2.96 -
2.97 -fun update_syntax add thy raw_decls
2.98 - (syntax as (Syntax {mode, mixfixes, idents = (structs, _), ...})) =
2.99 - (case filter_out (fn (_, (_, _, mx)) => mx = NoSyn) raw_decls of
2.100 - [] => syntax
2.101 - | decls =>
2.102 - let
2.103 - val new_mixfixes = map_filter (prep_mixfix add mode) decls;
2.104 - val new_structs = map_filter prep_struct decls;
2.105 - val mixfixes' = rev new_mixfixes @ mixfixes;
2.106 - val structs' =
2.107 - if add then structs @ new_structs
2.108 - else subtract (op =) new_structs structs;
2.109 - val fixes' = fold (fn ((x, true), _) => cons x | _ => I) mixfixes' [];
2.110 - in build_syntax thy mode mixfixes' (structs', fixes') end);
2.111 -
2.112 -val add_syntax = update_syntax true;
2.113 -
2.114 -end;
2.115 -
2.116 -
2.117 -(* syntax mode *)
2.118 -
2.119 -fun set_mode mode = map_syntax (fn (thy_syntax, local_syntax, _, mixfixes, idents) =>
2.120 - (thy_syntax, local_syntax, mode, mixfixes, idents));
2.121 -
2.122 -fun restore_mode (Syntax {mode, ...}) = set_mode mode;
2.123 -
2.124 -fun update_modesyntax thy add mode args syntax =
2.125 - syntax |> set_mode mode |> update_syntax add thy args |> restore_mode syntax;
2.126 -
2.127 -end;
3.1 --- a/src/Pure/ROOT.ML Tue Apr 05 15:15:33 2011 +0200
3.2 +++ b/src/Pure/ROOT.ML Tue Apr 05 15:46:35 2011 +0200
3.3 @@ -170,7 +170,7 @@
3.4 use "Isar/object_logic.ML";
3.5 use "Isar/rule_cases.ML";
3.6 use "Isar/auto_bind.ML";
3.7 -use "Isar/local_syntax.ML";
3.8 +use "Syntax/local_syntax.ML";
3.9 use "type_infer.ML";
3.10 use "Isar/proof_context.ML";
3.11 use "Isar/local_defs.ML";
4.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
4.2 +++ b/src/Pure/Syntax/local_syntax.ML Tue Apr 05 15:46:35 2011 +0200
4.3 @@ -0,0 +1,124 @@
4.4 +(* Title: Pure/Syntax/local_syntax.ML
4.5 + Author: Makarius
4.6 +
4.7 +Local syntax depending on theory syntax.
4.8 +*)
4.9 +
4.10 +signature LOCAL_SYNTAX =
4.11 +sig
4.12 + type T
4.13 + val syn_of: T -> Syntax.syntax
4.14 + val idents_of: T -> {structs: string list, fixes: string list}
4.15 + val init: theory -> T
4.16 + val rebuild: theory -> T -> T
4.17 + datatype kind = Type | Const | Fixed
4.18 + val add_syntax: theory -> (kind * (string * typ * mixfix)) list -> T -> T
4.19 + val set_mode: Syntax.mode -> T -> T
4.20 + val restore_mode: T -> T -> T
4.21 + val update_modesyntax: theory -> bool -> Syntax.mode ->
4.22 + (kind * (string * typ * mixfix)) list -> T -> T
4.23 +end;
4.24 +
4.25 +structure Local_Syntax: LOCAL_SYNTAX =
4.26 +struct
4.27 +
4.28 +(* datatype T *)
4.29 +
4.30 +type local_mixfix =
4.31 + (string * bool) * (*name, fixed?*)
4.32 + ((bool * bool * Syntax.mode) * (string * typ * mixfix)); (*type?, add?, mode, declaration*)
4.33 +
4.34 +datatype T = Syntax of
4.35 + {thy_syntax: Syntax.syntax,
4.36 + local_syntax: Syntax.syntax,
4.37 + mode: Syntax.mode,
4.38 + mixfixes: local_mixfix list,
4.39 + idents: string list * string list};
4.40 +
4.41 +fun make_syntax (thy_syntax, local_syntax, mode, mixfixes, idents) =
4.42 + Syntax {thy_syntax = thy_syntax, local_syntax = local_syntax,
4.43 + mode = mode, mixfixes = mixfixes, idents = idents};
4.44 +
4.45 +fun map_syntax f (Syntax {thy_syntax, local_syntax, mode, mixfixes, idents}) =
4.46 + make_syntax (f (thy_syntax, local_syntax, mode, mixfixes, idents));
4.47 +
4.48 +fun is_consistent thy (Syntax {thy_syntax, ...}) =
4.49 + Syntax.eq_syntax (Sign.syn_of thy, thy_syntax);
4.50 +
4.51 +fun syn_of (Syntax {local_syntax, ...}) = local_syntax;
4.52 +fun idents_of (Syntax {idents = (structs, fixes), ...}) = {structs = structs, fixes = fixes};
4.53 +
4.54 +
4.55 +(* build syntax *)
4.56 +
4.57 +fun build_syntax thy mode mixfixes (idents as (structs, _)) =
4.58 + let
4.59 + val thy_syntax = Sign.syn_of thy;
4.60 + fun update_gram ((true, add, m), decls) = Syntax.update_type_gram add m decls
4.61 + | update_gram ((false, add, m), decls) =
4.62 + Syntax.update_const_gram add (Sign.is_logtype thy) m decls;
4.63 +
4.64 + val (atrs, trs, trs', atrs') = Syntax.struct_trfuns structs;
4.65 + val local_syntax = thy_syntax
4.66 + |> Syntax.update_trfuns
4.67 + (map Syntax.mk_trfun atrs, map Syntax.mk_trfun trs,
4.68 + map Syntax.mk_trfun trs', map Syntax.mk_trfun atrs')
4.69 + |> fold update_gram (AList.coalesce (op =) (rev (map snd mixfixes)));
4.70 + in make_syntax (thy_syntax, local_syntax, mode, mixfixes, idents) end;
4.71 +
4.72 +fun init thy = build_syntax thy Syntax.mode_default [] ([], []);
4.73 +
4.74 +fun rebuild thy (syntax as Syntax {mode, mixfixes, idents, ...}) =
4.75 + if is_consistent thy syntax then syntax
4.76 + else build_syntax thy mode mixfixes idents;
4.77 +
4.78 +
4.79 +(* mixfix declarations *)
4.80 +
4.81 +datatype kind = Type | Const | Fixed;
4.82 +
4.83 +local
4.84 +
4.85 +fun prep_mixfix _ _ (_, (_, _, Structure)) = NONE
4.86 + | prep_mixfix add mode (Type, decl as (x, _, _)) = SOME ((x, false), ((true, add, mode), decl))
4.87 + | prep_mixfix add mode (Const, decl as (x, _, _)) = SOME ((x, false), ((false, add, mode), decl))
4.88 + | prep_mixfix add mode (Fixed, (x, T, mx)) =
4.89 + SOME ((x, true), ((false, add, mode), (Syntax.mark_fixed x, T, mx)));
4.90 +
4.91 +fun prep_struct (Fixed, (c, _, Structure)) = SOME c
4.92 + | prep_struct (_, (c, _, Structure)) = error ("Bad mixfix declaration for " ^ quote c)
4.93 + | prep_struct _ = NONE;
4.94 +
4.95 +in
4.96 +
4.97 +fun update_syntax add thy raw_decls
4.98 + (syntax as (Syntax {mode, mixfixes, idents = (structs, _), ...})) =
4.99 + (case filter_out (fn (_, (_, _, mx)) => mx = NoSyn) raw_decls of
4.100 + [] => syntax
4.101 + | decls =>
4.102 + let
4.103 + val new_mixfixes = map_filter (prep_mixfix add mode) decls;
4.104 + val new_structs = map_filter prep_struct decls;
4.105 + val mixfixes' = rev new_mixfixes @ mixfixes;
4.106 + val structs' =
4.107 + if add then structs @ new_structs
4.108 + else subtract (op =) new_structs structs;
4.109 + val fixes' = fold (fn ((x, true), _) => cons x | _ => I) mixfixes' [];
4.110 + in build_syntax thy mode mixfixes' (structs', fixes') end);
4.111 +
4.112 +val add_syntax = update_syntax true;
4.113 +
4.114 +end;
4.115 +
4.116 +
4.117 +(* syntax mode *)
4.118 +
4.119 +fun set_mode mode = map_syntax (fn (thy_syntax, local_syntax, _, mixfixes, idents) =>
4.120 + (thy_syntax, local_syntax, mode, mixfixes, idents));
4.121 +
4.122 +fun restore_mode (Syntax {mode, ...}) = set_mode mode;
4.123 +
4.124 +fun update_modesyntax thy add mode args syntax =
4.125 + syntax |> set_mode mode |> update_syntax add thy args |> restore_mode syntax;
4.126 +
4.127 +end;