src/Pure/display.ML
changeset 28290 4cc2b6046258
parent 28288 09c812966e7f
child 28316 b17d863a050f
equal deleted inserted replaced
28289:efd53393412b 28290:4cc2b6046258
   176 
   176 
   177     fun pretty_restrict (const, name) =
   177     fun pretty_restrict (const, name) =
   178       Pretty.block ([prt_const' const, Pretty.brk 2, Pretty.str ("(from " ^ quote name ^ ")")]);
   178       Pretty.block ([prt_const' const, Pretty.brk 2, Pretty.str ("(from " ^ quote name ^ ")")]);
   179 
   179 
   180     val axioms = (Theory.axiom_space thy, Theory.axiom_table thy);
   180     val axioms = (Theory.axiom_space thy, Theory.axiom_table thy);
   181     val oracles = (Theory.oracle_space thy, Theory.oracle_table thy);
       
   182     val defs = Theory.defs_of thy;
   181     val defs = Theory.defs_of thy;
   183     val {restricts, reducts} = Defs.dest defs;
   182     val {restricts, reducts} = Defs.dest defs;
   184     val {naming, syn = _, tsig, consts} = Sign.rep_sg thy;
   183     val {naming, syn = _, tsig, consts} = Sign.rep_sg thy;
   185     val {constants, constraints} = Consts.dest consts;
   184     val {constants, constraints} = Consts.dest consts;
   186     val extern_const = NameSpace.extern (#1 constants);
   185     val extern_const = NameSpace.extern (#1 constants);
   200     val log_cnsts = map_filter (fn (c, (ty, NONE)) => SOME (c, ty) | _ => NONE) cnsts;
   199     val log_cnsts = map_filter (fn (c, (ty, NONE)) => SOME (c, ty) | _ => NONE) cnsts;
   201     val abbrevs = map_filter (fn (c, (ty, SOME t)) => SOME (c, (ty, t)) | _ => NONE) cnsts;
   200     val abbrevs = map_filter (fn (c, (ty, SOME t)) => SOME (c, (ty, t)) | _ => NONE) cnsts;
   202     val cnstrs = NameSpace.extern_table constraints;
   201     val cnstrs = NameSpace.extern_table constraints;
   203 
   202 
   204     val axms = NameSpace.extern_table axioms;
   203     val axms = NameSpace.extern_table axioms;
   205     val oras = NameSpace.extern_table oracles;
       
   206 
   204 
   207     val (reds0, (reds1, reds2)) = filter_out (prune_const o fst o fst) reducts
   205     val (reds0, (reds1, reds2)) = filter_out (prune_const o fst o fst) reducts
   208       |> map (fn (lhs, rhs) =>
   206       |> map (fn (lhs, rhs) =>
   209         (apfst extern_const lhs, map (apfst extern_const) (filter_out (prune_const o fst) rhs)))
   207         (apfst extern_const lhs, map (apfst extern_const) (filter_out (prune_const o fst) rhs)))
   210       |> sort_wrt (#1 o #1)
   208       |> sort_wrt (#1 o #1)
   221       Pretty.big_list "type arities:" (pretty_arities arties),
   219       Pretty.big_list "type arities:" (pretty_arities arties),
   222       Pretty.big_list "logical consts:" (map (Pretty.block o prt_const) log_cnsts),
   220       Pretty.big_list "logical consts:" (map (Pretty.block o prt_const) log_cnsts),
   223       Pretty.big_list "abbreviations:" (map pretty_abbrev abbrevs),
   221       Pretty.big_list "abbreviations:" (map pretty_abbrev abbrevs),
   224       Pretty.big_list "constraints:" (map (Pretty.block o prt_const) cnstrs),
   222       Pretty.big_list "constraints:" (map (Pretty.block o prt_const) cnstrs),
   225       Pretty.big_list "axioms:" (map pretty_axm axms),
   223       Pretty.big_list "axioms:" (map pretty_axm axms),
   226       Pretty.strs ("oracles:" :: (map #1 oras)),
   224       Pretty.strs ("oracles:" :: Thm.extern_oracles thy),
   227       Pretty.big_list "definitions:"
   225       Pretty.big_list "definitions:"
   228         [pretty_finals reds0,
   226         [pretty_finals reds0,
   229          Pretty.big_list "non-overloaded:" (map pretty_reduct reds1),
   227          Pretty.big_list "non-overloaded:" (map pretty_reduct reds1),
   230          Pretty.big_list "overloaded:" (map pretty_reduct reds2),
   228          Pretty.big_list "overloaded:" (map pretty_reduct reds2),
   231          Pretty.big_list "pattern restrictions:" (map pretty_restrict rests)]]
   229          Pretty.big_list "pattern restrictions:" (map pretty_restrict rests)]]