src/Pure/Syntax/local_syntax.ML
author wenzelm
Sat, 25 May 2013 16:55:27 +0200
changeset 52144 9065615d0360
parent 52143 36ffe23b25f8
child 59152 66e6c539a36d
permissions -rw-r--r--
tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
42240
5a4d30cd47a7 moved Isar/local_syntax.ML to Syntax/local_syntax.ML;
wenzelm
parents: 35429
diff changeset
     1
(*  Title:      Pure/Syntax/local_syntax.ML
18997
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
     3
51655
28d6eb23522c tuned comment;
wenzelm
parents: 42290
diff changeset
     4
Local syntax depending on theory syntax, with special support for
28d6eb23522c tuned comment;
wenzelm
parents: 42290
diff changeset
     5
implicit structure references.
18997
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
     6
*)
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
     7
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
     8
signature LOCAL_SYNTAX =
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
     9
sig
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
    10
  type T
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
    11
  val syn_of: T -> Syntax.syntax
35429
afa8cf9e63d8 authentic syntax for classes and type constructors;
wenzelm
parents: 35412
diff changeset
    12
  val idents_of: T -> {structs: string list, fixes: string list}
18997
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
    13
  val init: theory -> T
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
    14
  val rebuild: theory -> T -> T
35412
b8dead547d9e more uniform treatment of syntax for types vs. consts;
wenzelm
parents: 33387
diff changeset
    15
  datatype kind = Type | Const | Fixed
b8dead547d9e more uniform treatment of syntax for types vs. consts;
wenzelm
parents: 33387
diff changeset
    16
  val add_syntax: theory -> (kind * (string * typ * mixfix)) list -> T -> T
20785
d60f81c56fd4 Syntax.mode;
wenzelm
parents: 19660
diff changeset
    17
  val set_mode: Syntax.mode -> T -> T
19541
1bb8e26a26ee maintain implicit syntax mode;
wenzelm
parents: 19482
diff changeset
    18
  val restore_mode: T -> T -> T
24951
834b8c2b9553 replaced add_modesyntax by general update_modesyntax (add or del);
wenzelm
parents: 20785
diff changeset
    19
  val update_modesyntax: theory -> bool -> Syntax.mode ->
35412
b8dead547d9e more uniform treatment of syntax for types vs. consts;
wenzelm
parents: 33387
diff changeset
    20
    (kind * (string * typ * mixfix)) list -> T -> T
18997
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
    21
end;
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
    22
33387
acea2f336721 modernized structure Local_Syntax;
wenzelm
parents: 32738
diff changeset
    23
structure Local_Syntax: LOCAL_SYNTAX =
18997
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
    24
struct
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
    25
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
    26
(* datatype T *)
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
    27
19386
38d83ffd6217 add_syntax: actually observe print mode;
wenzelm
parents: 19369
diff changeset
    28
type local_mixfix =
35412
b8dead547d9e more uniform treatment of syntax for types vs. consts;
wenzelm
parents: 33387
diff changeset
    29
  (string * bool) *  (*name, fixed?*)
b8dead547d9e more uniform treatment of syntax for types vs. consts;
wenzelm
parents: 33387
diff changeset
    30
  ((bool * bool * Syntax.mode) * (string * typ * mixfix));  (*type?, add?, mode, declaration*)
19386
38d83ffd6217 add_syntax: actually observe print mode;
wenzelm
parents: 19369
diff changeset
    31
18997
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
    32
datatype T = Syntax of
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
    33
 {thy_syntax: Syntax.syntax,
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
    34
  local_syntax: Syntax.syntax,
20785
d60f81c56fd4 Syntax.mode;
wenzelm
parents: 19660
diff changeset
    35
  mode: Syntax.mode,
19386
38d83ffd6217 add_syntax: actually observe print mode;
wenzelm
parents: 19369
diff changeset
    36
  mixfixes: local_mixfix list,
19369
a4374b41c9bf simplified handling of authentic syntax (cf. early externing in consts.ML);
wenzelm
parents: 19016
diff changeset
    37
  idents: string list * string list};
18997
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
    38
19541
1bb8e26a26ee maintain implicit syntax mode;
wenzelm
parents: 19482
diff changeset
    39
fun make_syntax (thy_syntax, local_syntax, mode, mixfixes, idents) =
18997
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
    40
  Syntax {thy_syntax = thy_syntax, local_syntax = local_syntax,
19541
1bb8e26a26ee maintain implicit syntax mode;
wenzelm
parents: 19482
diff changeset
    41
    mode = mode, mixfixes = mixfixes, idents = idents};
18997
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
    42
19541
1bb8e26a26ee maintain implicit syntax mode;
wenzelm
parents: 19482
diff changeset
    43
fun map_syntax f (Syntax {thy_syntax, local_syntax, mode, mixfixes, idents}) =
1bb8e26a26ee maintain implicit syntax mode;
wenzelm
parents: 19482
diff changeset
    44
  make_syntax (f (thy_syntax, local_syntax, mode, mixfixes, idents));
18997
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
    45
19369
a4374b41c9bf simplified handling of authentic syntax (cf. early externing in consts.ML);
wenzelm
parents: 19016
diff changeset
    46
fun is_consistent thy (Syntax {thy_syntax, ...}) =
18997
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
    47
  Syntax.eq_syntax (Sign.syn_of thy, thy_syntax);
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
    48
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
    49
fun syn_of (Syntax {local_syntax, ...}) = local_syntax;
35429
afa8cf9e63d8 authentic syntax for classes and type constructors;
wenzelm
parents: 35412
diff changeset
    50
fun idents_of (Syntax {idents = (structs, fixes), ...}) = {structs = structs, fixes = fixes};
18997
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
    51
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
    52
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
    53
(* build syntax *)
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
    54
19541
1bb8e26a26ee maintain implicit syntax mode;
wenzelm
parents: 19482
diff changeset
    55
fun build_syntax thy mode mixfixes (idents as (structs, _)) =
18997
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
    56
  let
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
    57
    val thy_syntax = Sign.syn_of thy;
35412
b8dead547d9e more uniform treatment of syntax for types vs. consts;
wenzelm
parents: 33387
diff changeset
    58
    fun update_gram ((true, add, m), decls) = Syntax.update_type_gram add m decls
b8dead547d9e more uniform treatment of syntax for types vs. consts;
wenzelm
parents: 33387
diff changeset
    59
      | update_gram ((false, add, m), decls) =
b8dead547d9e more uniform treatment of syntax for types vs. consts;
wenzelm
parents: 33387
diff changeset
    60
          Syntax.update_const_gram add (Sign.is_logtype thy) m decls;
b8dead547d9e more uniform treatment of syntax for types vs. consts;
wenzelm
parents: 33387
diff changeset
    61
18997
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
    62
    val local_syntax = thy_syntax
25390
8bfa6566ac6b syntax operations: turned extend'' into update'' (absorb duplicates);
wenzelm
parents: 25385
diff changeset
    63
      |> Syntax.update_trfuns
52144
wenzelm
parents: 52143
diff changeset
    64
          ([], [Syntax_Ext.mk_trfun (Syntax_Trans.struct_tr structs)],
wenzelm
parents: 52143
diff changeset
    65
           [], [Syntax_Ext.mk_trfun (Syntax_Trans.struct_ast_tr' structs)])
35412
b8dead547d9e more uniform treatment of syntax for types vs. consts;
wenzelm
parents: 33387
diff changeset
    66
      |> fold update_gram (AList.coalesce (op =) (rev (map snd mixfixes)));
19541
1bb8e26a26ee maintain implicit syntax mode;
wenzelm
parents: 19482
diff changeset
    67
  in make_syntax (thy_syntax, local_syntax, mode, mixfixes, idents) end;
1bb8e26a26ee maintain implicit syntax mode;
wenzelm
parents: 19482
diff changeset
    68
24960
39d1dd215d73 renamed Syntax.XXX_mode to Syntax.mode_XXX;
wenzelm
parents: 24954
diff changeset
    69
fun init thy = build_syntax thy Syntax.mode_default [] ([], []);
18997
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
    70
19541
1bb8e26a26ee maintain implicit syntax mode;
wenzelm
parents: 19482
diff changeset
    71
fun rebuild thy (syntax as Syntax {mode, mixfixes, idents, ...}) =
1bb8e26a26ee maintain implicit syntax mode;
wenzelm
parents: 19482
diff changeset
    72
  if is_consistent thy syntax then syntax
1bb8e26a26ee maintain implicit syntax mode;
wenzelm
parents: 19482
diff changeset
    73
  else build_syntax thy mode mixfixes idents;
18997
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
    74
19541
1bb8e26a26ee maintain implicit syntax mode;
wenzelm
parents: 19482
diff changeset
    75
18997
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
    76
(* mixfix declarations *)
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
    77
35412
b8dead547d9e more uniform treatment of syntax for types vs. consts;
wenzelm
parents: 33387
diff changeset
    78
datatype kind = Type | Const | Fixed;
b8dead547d9e more uniform treatment of syntax for types vs. consts;
wenzelm
parents: 33387
diff changeset
    79
18997
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
    80
local
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
    81
35412
b8dead547d9e more uniform treatment of syntax for types vs. consts;
wenzelm
parents: 33387
diff changeset
    82
fun prep_mixfix _ _ (_, (_, _, Structure)) = NONE
b8dead547d9e more uniform treatment of syntax for types vs. consts;
wenzelm
parents: 33387
diff changeset
    83
  | prep_mixfix add mode (Type, decl as (x, _, _)) = SOME ((x, false), ((true, add, mode), decl))
b8dead547d9e more uniform treatment of syntax for types vs. consts;
wenzelm
parents: 33387
diff changeset
    84
  | prep_mixfix add mode (Const, decl as (x, _, _)) = SOME ((x, false), ((false, add, mode), decl))
b8dead547d9e more uniform treatment of syntax for types vs. consts;
wenzelm
parents: 33387
diff changeset
    85
  | prep_mixfix add mode (Fixed, (x, T, mx)) =
42290
b1f544c84040 discontinued special treatment of structure Lexicon;
wenzelm
parents: 42288
diff changeset
    86
      SOME ((x, true), ((false, add, mode), (Lexicon.mark_fixed x, T, mx)));
19016
f26377a4605a tuned mixfixes, mixfix_conflict;
wenzelm
parents: 18997
diff changeset
    87
35412
b8dead547d9e more uniform treatment of syntax for types vs. consts;
wenzelm
parents: 33387
diff changeset
    88
fun prep_struct (Fixed, (c, _, Structure)) = SOME c
b8dead547d9e more uniform treatment of syntax for types vs. consts;
wenzelm
parents: 33387
diff changeset
    89
  | prep_struct (_, (c, _, Structure)) = error ("Bad mixfix declaration for " ^ quote c)
19016
f26377a4605a tuned mixfixes, mixfix_conflict;
wenzelm
parents: 18997
diff changeset
    90
  | prep_struct _ = NONE;
18997
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
    91
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
    92
in
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
    93
24951
834b8c2b9553 replaced add_modesyntax by general update_modesyntax (add or del);
wenzelm
parents: 20785
diff changeset
    94
fun update_syntax add thy raw_decls
834b8c2b9553 replaced add_modesyntax by general update_modesyntax (add or del);
wenzelm
parents: 20785
diff changeset
    95
    (syntax as (Syntax {mode, mixfixes, idents = (structs, _), ...})) =
834b8c2b9553 replaced add_modesyntax by general update_modesyntax (add or del);
wenzelm
parents: 20785
diff changeset
    96
  (case filter_out (fn (_, (_, _, mx)) => mx = NoSyn) raw_decls of
19016
f26377a4605a tuned mixfixes, mixfix_conflict;
wenzelm
parents: 18997
diff changeset
    97
    [] => syntax
f26377a4605a tuned mixfixes, mixfix_conflict;
wenzelm
parents: 18997
diff changeset
    98
  | decls =>
f26377a4605a tuned mixfixes, mixfix_conflict;
wenzelm
parents: 18997
diff changeset
    99
      let
35412
b8dead547d9e more uniform treatment of syntax for types vs. consts;
wenzelm
parents: 33387
diff changeset
   100
        val new_mixfixes = map_filter (prep_mixfix add mode) decls;
24954
0664f10a4094 update_modesyntax: may delete 'structure' notation as well;
wenzelm
parents: 24951
diff changeset
   101
        val new_structs = map_filter prep_struct decls;
0664f10a4094 update_modesyntax: may delete 'structure' notation as well;
wenzelm
parents: 24951
diff changeset
   102
        val mixfixes' = rev new_mixfixes @ mixfixes;
0664f10a4094 update_modesyntax: may delete 'structure' notation as well;
wenzelm
parents: 24951
diff changeset
   103
        val structs' =
0664f10a4094 update_modesyntax: may delete 'structure' notation as well;
wenzelm
parents: 24951
diff changeset
   104
          if add then structs @ new_structs
0664f10a4094 update_modesyntax: may delete 'structure' notation as well;
wenzelm
parents: 24951
diff changeset
   105
          else subtract (op =) new_structs structs;
20785
d60f81c56fd4 Syntax.mode;
wenzelm
parents: 19660
diff changeset
   106
        val fixes' = fold (fn ((x, true), _) => cons x | _ => I) mixfixes' [];
19541
1bb8e26a26ee maintain implicit syntax mode;
wenzelm
parents: 19482
diff changeset
   107
      in build_syntax thy mode mixfixes' (structs', fixes') end);
18997
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
   108
24951
834b8c2b9553 replaced add_modesyntax by general update_modesyntax (add or del);
wenzelm
parents: 20785
diff changeset
   109
val add_syntax = update_syntax true;
834b8c2b9553 replaced add_modesyntax by general update_modesyntax (add or del);
wenzelm
parents: 20785
diff changeset
   110
18997
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
   111
end;
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
   112
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
   113
19660
e3ec6839c631 added add_modesyntax;
wenzelm
parents: 19618
diff changeset
   114
(* syntax mode *)
e3ec6839c631 added add_modesyntax;
wenzelm
parents: 19618
diff changeset
   115
e3ec6839c631 added add_modesyntax;
wenzelm
parents: 19618
diff changeset
   116
fun set_mode mode = map_syntax (fn (thy_syntax, local_syntax, _, mixfixes, idents) =>
e3ec6839c631 added add_modesyntax;
wenzelm
parents: 19618
diff changeset
   117
  (thy_syntax, local_syntax, mode, mixfixes, idents));
e3ec6839c631 added add_modesyntax;
wenzelm
parents: 19618
diff changeset
   118
e3ec6839c631 added add_modesyntax;
wenzelm
parents: 19618
diff changeset
   119
fun restore_mode (Syntax {mode, ...}) = set_mode mode;
e3ec6839c631 added add_modesyntax;
wenzelm
parents: 19618
diff changeset
   120
24951
834b8c2b9553 replaced add_modesyntax by general update_modesyntax (add or del);
wenzelm
parents: 20785
diff changeset
   121
fun update_modesyntax thy add mode args syntax =
834b8c2b9553 replaced add_modesyntax by general update_modesyntax (add or del);
wenzelm
parents: 20785
diff changeset
   122
  syntax |> set_mode mode |> update_syntax add thy args |> restore_mode syntax;
19660
e3ec6839c631 added add_modesyntax;
wenzelm
parents: 19618
diff changeset
   123
18997
3229c88bbbdf Local syntax depending on theory syntax.
wenzelm
parents:
diff changeset
   124
end;