moved global pretty/string_of functions from Sign to Syntax;
authorwenzelm
Sun May 18 15:04:46 2008 +0200 (2008-05-18)
changeset 26951030e4a818b39
parent 26950 80366b6eb94c
child 26952 df36f4c52ee8
moved global pretty/string_of functions from Sign to Syntax;
reordered signature;
src/Pure/Syntax/syntax.ML
     1.1 --- a/src/Pure/Syntax/syntax.ML	Sun May 18 15:04:45 2008 +0200
     1.2 +++ b/src/Pure/Syntax/syntax.ML	Sun May 18 15:04:46 2008 +0200
     1.3 @@ -23,16 +23,40 @@
     1.4    include SYN_TRANS1
     1.5    include MIXFIX1
     1.6    include PRINTER0
     1.7 -  datatype 'a trrule =
     1.8 -    ParseRule of 'a * 'a |
     1.9 -    PrintRule of 'a * 'a |
    1.10 -    ParsePrintRule of 'a * 'a
    1.11    type syntax
    1.12    val eq_syntax: syntax * syntax -> bool
    1.13    val is_keyword: syntax -> string -> bool
    1.14    type mode
    1.15    val mode_default: mode
    1.16    val mode_input: mode
    1.17 +  val merge_syntaxes: syntax -> syntax -> syntax
    1.18 +  val basic_syn: syntax
    1.19 +  val basic_nonterms: string list
    1.20 +  val print_gram: syntax -> unit
    1.21 +  val print_trans: syntax -> unit
    1.22 +  val print_syntax: syntax -> unit
    1.23 +  val guess_infix: syntax -> string -> mixfix option
    1.24 +  val ambiguity_is_error: bool ref
    1.25 +  val ambiguity_level: int ref
    1.26 +  val ambiguity_limit: int ref
    1.27 +  val read: Proof.context -> (string -> bool) -> syntax -> typ -> string -> term list
    1.28 +  val standard_parse_term: Pretty.pp -> (term -> string option) ->
    1.29 +    (((string * int) * sort) list -> string * int -> Term.sort) ->
    1.30 +    (string -> string option) -> (string -> string option) ->
    1.31 +    (typ -> typ) -> (sort -> sort) -> Proof.context ->
    1.32 +    (string -> bool) -> syntax -> typ -> string -> term
    1.33 +  val standard_parse_typ: Proof.context -> syntax ->
    1.34 +    ((indexname * sort) list -> indexname -> sort) -> (sort -> sort) -> string -> typ
    1.35 +  val standard_parse_sort: Proof.context -> syntax -> (sort -> sort) -> string -> sort
    1.36 +  datatype 'a trrule =
    1.37 +    ParseRule of 'a * 'a |
    1.38 +    PrintRule of 'a * 'a |
    1.39 +    ParsePrintRule of 'a * 'a
    1.40 +  val map_trrule: ('a -> 'b) -> 'a trrule -> 'b trrule
    1.41 +  val standard_unparse_term: (string -> xstring) ->
    1.42 +    Proof.context -> syntax -> bool -> term -> Pretty.T
    1.43 +  val standard_unparse_typ: Proof.context -> syntax -> typ -> Pretty.T
    1.44 +  val standard_unparse_sort: Proof.context -> syntax -> sort -> Pretty.T
    1.45    val update_type_gram: (string * int * mixfix) list -> syntax -> syntax
    1.46    val update_consts: string list -> syntax -> syntax
    1.47    val update_trfuns:
    1.48 @@ -57,29 +81,6 @@
    1.49      (string * string) trrule list -> syntax -> syntax
    1.50    val update_trrules_i: ast trrule list -> syntax -> syntax
    1.51    val remove_trrules_i: ast trrule list -> syntax -> syntax
    1.52 -  val map_trrule: ('a -> 'b) -> 'a trrule -> 'b trrule
    1.53 -  val merge_syntaxes: syntax -> syntax -> syntax
    1.54 -  val basic_syn: syntax
    1.55 -  val basic_nonterms: string list
    1.56 -  val print_gram: syntax -> unit
    1.57 -  val print_trans: syntax -> unit
    1.58 -  val print_syntax: syntax -> unit
    1.59 -  val read: Proof.context -> (string -> bool) -> syntax -> typ -> string -> term list
    1.60 -  val standard_parse_term: Pretty.pp -> (term -> string option) ->
    1.61 -    (((string * int) * sort) list -> string * int -> Term.sort) ->
    1.62 -    (string -> string option) -> (string -> string option) ->
    1.63 -    (typ -> typ) -> (sort -> sort) -> Proof.context ->
    1.64 -    (string -> bool) -> syntax -> typ -> string -> term
    1.65 -  val standard_parse_typ: Proof.context -> syntax ->
    1.66 -    ((indexname * sort) list -> indexname -> sort) -> (sort -> sort) -> string -> typ
    1.67 -  val standard_parse_sort: Proof.context -> syntax -> (sort -> sort) -> string -> sort
    1.68 -  val standard_unparse_term: (string -> xstring) ->
    1.69 -    Proof.context -> syntax -> bool -> term -> Pretty.T
    1.70 -  val standard_unparse_typ: Proof.context -> syntax -> typ -> Pretty.T
    1.71 -  val standard_unparse_sort: Proof.context -> syntax -> sort -> Pretty.T
    1.72 -  val ambiguity_is_error: bool ref
    1.73 -  val ambiguity_level: int ref
    1.74 -  val ambiguity_limit: int ref
    1.75    val parse_sort: Proof.context -> string -> sort
    1.76    val parse_typ: Proof.context -> string -> typ
    1.77    val parse_term: Proof.context -> string -> term
    1.78 @@ -142,8 +143,17 @@
    1.79    val string_of_sort: Proof.context -> sort -> string
    1.80    val string_of_classrel: Proof.context -> class list -> string
    1.81    val string_of_arity: Proof.context -> arity -> string
    1.82 -  val guess_infix: syntax -> string -> mixfix option
    1.83 +  val is_pretty_global: Proof.context -> bool
    1.84 +  val set_pretty_global: bool -> Proof.context -> Proof.context
    1.85 +  val init_pretty_global: theory -> Proof.context
    1.86 +  val pretty_term_global: theory -> term -> Pretty.T
    1.87 +  val pretty_typ_global: theory -> typ -> Pretty.T
    1.88 +  val pretty_sort_global: theory -> sort -> Pretty.T
    1.89 +  val string_of_term_global: theory -> term -> string
    1.90 +  val string_of_typ_global: theory -> typ -> string
    1.91 +  val string_of_sort_global: theory -> sort -> string
    1.92    val pp: Proof.context -> Pretty.pp
    1.93 +  val pp_global: theory -> Pretty.pp
    1.94  end;
    1.95  
    1.96  structure Syntax: SYNTAX =
    1.97 @@ -430,6 +440,17 @@
    1.98  end;
    1.99  
   1.100  
   1.101 +(* reconstructing infixes -- educated guessing *)
   1.102 +
   1.103 +fun guess_infix (Syntax ({gram, ...}, _)) c =
   1.104 +  (case Parser.guess_infix_lr gram c of
   1.105 +    SOME (s, l, r, j) => SOME
   1.106 +     (if l then Mixfix.InfixlName (s, j)
   1.107 +      else if r then Mixfix.InfixrName (s, j)
   1.108 +      else Mixfix.InfixName (s, j))
   1.109 +  | NONE => NONE);
   1.110 +
   1.111 +
   1.112  
   1.113  (** read **)
   1.114  
   1.115 @@ -815,19 +836,37 @@
   1.116  
   1.117  (* pretty = uncheck + unparse *)
   1.118  
   1.119 +fun pretty_term ctxt = singleton (uncheck_terms ctxt) #> unparse_term ctxt;
   1.120 +fun pretty_typ ctxt = singleton (uncheck_typs ctxt) #> unparse_typ ctxt;
   1.121  fun pretty_sort ctxt = uncheck_sort ctxt #> unparse_sort ctxt;
   1.122  fun pretty_classrel ctxt = uncheck_classrel ctxt #> unparse_classrel ctxt;
   1.123  fun pretty_arity ctxt = uncheck_arity ctxt #> unparse_arity ctxt;
   1.124 -fun pretty_typ ctxt = singleton (uncheck_typs ctxt) #> unparse_typ ctxt;
   1.125 -fun pretty_term ctxt = singleton (uncheck_terms ctxt) #> unparse_term ctxt;
   1.126  
   1.127 +val string_of_term = Pretty.string_of oo pretty_term;
   1.128 +val string_of_typ = Pretty.string_of oo pretty_typ;
   1.129  val string_of_sort = Pretty.string_of oo pretty_sort;
   1.130  val string_of_classrel = Pretty.string_of oo pretty_classrel;
   1.131  val string_of_arity = Pretty.string_of oo pretty_arity;
   1.132 -val string_of_typ = Pretty.string_of oo pretty_typ;
   1.133 -val string_of_term = Pretty.string_of oo pretty_term;
   1.134 +
   1.135 +
   1.136 +(* global pretty printing *)
   1.137 +
   1.138 +structure PrettyGlobal = ProofDataFun(type T = bool fun init _ = false);
   1.139 +val is_pretty_global = PrettyGlobal.get;
   1.140 +val set_pretty_global = PrettyGlobal.put;
   1.141 +val init_pretty_global = set_pretty_global true o ProofContext.init;
   1.142  
   1.143 -(*pp operations -- deferred evaluation*)
   1.144 +val pretty_term_global = pretty_term o init_pretty_global;
   1.145 +val pretty_typ_global = pretty_typ o init_pretty_global;
   1.146 +val pretty_sort_global = pretty_sort o init_pretty_global;
   1.147 +
   1.148 +val string_of_term_global = string_of_term o init_pretty_global;
   1.149 +val string_of_typ_global = string_of_typ o init_pretty_global;
   1.150 +val string_of_sort_global = string_of_sort o init_pretty_global;
   1.151 +
   1.152 +
   1.153 +(* pp operations -- deferred evaluation *)
   1.154 +
   1.155  fun pp ctxt = Pretty.pp
   1.156   (fn x => pretty_term ctxt x,
   1.157    fn x => pretty_typ ctxt x,
   1.158 @@ -835,14 +874,13 @@
   1.159    fn x => pretty_classrel ctxt x,
   1.160    fn x => pretty_arity ctxt x);
   1.161  
   1.162 -(*educated guess for reconstructing infixes*)
   1.163 -fun guess_infix (Syntax ({gram, ...}, _)) c =
   1.164 -  (case Parser.guess_infix_lr gram c of
   1.165 -    SOME (s, l, r, j) => SOME
   1.166 -     (if l then Mixfix.InfixlName (s, j)
   1.167 -      else if r then Mixfix.InfixrName (s, j)
   1.168 -      else Mixfix.InfixName (s, j))
   1.169 -  | NONE => NONE);
   1.170 +fun pp_global thy = Pretty.pp
   1.171 + (fn x => pretty_term_global thy x,
   1.172 +  fn x => pretty_typ_global thy x,
   1.173 +  fn x => pretty_sort_global thy x,
   1.174 +  fn x => pretty_classrel (init_pretty_global thy) x,
   1.175 +  fn x => pretty_arity (init_pretty_global thy) x);
   1.176 +
   1.177  
   1.178  (*export parts of internal Syntax structures*)
   1.179  open Lexicon SynExt Ast Parser TypeExt SynTrans Mixfix Printer;