src/Pure/Isar/local_syntax.ML
changeset 35412 b8dead547d9e
parent 33387 acea2f336721
child 35429 afa8cf9e63d8
     1.1 --- a/src/Pure/Isar/local_syntax.ML	Mon Mar 01 09:47:44 2010 +0100
     1.2 +++ b/src/Pure/Isar/local_syntax.ML	Mon Mar 01 17:07:36 2010 +0100
     1.3 @@ -13,11 +13,12 @@
     1.4    val structs_of: T -> string list
     1.5    val init: theory -> T
     1.6    val rebuild: theory -> T -> T
     1.7 -  val add_syntax: theory -> (bool * (string * typ * mixfix)) list -> T -> T
     1.8 +  datatype kind = Type | Const | Fixed
     1.9 +  val add_syntax: theory -> (kind * (string * typ * mixfix)) list -> T -> T
    1.10    val set_mode: Syntax.mode -> T -> T
    1.11    val restore_mode: T -> T -> T
    1.12    val update_modesyntax: theory -> bool -> Syntax.mode ->
    1.13 -    (bool * (string * typ * mixfix)) list -> T -> T
    1.14 +    (kind * (string * typ * mixfix)) list -> T -> T
    1.15    val extern_term: T -> term -> term
    1.16  end;
    1.17  
    1.18 @@ -27,8 +28,8 @@
    1.19  (* datatype T *)
    1.20  
    1.21  type local_mixfix =
    1.22 -  (string * bool) *                                    (*name, fixed?*)
    1.23 -  ((bool * Syntax.mode) * (string * typ * mixfix));    (*add?, mode, declaration*)
    1.24 +  (string * bool) *  (*name, fixed?*)
    1.25 +  ((bool * bool * Syntax.mode) * (string * typ * mixfix));  (*type?, add?, mode, declaration*)
    1.26  
    1.27  datatype T = Syntax of
    1.28   {thy_syntax: Syntax.syntax,
    1.29 @@ -57,15 +58,16 @@
    1.30  fun build_syntax thy mode mixfixes (idents as (structs, _)) =
    1.31    let
    1.32      val thy_syntax = Sign.syn_of thy;
    1.33 -    val is_logtype = Sign.is_logtype thy;
    1.34 -    fun const_gram ((true, m), decls) = Syntax.update_const_gram is_logtype m decls
    1.35 -      | const_gram ((false, m), decls) = Syntax.remove_const_gram is_logtype m decls;
    1.36 +    fun update_gram ((true, add, m), decls) = Syntax.update_type_gram add m decls
    1.37 +      | update_gram ((false, add, m), decls) =
    1.38 +          Syntax.update_const_gram add (Sign.is_logtype thy) m decls;
    1.39 +
    1.40      val (atrs, trs, trs', atrs') = Syntax.struct_trfuns structs;
    1.41      val local_syntax = thy_syntax
    1.42        |> Syntax.update_trfuns
    1.43            (map Syntax.mk_trfun atrs, map Syntax.mk_trfun trs,
    1.44             map Syntax.mk_trfun trs', map Syntax.mk_trfun atrs')
    1.45 -      |> fold const_gram (AList.coalesce (op =) (rev (map snd mixfixes)));
    1.46 +      |> fold update_gram (AList.coalesce (op =) (rev (map snd mixfixes)));
    1.47    in make_syntax (thy_syntax, local_syntax, mode, mixfixes, idents) end;
    1.48  
    1.49  fun init thy = build_syntax thy Syntax.mode_default [] ([], []);
    1.50 @@ -77,16 +79,18 @@
    1.51  
    1.52  (* mixfix declarations *)
    1.53  
    1.54 +datatype kind = Type | Const | Fixed;
    1.55 +
    1.56  local
    1.57  
    1.58 -fun prep_mixfix _ (_, (_, _, Structure)) = NONE
    1.59 -  | prep_mixfix mode (fixed, (x, T, mx)) =
    1.60 -      let val c = if fixed then Syntax.fixedN ^ x else x
    1.61 -      in SOME ((x, fixed), (mode, (c, T, mx))) end;
    1.62 +fun prep_mixfix _ _ (_, (_, _, Structure)) = NONE
    1.63 +  | prep_mixfix add mode (Type, decl as (x, _, _)) = SOME ((x, false), ((true, add, mode), decl))
    1.64 +  | prep_mixfix add mode (Const, decl as (x, _, _)) = SOME ((x, false), ((false, add, mode), decl))
    1.65 +  | prep_mixfix add mode (Fixed, (x, T, mx)) =
    1.66 +      SOME ((x, true), ((false, add, mode), (Syntax.mark_fixed x, T, mx)));
    1.67  
    1.68 -fun prep_struct (fixed, (c, _, Structure)) =
    1.69 -      if fixed then SOME c
    1.70 -      else error ("Bad mixfix declaration for constant: " ^ quote c)
    1.71 +fun prep_struct (Fixed, (c, _, Structure)) = SOME c
    1.72 +  | prep_struct (_, (c, _, Structure)) = error ("Bad mixfix declaration for " ^ quote c)
    1.73    | prep_struct _ = NONE;
    1.74  
    1.75  in
    1.76 @@ -97,7 +101,7 @@
    1.77      [] => syntax
    1.78    | decls =>
    1.79        let
    1.80 -        val new_mixfixes = map_filter (prep_mixfix (add, mode)) decls;
    1.81 +        val new_mixfixes = map_filter (prep_mixfix add mode) decls;
    1.82          val new_structs = map_filter prep_struct decls;
    1.83          val mixfixes' = rev new_mixfixes @ mixfixes;
    1.84          val structs' =
    1.85 @@ -130,7 +134,7 @@
    1.86      fun map_free (t as Free (x, T)) =
    1.87            let val i = find_index (fn s => s = x) structs + 1 in
    1.88              if i = 0 andalso member (op =) fixes x then
    1.89 -              Const (Syntax.fixedN ^ x, T)
    1.90 +              Term.Const (Syntax.mark_fixed x, T)
    1.91              else if i = 1 andalso not (! show_structs) then
    1.92                Syntax.const "_struct" $ Syntax.const "_indexdefault"
    1.93              else t