renamed Syntax.XXX_mode to Syntax.mode_XXX;
authorwenzelm
Thu Oct 11 16:05:53 2007 +0200 (2007-10-11)
changeset 24970050afeec89a7
parent 24969 b38527eefb3b
child 24971 4d006b03aa4a
renamed Syntax.XXX_mode to Syntax.mode_XXX;
moved ProofContext.pp to Syntax.pp;
src/Pure/Syntax/syntax.ML
     1.1 --- a/src/Pure/Syntax/syntax.ML	Thu Oct 11 16:05:47 2007 +0200
     1.2 +++ b/src/Pure/Syntax/syntax.ML	Thu Oct 11 16:05:53 2007 +0200
     1.3 @@ -39,8 +39,8 @@
     1.4    val eq_syntax: syntax * syntax -> bool
     1.5    val is_keyword: syntax -> string -> bool
     1.6    type mode
     1.7 -  val default_mode: mode
     1.8 -  val input_mode: mode
     1.9 +  val mode_default: mode
    1.10 +  val mode_input: mode
    1.11    val internalM: string
    1.12    val extend_type_gram: (string * int * mixfix) list -> syntax -> syntax
    1.13    val extend_const_gram: (string -> bool) ->
    1.14 @@ -148,6 +148,7 @@
    1.15    val string_of_sort: Proof.context -> sort -> string
    1.16    val string_of_classrel: Proof.context -> class list -> string
    1.17    val string_of_arity: Proof.context -> arity -> string
    1.18 +  val pp: Proof.context -> Pretty.pp
    1.19  end;
    1.20  
    1.21  structure Syntax: SYNTAX =
    1.22 @@ -252,8 +253,8 @@
    1.23  fun is_keyword (Syntax ({lexicon, ...}, _)) = Scan.is_literal lexicon o Symbol.explode;
    1.24  
    1.25  type mode = string * bool;
    1.26 -val default_mode = ("", true);
    1.27 -val input_mode = ("input", true);
    1.28 +val mode_default = ("", true);
    1.29 +val mode_input = ("input", true);
    1.30  val internalM = "internal";
    1.31  
    1.32  
    1.33 @@ -373,8 +374,8 @@
    1.34  
    1.35  val basic_syn =
    1.36    empty_syntax
    1.37 -  |> extend_syntax default_mode TypeExt.type_ext
    1.38 -  |> extend_syntax default_mode SynExt.pure_ext;
    1.39 +  |> extend_syntax mode_default TypeExt.type_ext
    1.40 +  |> extend_syntax mode_default SynExt.pure_ext;
    1.41  
    1.42  val basic_nonterms =
    1.43    (Lexicon.terminals @ [SynExt.logic, "type", "types", "sort", "classes",
    1.44 @@ -618,7 +619,7 @@
    1.45  (** modify syntax **)
    1.46  
    1.47  fun ext_syntax' f is_logtype prmode decls = extend_syntax prmode (f is_logtype decls);
    1.48 -fun ext_syntax f = ext_syntax' (K f) (K false) default_mode;
    1.49 +fun ext_syntax f = ext_syntax' (K f) (K false) mode_default;
    1.50  
    1.51  val extend_type_gram       = ext_syntax Mixfix.syn_ext_types;
    1.52  val extend_const_gram      = ext_syntax' Mixfix.syn_ext_consts;
    1.53 @@ -634,10 +635,10 @@
    1.54    ext_syntax SynExt.syn_ext_rules o read_rules ctxt is_logtype syn;
    1.55  
    1.56  fun remove_trrules ctxt is_logtype syn =
    1.57 -  remove_syntax default_mode o SynExt.syn_ext_rules o read_rules ctxt is_logtype syn;
    1.58 +  remove_syntax mode_default o SynExt.syn_ext_rules o read_rules ctxt is_logtype syn;
    1.59  
    1.60  val extend_trrules_i = ext_syntax SynExt.syn_ext_rules o cert_rules;
    1.61 -val remove_trrules_i = remove_syntax default_mode o SynExt.syn_ext_rules o cert_rules;
    1.62 +val remove_trrules_i = remove_syntax mode_default o SynExt.syn_ext_rules o cert_rules;
    1.63  
    1.64  
    1.65  
    1.66 @@ -820,6 +821,13 @@
    1.67  val string_of_typ = Pretty.string_of oo pretty_typ;
    1.68  val string_of_term = Pretty.string_of oo pretty_term;
    1.69  
    1.70 +(*pp operations -- deferred evaluation*)
    1.71 +fun pp ctxt = Pretty.pp
    1.72 + (fn x => pretty_term ctxt x,
    1.73 +  fn x => pretty_typ ctxt x,
    1.74 +  fn x => pretty_sort ctxt x,
    1.75 +  fn x => pretty_classrel ctxt x,
    1.76 +  fn x => pretty_arity ctxt x);
    1.77  
    1.78  (*export parts of internal Syntax structures*)
    1.79  open Lexicon SynExt Ast Parser TypeExt SynTrans Mixfix Printer;