Syntax.mode;
authorwenzelm
Fri Sep 29 22:47:01 2006 +0200 (2006-09-29)
changeset 20784eece9aaaf352
parent 20783 17114542d2d4
child 20785 d60f81c56fd4
Syntax.mode;
src/Pure/Isar/local_theory.ML
src/Pure/Isar/proof_context.ML
src/Pure/Isar/specification.ML
src/Pure/Syntax/syntax.ML
src/Pure/sign.ML
     1.1 --- a/src/Pure/Isar/local_theory.ML	Fri Sep 29 22:46:59 2006 +0200
     1.2 +++ b/src/Pure/Isar/local_theory.ML	Fri Sep 29 22:47:01 2006 +0200
     1.3 @@ -25,8 +25,8 @@
     1.4    val naming: local_theory -> local_theory
     1.5    val mapping: xstring option -> (local_theory -> local_theory) -> theory -> local_theory * theory
     1.6    val term_syntax: (Context.generic -> Context.generic) -> local_theory -> local_theory
     1.7 -  val syntax: string * bool -> (string * mixfix) list -> local_theory -> local_theory
     1.8 -  val abbrevs: string * bool -> ((bstring * mixfix) * term) list -> local_theory -> local_theory
     1.9 +  val syntax: Syntax.mode -> (string * mixfix) list -> local_theory -> local_theory
    1.10 +  val abbrevs: Syntax.mode -> ((bstring * mixfix) * term) list -> local_theory -> local_theory
    1.11    val consts: ((bstring * typ) * mixfix) list -> local_theory -> term list * local_theory
    1.12    val consts_restricted: (string * typ -> bool) ->
    1.13      ((bstring * typ) * mixfix) list -> local_theory -> term list * local_theory
     2.1 --- a/src/Pure/Isar/proof_context.ML	Fri Sep 29 22:46:59 2006 +0200
     2.2 +++ b/src/Pure/Isar/proof_context.ML	Fri Sep 29 22:47:01 2006 +0200
     2.3 @@ -13,7 +13,7 @@
     2.4    val init: theory -> Proof.context
     2.5    val full_name: Proof.context -> bstring -> string
     2.6    val consts_of: Proof.context -> Consts.T
     2.7 -  val set_syntax_mode: string * bool -> Proof.context -> Proof.context
     2.8 +  val set_syntax_mode: Syntax.mode -> Proof.context -> Proof.context
     2.9    val restore_syntax_mode: Proof.context -> Proof.context -> Proof.context
    2.10    val fact_index_of: Proof.context -> FactIndex.T
    2.11    val transfer: theory -> Proof.context -> Proof.context
    2.12 @@ -137,8 +137,8 @@
    2.13    val apply_case: RuleCases.T -> Proof.context -> (string * term list) list * Proof.context
    2.14    val get_case: Proof.context -> string -> string option list -> RuleCases.T
    2.15    val expand_abbrevs: bool -> Proof.context -> Proof.context
    2.16 -  val add_const_syntax: string * bool -> (string * mixfix) list -> Proof.context -> Proof.context
    2.17 -  val add_abbrevs: string * bool -> ((bstring * mixfix) * term) list ->
    2.18 +  val add_const_syntax: Syntax.mode -> (string * mixfix) list -> Proof.context -> Proof.context
    2.19 +  val add_abbrevs: Syntax.mode -> ((bstring * mixfix) * term) list ->
    2.20      Proof.context -> Proof.context
    2.21    val verbose: bool ref
    2.22    val setmp_verbose: ('a -> 'b) -> 'a -> 'b
     3.1 --- a/src/Pure/Isar/specification.ML	Fri Sep 29 22:46:59 2006 +0200
     3.2 +++ b/src/Pure/Isar/specification.ML	Fri Sep 29 22:47:01 2006 +0200
     3.3 @@ -28,12 +28,12 @@
     3.4    val definition_i:
     3.5      ((string * typ option * mixfix) option * ((string * Attrib.src list) * term)) list ->
     3.6      local_theory -> (term * (bstring * thm)) list * local_theory
     3.7 -  val abbreviation: string * bool -> ((string * string option * mixfix) option * string) list ->
     3.8 +  val abbreviation: Syntax.mode -> ((string * string option * mixfix) option * string) list ->
     3.9      local_theory -> local_theory
    3.10 -  val abbreviation_i: string * bool -> ((string * typ option * mixfix) option * term) list ->
    3.11 +  val abbreviation_i: Syntax.mode -> ((string * typ option * mixfix) option * term) list ->
    3.12      local_theory -> local_theory
    3.13 -  val const_syntax: string * bool -> (xstring * mixfix) list -> local_theory -> local_theory
    3.14 -  val const_syntax_i: string * bool -> (string * mixfix) list -> local_theory -> local_theory
    3.15 +  val const_syntax: Syntax.mode -> (xstring * mixfix) list -> local_theory -> local_theory
    3.16 +  val const_syntax_i: Syntax.mode -> (string * mixfix) list -> local_theory -> local_theory
    3.17  end;
    3.18  
    3.19  structure Specification: SPECIFICATION =
     4.1 --- a/src/Pure/Syntax/syntax.ML	Fri Sep 29 22:46:59 2006 +0200
     4.2 +++ b/src/Pure/Syntax/syntax.ML	Fri Sep 29 22:47:01 2006 +0200
     4.3 @@ -37,10 +37,11 @@
     4.4    type syntax
     4.5    val eq_syntax: syntax * syntax -> bool
     4.6    val is_keyword: syntax -> string -> bool
     4.7 -  val default_mode: string * bool
     4.8 +  type mode
     4.9 +  val default_mode: mode
    4.10    val extend_type_gram: (string * int * mixfix) list -> syntax -> syntax
    4.11    val extend_const_gram: (string -> bool) ->
    4.12 -    string * bool -> (string * typ * mixfix) list -> syntax -> syntax
    4.13 +    mode -> (string * typ * mixfix) list -> syntax -> syntax
    4.14    val extend_consts: string list -> syntax -> syntax
    4.15    val extend_trfuns:
    4.16      (string * ((ast list -> ast) * stamp)) list *
    4.17 @@ -54,7 +55,7 @@
    4.18      (string * ((Context.generic -> ast list -> ast) * stamp)) list -> syntax -> syntax
    4.19    val extend_tokentrfuns: (string * string * (string -> string * real)) list -> syntax -> syntax
    4.20    val remove_const_gram: (string -> bool) ->
    4.21 -    string * bool -> (string * typ * mixfix) list -> syntax -> syntax
    4.22 +    mode -> (string * typ * mixfix) list -> syntax -> syntax
    4.23    val extend_trrules: Context.generic -> (string -> bool) -> syntax ->
    4.24      (string * string) trrule list -> syntax -> syntax
    4.25    val remove_trrules: Context.generic -> (string -> bool) -> syntax ->
    4.26 @@ -182,6 +183,7 @@
    4.27  
    4.28  fun is_keyword (Syntax ({lexicon, ...}, _)) = Scan.is_literal lexicon o Symbol.explode;
    4.29  
    4.30 +type mode = string * bool;
    4.31  val default_mode = ("", true);
    4.32  
    4.33  
     5.1 --- a/src/Pure/sign.ML	Fri Sep 29 22:46:59 2006 +0200
     5.2 +++ b/src/Pure/sign.ML	Fri Sep 29 22:47:01 2006 +0200
     5.3 @@ -17,10 +17,10 @@
     5.4    val add_tyabbrs_i: (bstring * string list * typ * mixfix) list -> theory -> theory
     5.5    val add_syntax: (bstring * string * mixfix) list -> theory -> theory
     5.6    val add_syntax_i: (bstring * typ * mixfix) list -> theory -> theory
     5.7 -  val add_modesyntax: (string * bool) -> (bstring * string * mixfix) list -> theory -> theory
     5.8 -  val add_modesyntax_i: (string * bool) -> (bstring * typ * mixfix) list -> theory -> theory
     5.9 -  val del_modesyntax: (string * bool) -> (bstring * string * mixfix) list -> theory -> theory
    5.10 -  val del_modesyntax_i: (string * bool) -> (bstring * typ * mixfix) list -> theory -> theory
    5.11 +  val add_modesyntax: Syntax.mode -> (bstring * string * mixfix) list -> theory -> theory
    5.12 +  val add_modesyntax_i: Syntax.mode -> (bstring * typ * mixfix) list -> theory -> theory
    5.13 +  val del_modesyntax: Syntax.mode -> (bstring * string * mixfix) list -> theory -> theory
    5.14 +  val del_modesyntax_i: Syntax.mode -> (bstring * typ * mixfix) list -> theory -> theory
    5.15    val add_consts: (bstring * string * mixfix) list -> theory -> theory
    5.16    val add_consts_i: (bstring * typ * mixfix) list -> theory -> theory
    5.17    val add_const_constraint: xstring * string option -> theory -> theory
    5.18 @@ -190,8 +190,8 @@
    5.19    val read_term: theory -> string -> term
    5.20    val read_prop: theory -> string -> term
    5.21    val add_consts_authentic: (bstring * typ * mixfix) list -> theory -> theory
    5.22 -  val add_const_syntax: string * bool -> (string * mixfix) list -> theory -> theory
    5.23 -  val add_abbrevs: string * bool -> ((bstring * mixfix) * term) list -> theory -> theory
    5.24 +  val add_const_syntax: Syntax.mode -> (string * mixfix) list -> theory -> theory
    5.25 +  val add_abbrevs: Syntax.mode -> ((bstring * mixfix) * term) list -> theory -> theory
    5.26    include SIGN_THEORY
    5.27  end
    5.28  
    5.29 @@ -696,11 +696,11 @@
    5.30  
    5.31  (* modify syntax *)
    5.32  
    5.33 -fun gen_syntax change_gram prep_typ prmode args thy =
    5.34 +fun gen_syntax change_gram prep_typ mode args thy =
    5.35    let
    5.36      fun prep (c, T, mx) = (c, prep_typ thy T, mx) handle ERROR msg =>
    5.37        cat_error msg ("in syntax declaration " ^ quote (Syntax.const_name c mx));
    5.38 -  in thy |> map_syn (change_gram (is_logtype thy) prmode (map prep args)) end;
    5.39 +  in thy |> map_syn (change_gram (is_logtype thy) mode (map prep args)) end;
    5.40  
    5.41  fun gen_add_syntax x = gen_syntax Syntax.extend_const_gram x;
    5.42  
    5.43 @@ -711,8 +711,8 @@
    5.44  val del_modesyntax = gen_syntax Syntax.remove_const_gram (read_typ_syntax o no_def_sort);
    5.45  val del_modesyntax_i = gen_syntax Syntax.remove_const_gram certify_typ_syntax;
    5.46  
    5.47 -fun add_const_syntax prmode args thy =
    5.48 -  thy |> add_modesyntax_i prmode (map (Consts.syntax (consts_of thy)) args);
    5.49 +fun add_const_syntax mode args thy =
    5.50 +  thy |> add_modesyntax_i mode (map (Consts.syntax (consts_of thy)) args);
    5.51  
    5.52  
    5.53  (* add constants *)