--- a/src/Pure/IsaMakefile Tue Apr 05 15:15:33 2011 +0200
+++ b/src/Pure/IsaMakefile Tue Apr 05 15:46:35 2011 +0200
@@ -121,7 +121,6 @@
Isar/isar_syn.ML \
Isar/keyword.ML \
Isar/local_defs.ML \
- Isar/local_syntax.ML \
Isar/local_theory.ML \
Isar/locale.ML \
Isar/method.ML \
@@ -180,6 +179,7 @@
ROOT.ML \
Syntax/ast.ML \
Syntax/lexicon.ML \
+ Syntax/local_syntax.ML \
Syntax/mixfix.ML \
Syntax/parser.ML \
Syntax/printer.ML \
--- a/src/Pure/Isar/local_syntax.ML Tue Apr 05 15:15:33 2011 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,124 +0,0 @@
-(* Title: Pure/Isar/local_syntax.ML
- Author: Makarius
-
-Local syntax depending on theory syntax.
-*)
-
-signature LOCAL_SYNTAX =
-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 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
-end;
-
-structure Local_Syntax: LOCAL_SYNTAX =
-struct
-
-(* datatype T *)
-
-type local_mixfix =
- (string * bool) * (*name, fixed?*)
- ((bool * bool * Syntax.mode) * (string * typ * mixfix)); (*type?, add?, mode, declaration*)
-
-datatype T = Syntax of
- {thy_syntax: Syntax.syntax,
- local_syntax: Syntax.syntax,
- mode: Syntax.mode,
- mixfixes: local_mixfix list,
- idents: string list * string 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 map_syntax f (Syntax {thy_syntax, local_syntax, mode, mixfixes, idents}) =
- make_syntax (f (thy_syntax, local_syntax, mode, mixfixes, idents));
-
-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, _)) =
- let
- val thy_syntax = Sign.syn_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.is_logtype thy) m decls;
-
- val (atrs, trs, trs', atrs') = Syntax.struct_trfuns structs;
- val local_syntax = thy_syntax
- |> Syntax.update_trfuns
- (map Syntax.mk_trfun atrs, map Syntax.mk_trfun trs,
- map Syntax.mk_trfun trs', map Syntax.mk_trfun atrs')
- |> fold update_gram (AList.coalesce (op =) (rev (map snd mixfixes)));
- in make_syntax (thy_syntax, local_syntax, mode, mixfixes, idents) end;
-
-fun init thy = build_syntax thy Syntax.mode_default [] ([], []);
-
-fun rebuild thy (syntax as Syntax {mode, mixfixes, idents, ...}) =
- if is_consistent thy syntax then syntax
- else build_syntax thy mode mixfixes idents;
-
-
-(* mixfix declarations *)
-
-datatype kind = Type | Const | Fixed;
-
-local
-
-fun prep_mixfix _ _ (_, (_, _, Structure)) = NONE
- | prep_mixfix add mode (Type, decl as (x, _, _)) = SOME ((x, false), ((true, add, mode), decl))
- | prep_mixfix add mode (Const, decl as (x, _, _)) = SOME ((x, false), ((false, add, mode), decl))
- | prep_mixfix add mode (Fixed, (x, T, mx)) =
- SOME ((x, true), ((false, add, mode), (Syntax.mark_fixed x, T, mx)));
-
-fun prep_struct (Fixed, (c, _, Structure)) = SOME c
- | prep_struct (_, (c, _, Structure)) = error ("Bad mixfix declaration for " ^ quote c)
- | prep_struct _ = NONE;
-
-in
-
-fun update_syntax add thy raw_decls
- (syntax as (Syntax {mode, mixfixes, idents = (structs, _), ...})) =
- (case filter_out (fn (_, (_, _, mx)) => mx = NoSyn) raw_decls of
- [] => 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;
-
-end;
-
-
-(* syntax mode *)
-
-fun set_mode mode = map_syntax (fn (thy_syntax, local_syntax, _, mixfixes, idents) =>
- (thy_syntax, local_syntax, mode, mixfixes, idents));
-
-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;
-
-end;
--- a/src/Pure/ROOT.ML Tue Apr 05 15:15:33 2011 +0200
+++ b/src/Pure/ROOT.ML Tue Apr 05 15:46:35 2011 +0200
@@ -170,7 +170,7 @@
use "Isar/object_logic.ML";
use "Isar/rule_cases.ML";
use "Isar/auto_bind.ML";
-use "Isar/local_syntax.ML";
+use "Syntax/local_syntax.ML";
use "type_infer.ML";
use "Isar/proof_context.ML";
use "Isar/local_defs.ML";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Syntax/local_syntax.ML Tue Apr 05 15:46:35 2011 +0200
@@ -0,0 +1,124 @@
+(* Title: Pure/Syntax/local_syntax.ML
+ Author: Makarius
+
+Local syntax depending on theory syntax.
+*)
+
+signature LOCAL_SYNTAX =
+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 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
+end;
+
+structure Local_Syntax: LOCAL_SYNTAX =
+struct
+
+(* datatype T *)
+
+type local_mixfix =
+ (string * bool) * (*name, fixed?*)
+ ((bool * bool * Syntax.mode) * (string * typ * mixfix)); (*type?, add?, mode, declaration*)
+
+datatype T = Syntax of
+ {thy_syntax: Syntax.syntax,
+ local_syntax: Syntax.syntax,
+ mode: Syntax.mode,
+ mixfixes: local_mixfix list,
+ idents: string list * string 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 map_syntax f (Syntax {thy_syntax, local_syntax, mode, mixfixes, idents}) =
+ make_syntax (f (thy_syntax, local_syntax, mode, mixfixes, idents));
+
+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, _)) =
+ let
+ val thy_syntax = Sign.syn_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.is_logtype thy) m decls;
+
+ val (atrs, trs, trs', atrs') = Syntax.struct_trfuns structs;
+ val local_syntax = thy_syntax
+ |> Syntax.update_trfuns
+ (map Syntax.mk_trfun atrs, map Syntax.mk_trfun trs,
+ map Syntax.mk_trfun trs', map Syntax.mk_trfun atrs')
+ |> fold update_gram (AList.coalesce (op =) (rev (map snd mixfixes)));
+ in make_syntax (thy_syntax, local_syntax, mode, mixfixes, idents) end;
+
+fun init thy = build_syntax thy Syntax.mode_default [] ([], []);
+
+fun rebuild thy (syntax as Syntax {mode, mixfixes, idents, ...}) =
+ if is_consistent thy syntax then syntax
+ else build_syntax thy mode mixfixes idents;
+
+
+(* mixfix declarations *)
+
+datatype kind = Type | Const | Fixed;
+
+local
+
+fun prep_mixfix _ _ (_, (_, _, Structure)) = NONE
+ | prep_mixfix add mode (Type, decl as (x, _, _)) = SOME ((x, false), ((true, add, mode), decl))
+ | prep_mixfix add mode (Const, decl as (x, _, _)) = SOME ((x, false), ((false, add, mode), decl))
+ | prep_mixfix add mode (Fixed, (x, T, mx)) =
+ SOME ((x, true), ((false, add, mode), (Syntax.mark_fixed x, T, mx)));
+
+fun prep_struct (Fixed, (c, _, Structure)) = SOME c
+ | prep_struct (_, (c, _, Structure)) = error ("Bad mixfix declaration for " ^ quote c)
+ | prep_struct _ = NONE;
+
+in
+
+fun update_syntax add thy raw_decls
+ (syntax as (Syntax {mode, mixfixes, idents = (structs, _), ...})) =
+ (case filter_out (fn (_, (_, _, mx)) => mx = NoSyn) raw_decls of
+ [] => 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;
+
+end;
+
+
+(* syntax mode *)
+
+fun set_mode mode = map_syntax (fn (thy_syntax, local_syntax, _, mixfixes, idents) =>
+ (thy_syntax, local_syntax, mode, mixfixes, idents));
+
+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;
+
+end;