48 |
48 |
49 fun pretty_locale ctxt (name, pos) = |
49 fun pretty_locale ctxt (name, pos) = |
50 let val thy = Proof_Context.theory_of ctxt |
50 let val thy = Proof_Context.theory_of ctxt |
51 in Pretty.str (Locale.extern thy (Locale.check thy (name, pos))) end; |
51 in Pretty.str (Locale.extern thy (Locale.check thy (name, pos))) end; |
52 |
52 |
|
53 fun pretty_bundle ctxt (name, pos) = |
|
54 Pretty.str (Bundle.extern ctxt (Bundle.check ctxt (name, pos))); |
|
55 |
53 fun pretty_class ctxt s = |
56 fun pretty_class ctxt s = |
54 Pretty.str (Proof_Context.extern_class ctxt (Proof_Context.read_class ctxt s)); |
57 Pretty.str (Proof_Context.extern_class ctxt (Proof_Context.read_class ctxt s)); |
55 |
58 |
56 fun pretty_type ctxt s = |
59 fun pretty_type ctxt s = |
57 let val Type (name, _) = Proof_Context.read_type_name {proper = true, strict = false} ctxt s |
60 let val Type (name, _) = Proof_Context.read_type_name {proper = true, strict = false} ctxt s |
76 basic_entity \<^binding>\<open>typeof\<close> (Term_Style.parse -- Args.term) pretty_term_typeof #> |
79 basic_entity \<^binding>\<open>typeof\<close> (Term_Style.parse -- Args.term) pretty_term_typeof #> |
77 basic_entity \<^binding>\<open>const\<close> (Args.const {proper = true, strict = false}) pretty_const #> |
80 basic_entity \<^binding>\<open>const\<close> (Args.const {proper = true, strict = false}) pretty_const #> |
78 basic_entity \<^binding>\<open>abbrev\<close> (Scan.lift Args.embedded_inner_syntax) pretty_abbrev #> |
81 basic_entity \<^binding>\<open>abbrev\<close> (Scan.lift Args.embedded_inner_syntax) pretty_abbrev #> |
79 basic_entity \<^binding>\<open>typ\<close> Args.typ_abbrev Syntax.pretty_typ #> |
82 basic_entity \<^binding>\<open>typ\<close> Args.typ_abbrev Syntax.pretty_typ #> |
80 basic_entity \<^binding>\<open>locale\<close> (Scan.lift Args.embedded_position) pretty_locale #> |
83 basic_entity \<^binding>\<open>locale\<close> (Scan.lift Args.embedded_position) pretty_locale #> |
|
84 basic_entity \<^binding>\<open>bundle\<close> (Scan.lift Args.embedded_position) pretty_bundle #> |
81 basic_entity \<^binding>\<open>class\<close> (Scan.lift Args.embedded_inner_syntax) pretty_class #> |
85 basic_entity \<^binding>\<open>class\<close> (Scan.lift Args.embedded_inner_syntax) pretty_class #> |
82 basic_entity \<^binding>\<open>type\<close> (Scan.lift Args.embedded_inner_syntax) pretty_type #> |
86 basic_entity \<^binding>\<open>type\<close> (Scan.lift Args.embedded_inner_syntax) pretty_type #> |
83 basic_entity \<^binding>\<open>theory\<close> (Scan.lift Args.embedded_position) pretty_theory #> |
87 basic_entity \<^binding>\<open>theory\<close> (Scan.lift Args.embedded_position) pretty_theory #> |
84 basic_entities \<^binding>\<open>prf\<close> Attrib.thms (pretty_prf false) #> |
88 basic_entities \<^binding>\<open>prf\<close> Attrib.thms (pretty_prf false) #> |
85 basic_entities \<^binding>\<open>full_prf\<close> Attrib.thms (pretty_prf true) #> |
89 basic_entities \<^binding>\<open>full_prf\<close> Attrib.thms (pretty_prf true) #> |