author  wenzelm 
Fri, 24 Aug 2012 12:35:39 +0200  
changeset 48918  6e5fd4585512 
parent 48881  46e053eda5dd 
child 49012  8686c36fa27d 
permissions  rwrr 
5831  1 
(* Title: Pure/Isar/isar_cmd.ML 
2 
Author: Markus Wenzel, TU Muenchen 

3 

30805  4 
Miscellaneous Isar commands. 
5831  5 
*) 
6 

7 
signature ISAR_CMD = 

8 
sig 

30575  9 
val global_setup: Symbol_Pos.text * Position.T > theory > theory 
10 
val local_setup: Symbol_Pos.text * Position.T > Proof.context > Proof.context 

11 
val parse_ast_translation: bool * (Symbol_Pos.text * Position.T) > theory > theory 

12 
val parse_translation: bool * (Symbol_Pos.text * Position.T) > theory > theory 

13 
val print_translation: bool * (Symbol_Pos.text * Position.T) > theory > theory 

14 
val typed_print_translation: bool * (Symbol_Pos.text * Position.T) > theory > theory 

15 
val print_ast_translation: bool * (Symbol_Pos.text * Position.T) > theory > theory 

42204  16 
val translations: (xstring * string) Syntax.trrule list > theory > theory 
17 
val no_translations: (xstring * string) Syntax.trrule list > theory > theory 

30573  18 
val oracle: bstring * Position.T > Symbol_Pos.text * Position.T > theory > theory 
35852
4e3fe0b8687b
minor renovation of oldstyle 'axioms'  make it an alias of iterated 'axiomatization';
wenzelm
parents:
35141
diff
changeset

19 
val add_axioms: (Attrib.binding * string) list > theory > theory 
29579  20 
val add_defs: (bool * bool) * ((binding * string) * Attrib.src list) list > theory > theory 
40784  21 
val declaration: {syntax: bool, pervasive: bool} > 
22 
Symbol_Pos.text * Position.T > local_theory > local_theory 

42464  23 
val simproc_setup: string * Position.T > string list > Symbol_Pos.text * Position.T > 
24 
string list > local_theory > local_theory 

36176
3fe7e97ccca8
replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact'  frees some popular keywords;
wenzelm
parents:
36174
diff
changeset

25 
val hide_class: bool > xstring list > theory > theory 
3fe7e97ccca8
replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact'  frees some popular keywords;
wenzelm
parents:
36174
diff
changeset

26 
val hide_type: bool > xstring list > theory > theory 
3fe7e97ccca8
replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact'  frees some popular keywords;
wenzelm
parents:
36174
diff
changeset

27 
val hide_const: bool > xstring list > theory > theory 
3fe7e97ccca8
replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact'  frees some popular keywords;
wenzelm
parents:
36174
diff
changeset

28 
val hide_fact: bool > xstring list > theory > theory 
28084
a05ca48ef263
type Attrib.binding abbreviates Name.binding without attributes;
wenzelm
parents:
28083
diff
changeset

29 
val have: (Attrib.binding * (string * string list) list) list > bool > Proof.state > Proof.state 
a05ca48ef263
type Attrib.binding abbreviates Name.binding without attributes;
wenzelm
parents:
28083
diff
changeset

30 
val hence: (Attrib.binding * (string * string list) list) list > bool > Proof.state > Proof.state 
a05ca48ef263
type Attrib.binding abbreviates Name.binding without attributes;
wenzelm
parents:
28083
diff
changeset

31 
val show: (Attrib.binding * (string * string list) list) list > bool > Proof.state > Proof.state 
a05ca48ef263
type Attrib.binding abbreviates Name.binding without attributes;
wenzelm
parents:
28083
diff
changeset

32 
val thus: (Attrib.binding * (string * string list) list) list > bool > Proof.state > Proof.state 
21350  33 
val qed: Method.text option > Toplevel.transition > Toplevel.transition 
34 
val terminal_proof: Method.text * Method.text option > 

35 
Toplevel.transition > Toplevel.transition 

36 
val default_proof: Toplevel.transition > Toplevel.transition 

37 
val immediate_proof: Toplevel.transition > Toplevel.transition 

38 
val done_proof: Toplevel.transition > Toplevel.transition 

39 
val skip_proof: Toplevel.transition > Toplevel.transition 

30575  40 
val ml_diag: bool > Symbol_Pos.text * Position.T > Toplevel.transition > Toplevel.transition 
48776
37cd53e69840
faster compilation of ML with antiquotations: static ML_context is bound once in auxiliary structure Isabelle;
wenzelm
parents:
47815
diff
changeset

41 
val diag_state: Proof.context > Toplevel.state 
37cd53e69840
faster compilation of ML with antiquotations: static ML_context is bound once in auxiliary structure Isabelle;
wenzelm
parents:
47815
diff
changeset

42 
val diag_goal: Proof.context > {context: Proof.context, facts: thm list, goal: thm} 
48881
46e053eda5dd
clarified Parse.path vs. Parse.explode  prefer errors in proper transaction context;
wenzelm
parents:
48792
diff
changeset

43 
val display_drafts: string list > Toplevel.transition > Toplevel.transition 
46e053eda5dd
clarified Parse.path vs. Parse.explode  prefer errors in proper transaction context;
wenzelm
parents:
48792
diff
changeset

44 
val print_drafts: string list > Toplevel.transition > Toplevel.transition 
7308  45 
val print_context: Toplevel.transition > Toplevel.transition 
20621  46 
val print_theory: bool > Toplevel.transition > Toplevel.transition 
5831  47 
val print_syntax: Toplevel.transition > Toplevel.transition 
21725  48 
val print_abbrevs: Toplevel.transition > Toplevel.transition 
21003
37492b0062c6
renamed print_lthms to print_facts, do not insist on proof state;
wenzelm
parents:
20978
diff
changeset

49 
val print_facts: Toplevel.transition > Toplevel.transition 
24115  50 
val print_configs: Toplevel.transition > Toplevel.transition 
33515
d066e8369a33
print_theorems: suppress concealed (global) facts, unless "!" option is given;
wenzelm
parents:
33456
diff
changeset

51 
val print_theorems: bool > Toplevel.transition > Toplevel.transition 
12060  52 
val print_locales: Toplevel.transition > Toplevel.transition 
46922
3717f3878714
source positions for locale and class expressions;
wenzelm
parents:
45666
diff
changeset

53 
val print_locale: bool * (xstring * Position.T) > Toplevel.transition > Toplevel.transition 
3717f3878714
source positions for locale and class expressions;
wenzelm
parents:
45666
diff
changeset

54 
val print_registrations: xstring * Position.T > Toplevel.transition > Toplevel.transition 
41435  55 
val print_dependencies: bool * Expression.expression > Toplevel.transition 
56 
> Toplevel.transition 

5831  57 
val print_attributes: Toplevel.transition > Toplevel.transition 
16026  58 
val print_simpset: Toplevel.transition > Toplevel.transition 
12382  59 
val print_rules: Toplevel.transition > Toplevel.transition 
9219  60 
val print_trans_rules: Toplevel.transition > Toplevel.transition 
5831  61 
val print_methods: Toplevel.transition > Toplevel.transition 
9219  62 
val print_antiquotations: Toplevel.transition > Toplevel.transition 
20574  63 
val class_deps: Toplevel.transition > Toplevel.transition 
22485  64 
val thy_deps: Toplevel.transition > Toplevel.transition 
26336
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26186
diff
changeset

65 
val thm_deps: (Facts.ref * Attrib.src list) list > Toplevel.transition > Toplevel.transition 
26184  66 
val unused_thms: (string list * string list option) option > 
67 
Toplevel.transition > Toplevel.transition 

5831  68 
val print_binds: Toplevel.transition > Toplevel.transition 
8369  69 
val print_cases: Toplevel.transition > Toplevel.transition 
26336
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26186
diff
changeset

70 
val print_stmts: string list * (Facts.ref * Attrib.src list) list 
19268  71 
> Toplevel.transition > Toplevel.transition 
26336
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26186
diff
changeset

72 
val print_thms: string list * (Facts.ref * Attrib.src list) list 
10581  73 
> Toplevel.transition > Toplevel.transition 
26336
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26186
diff
changeset

74 
val print_prfs: bool > string list * (Facts.ref * Attrib.src list) list option 
11524
197f2e14a714
Added functions for printing primitive proof terms.
berghofe
parents:
11017
diff
changeset

75 
> Toplevel.transition > Toplevel.transition 
12876
a70df1e5bf10
got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents:
12758
diff
changeset

76 
val print_prop: (string list * string) > Toplevel.transition > Toplevel.transition 
a70df1e5bf10
got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents:
12758
diff
changeset

77 
val print_term: (string list * string) > Toplevel.transition > Toplevel.transition 
48792  78 
val print_type: (string list * (string * string option)) > 
79 
Toplevel.transition > Toplevel.transition 

30573  80 
val header_markup: Symbol_Pos.text * Position.T > Toplevel.transition > Toplevel.transition 
45488
6d71d9e52369
pass positions for named targets, for formal links in the document model;
wenzelm
parents:
45291
diff
changeset

81 
val local_theory_markup: (xstring * Position.T) option * (Symbol_Pos.text * Position.T) > 
17262
63cf42df2723
add_chapter/section/subsection/subsubsection/text: optional locale specification;
wenzelm
parents:
17228
diff
changeset

82 
Toplevel.transition > Toplevel.transition 
30573  83 
val proof_markup: Symbol_Pos.text * Position.T > Toplevel.transition > Toplevel.transition 
5831  84 
end; 
85 

37216
3165bc303f66
modernized some structure names, keeping a few legacy aliases;
wenzelm
parents:
37198
diff
changeset

86 
structure Isar_Cmd: ISAR_CMD = 
5831  87 
struct 
88 

89 

22116
6917be2e647d
added various ML setup functions (from sign.ML, pure_thy.ML);
wenzelm
parents:
22087
diff
changeset

90 
(** theory declarations **) 
6917be2e647d
added various ML setup functions (from sign.ML, pure_thy.ML);
wenzelm
parents:
22087
diff
changeset

91 

30461  92 
(* generic setup *) 
22116
6917be2e647d
added various ML setup functions (from sign.ML, pure_thy.ML);
wenzelm
parents:
22087
diff
changeset

93 

30461  94 
fun global_setup (txt, pos) = 
37198
3af985b10550
replaced ML_Lex.read_antiq by more concise ML_Lex.read, which includes full read/report with explicit position information;
wenzelm
parents:
37146
diff
changeset

95 
ML_Lex.read pos txt 
3af985b10550
replaced ML_Lex.read_antiq by more concise ML_Lex.read, which includes full read/report with explicit position information;
wenzelm
parents:
37146
diff
changeset

96 
> ML_Context.expression pos "val setup: theory > theory" "Context.map_theory setup" 
26435  97 
> Context.theory_map; 
22116
6917be2e647d
added various ML setup functions (from sign.ML, pure_thy.ML);
wenzelm
parents:
22087
diff
changeset

98 

30461  99 
fun local_setup (txt, pos) = 
37198
3af985b10550
replaced ML_Lex.read_antiq by more concise ML_Lex.read, which includes full read/report with explicit position information;
wenzelm
parents:
37146
diff
changeset

100 
ML_Lex.read pos txt 
3af985b10550
replaced ML_Lex.read_antiq by more concise ML_Lex.read, which includes full read/report with explicit position information;
wenzelm
parents:
37146
diff
changeset

101 
> ML_Context.expression pos "val setup: local_theory > local_theory" "Context.map_proof setup" 
30461  102 
> Context.proof_map; 
103 

22116
6917be2e647d
added various ML setup functions (from sign.ML, pure_thy.ML);
wenzelm
parents:
22087
diff
changeset

104 

6917be2e647d
added various ML setup functions (from sign.ML, pure_thy.ML);
wenzelm
parents:
22087
diff
changeset

105 
(* translation functions *) 
6917be2e647d
added various ML setup functions (from sign.ML, pure_thy.ML);
wenzelm
parents:
22087
diff
changeset

106 

6917be2e647d
added various ML setup functions (from sign.ML, pure_thy.ML);
wenzelm
parents:
22087
diff
changeset

107 
local 
6917be2e647d
added various ML setup functions (from sign.ML, pure_thy.ML);
wenzelm
parents:
22087
diff
changeset

108 

6917be2e647d
added various ML setup functions (from sign.ML, pure_thy.ML);
wenzelm
parents:
22087
diff
changeset

109 
fun advancedT false = "" 
6917be2e647d
added various ML setup functions (from sign.ML, pure_thy.ML);
wenzelm
parents:
22087
diff
changeset

110 
 advancedT true = "Proof.context > "; 
6917be2e647d
added various ML setup functions (from sign.ML, pure_thy.ML);
wenzelm
parents:
22087
diff
changeset

111 

6917be2e647d
added various ML setup functions (from sign.ML, pure_thy.ML);
wenzelm
parents:
22087
diff
changeset

112 
fun advancedN false = "" 
6917be2e647d
added various ML setup functions (from sign.ML, pure_thy.ML);
wenzelm
parents:
22087
diff
changeset

113 
 advancedN true = "advanced_"; 
6917be2e647d
added various ML setup functions (from sign.ML, pure_thy.ML);
wenzelm
parents:
22087
diff
changeset

114 

6917be2e647d
added various ML setup functions (from sign.ML, pure_thy.ML);
wenzelm
parents:
22087
diff
changeset

115 
in 
6917be2e647d
added various ML setup functions (from sign.ML, pure_thy.ML);
wenzelm
parents:
22087
diff
changeset

116 

26385
ae7564661e76
ML runtime compilation: pass position, tuned signature;
wenzelm
parents:
26336
diff
changeset

117 
fun parse_ast_translation (a, (txt, pos)) = 
37198
3af985b10550
replaced ML_Lex.read_antiq by more concise ML_Lex.read, which includes full read/report with explicit position information;
wenzelm
parents:
37146
diff
changeset

118 
ML_Lex.read pos txt 
3af985b10550
replaced ML_Lex.read_antiq by more concise ML_Lex.read, which includes full read/report with explicit position information;
wenzelm
parents:
37146
diff
changeset

119 
> ML_Context.expression pos 
26455  120 
("val parse_ast_translation: (string * (" ^ advancedT a ^ 
42224
578a51fae383
discontinued special treatment of structure Ast: no pervasive content, no inclusion in structure Syntax;
wenzelm
parents:
42204
diff
changeset

121 
"Ast.ast list > Ast.ast)) list") 
22116
6917be2e647d
added various ML setup functions (from sign.ML, pure_thy.ML);
wenzelm
parents:
22087
diff
changeset

122 
("Context.map_theory (Sign.add_" ^ advancedN a ^ "trfuns (parse_ast_translation, [], [], []))") 
6917be2e647d
added various ML setup functions (from sign.ML, pure_thy.ML);
wenzelm
parents:
22087
diff
changeset

123 
> Context.theory_map; 
6917be2e647d
added various ML setup functions (from sign.ML, pure_thy.ML);
wenzelm
parents:
22087
diff
changeset

124 

26385
ae7564661e76
ML runtime compilation: pass position, tuned signature;
wenzelm
parents:
26336
diff
changeset

125 
fun parse_translation (a, (txt, pos)) = 
37198
3af985b10550
replaced ML_Lex.read_antiq by more concise ML_Lex.read, which includes full read/report with explicit position information;
wenzelm
parents:
37146
diff
changeset

126 
ML_Lex.read pos txt 
3af985b10550
replaced ML_Lex.read_antiq by more concise ML_Lex.read, which includes full read/report with explicit position information;
wenzelm
parents:
37146
diff
changeset

127 
> ML_Context.expression pos 
26455  128 
("val parse_translation: (string * (" ^ advancedT a ^ 
22116
6917be2e647d
added various ML setup functions (from sign.ML, pure_thy.ML);
wenzelm
parents:
22087
diff
changeset

129 
"term list > term)) list") 
6917be2e647d
added various ML setup functions (from sign.ML, pure_thy.ML);
wenzelm
parents:
22087
diff
changeset

130 
("Context.map_theory (Sign.add_" ^ advancedN a ^ "trfuns ([], parse_translation, [], []))") 
6917be2e647d
added various ML setup functions (from sign.ML, pure_thy.ML);
wenzelm
parents:
22087
diff
changeset

131 
> Context.theory_map; 
6917be2e647d
added various ML setup functions (from sign.ML, pure_thy.ML);
wenzelm
parents:
22087
diff
changeset

132 

26385
ae7564661e76
ML runtime compilation: pass position, tuned signature;
wenzelm
parents:
26336
diff
changeset

133 
fun print_translation (a, (txt, pos)) = 
37198
3af985b10550
replaced ML_Lex.read_antiq by more concise ML_Lex.read, which includes full read/report with explicit position information;
wenzelm
parents:
37146
diff
changeset

134 
ML_Lex.read pos txt 
3af985b10550
replaced ML_Lex.read_antiq by more concise ML_Lex.read, which includes full read/report with explicit position information;
wenzelm
parents:
37146
diff
changeset

135 
> ML_Context.expression pos 
26455  136 
("val print_translation: (string * (" ^ advancedT a ^ 
22116
6917be2e647d
added various ML setup functions (from sign.ML, pure_thy.ML);
wenzelm
parents:
22087
diff
changeset

137 
"term list > term)) list") 
6917be2e647d
added various ML setup functions (from sign.ML, pure_thy.ML);
wenzelm
parents:
22087
diff
changeset

138 
("Context.map_theory (Sign.add_" ^ advancedN a ^ "trfuns ([], [], print_translation, []))") 
6917be2e647d
added various ML setup functions (from sign.ML, pure_thy.ML);
wenzelm
parents:
22087
diff
changeset

139 
> Context.theory_map; 
6917be2e647d
added various ML setup functions (from sign.ML, pure_thy.ML);
wenzelm
parents:
22087
diff
changeset

140 

26385
ae7564661e76
ML runtime compilation: pass position, tuned signature;
wenzelm
parents:
26336
diff
changeset

141 
fun print_ast_translation (a, (txt, pos)) = 
37198
3af985b10550
replaced ML_Lex.read_antiq by more concise ML_Lex.read, which includes full read/report with explicit position information;
wenzelm
parents:
37146
diff
changeset

142 
ML_Lex.read pos txt 
3af985b10550
replaced ML_Lex.read_antiq by more concise ML_Lex.read, which includes full read/report with explicit position information;
wenzelm
parents:
37146
diff
changeset

143 
> ML_Context.expression pos 
26455  144 
("val print_ast_translation: (string * (" ^ advancedT a ^ 
42224
578a51fae383
discontinued special treatment of structure Ast: no pervasive content, no inclusion in structure Syntax;
wenzelm
parents:
42204
diff
changeset

145 
"Ast.ast list > Ast.ast)) list") 
22116
6917be2e647d
added various ML setup functions (from sign.ML, pure_thy.ML);
wenzelm
parents:
22087
diff
changeset

146 
("Context.map_theory (Sign.add_" ^ advancedN a ^ "trfuns ([], [], [], print_ast_translation))") 
6917be2e647d
added various ML setup functions (from sign.ML, pure_thy.ML);
wenzelm
parents:
22087
diff
changeset

147 
> Context.theory_map; 
6917be2e647d
added various ML setup functions (from sign.ML, pure_thy.ML);
wenzelm
parents:
22087
diff
changeset

148 

26385
ae7564661e76
ML runtime compilation: pass position, tuned signature;
wenzelm
parents:
26336
diff
changeset

149 
fun typed_print_translation (a, (txt, pos)) = 
37198
3af985b10550
replaced ML_Lex.read_antiq by more concise ML_Lex.read, which includes full read/report with explicit position information;
wenzelm
parents:
37146
diff
changeset

150 
ML_Lex.read pos txt 
3af985b10550
replaced ML_Lex.read_antiq by more concise ML_Lex.read, which includes full read/report with explicit position information;
wenzelm
parents:
37146
diff
changeset

151 
> ML_Context.expression pos 
42247
12fe41a92cd5
typed_print_translation: discontinued show_sorts argument;
wenzelm
parents:
42243
diff
changeset

152 
("val typed_print_translation: (string * (" ^ advancedT a ^ "typ > term list > term)) list") 
22116
6917be2e647d
added various ML setup functions (from sign.ML, pure_thy.ML);
wenzelm
parents:
22087
diff
changeset

153 
("Context.map_theory (Sign.add_" ^ advancedN a ^ "trfunsT typed_print_translation)") 
6917be2e647d
added various ML setup functions (from sign.ML, pure_thy.ML);
wenzelm
parents:
22087
diff
changeset

154 
> Context.theory_map; 
6917be2e647d
added various ML setup functions (from sign.ML, pure_thy.ML);
wenzelm
parents:
22087
diff
changeset

155 

6917be2e647d
added various ML setup functions (from sign.ML, pure_thy.ML);
wenzelm
parents:
22087
diff
changeset

156 
end; 
6917be2e647d
added various ML setup functions (from sign.ML, pure_thy.ML);
wenzelm
parents:
22087
diff
changeset

157 

6917be2e647d
added various ML setup functions (from sign.ML, pure_thy.ML);
wenzelm
parents:
22087
diff
changeset

158 

42204  159 
(* translation rules *) 
160 

161 
fun read_trrules thy raw_rules = 

162 
let 

42360  163 
val ctxt = Proof_Context.init_global thy; 
42204  164 
in 
165 
raw_rules > map (Syntax.map_trrule (fn (r, s) => 

42360  166 
Syntax_Phases.parse_ast_pattern ctxt (Proof_Context.intern_type ctxt r, s))) 
42204  167 
end; 
168 

169 
fun translations args thy = Sign.add_trrules (read_trrules thy args) thy; 

170 
fun no_translations args thy = Sign.del_trrules (read_trrules thy args) thy; 

171 

172 

22116
6917be2e647d
added various ML setup functions (from sign.ML, pure_thy.ML);
wenzelm
parents:
22087
diff
changeset

173 
(* oracles *) 
6917be2e647d
added various ML setup functions (from sign.ML, pure_thy.ML);
wenzelm
parents:
22087
diff
changeset

174 

30334  175 
fun oracle (name, pos) (body_txt, body_pos) = 
27871
4ef76f8788ad
oracle, header/local_theory/proof_markup: pass SymbolPos.text;
wenzelm
parents:
27853
diff
changeset

176 
let 
37198
3af985b10550
replaced ML_Lex.read_antiq by more concise ML_Lex.read, which includes full read/report with explicit position information;
wenzelm
parents:
37146
diff
changeset

177 
val body = ML_Lex.read body_pos body_txt; 
3af985b10550
replaced ML_Lex.read_antiq by more concise ML_Lex.read, which includes full read/report with explicit position information;
wenzelm
parents:
37146
diff
changeset

178 
val ants = 
3af985b10550
replaced ML_Lex.read_antiq by more concise ML_Lex.read, which includes full read/report with explicit position information;
wenzelm
parents:
37146
diff
changeset

179 
ML_Lex.read Position.none 
3af985b10550
replaced ML_Lex.read_antiq by more concise ML_Lex.read, which includes full read/report with explicit position information;
wenzelm
parents:
37146
diff
changeset

180 
("local\n\ 
3af985b10550
replaced ML_Lex.read_antiq by more concise ML_Lex.read, which includes full read/report with explicit position information;
wenzelm
parents:
37146
diff
changeset

181 
\ val binding = " ^ ML_Syntax.make_binding (name, pos) ^ ";\n\ 
3af985b10550
replaced ML_Lex.read_antiq by more concise ML_Lex.read, which includes full read/report with explicit position information;
wenzelm
parents:
37146
diff
changeset

182 
\ val body = ") @ body @ ML_Lex.read Position.none (";\n\ 
3af985b10550
replaced ML_Lex.read_antiq by more concise ML_Lex.read, which includes full read/report with explicit position information;
wenzelm
parents:
37146
diff
changeset

183 
\in\n\ 
3af985b10550
replaced ML_Lex.read_antiq by more concise ML_Lex.read, which includes full read/report with explicit position information;
wenzelm
parents:
37146
diff
changeset

184 
\ val " ^ name ^ " = snd (Context.>>> (Context.map_theory_result (Thm.add_oracle (binding, body))));\n\ 
3af985b10550
replaced ML_Lex.read_antiq by more concise ML_Lex.read, which includes full read/report with explicit position information;
wenzelm
parents:
37146
diff
changeset

185 
\end;\n"); 
3af985b10550
replaced ML_Lex.read_antiq by more concise ML_Lex.read, which includes full read/report with explicit position information;
wenzelm
parents:
37146
diff
changeset

186 
in Context.theory_map (ML_Context.exec (fn () => ML_Context.eval false body_pos ants)) end; 
22116
6917be2e647d
added various ML setup functions (from sign.ML, pure_thy.ML);
wenzelm
parents:
22087
diff
changeset

187 

6917be2e647d
added various ML setup functions (from sign.ML, pure_thy.ML);
wenzelm
parents:
22087
diff
changeset

188 

35852
4e3fe0b8687b
minor renovation of oldstyle 'axioms'  make it an alias of iterated 'axiomatization';
wenzelm
parents:
35141
diff
changeset

189 
(* oldstyle axioms *) 
21350  190 

35894  191 
val add_axioms = fold (snd oo Specification.axiom_cmd); 
21350  192 

35852
4e3fe0b8687b
minor renovation of oldstyle 'axioms'  make it an alias of iterated 'axiomatization';
wenzelm
parents:
35141
diff
changeset

193 
fun add_defs ((unchecked, overloaded), args) thy = 
39557
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is globalonly;
wenzelm
parents:
39507
diff
changeset

194 
thy > 
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is globalonly;
wenzelm
parents:
39507
diff
changeset

195 
(if unchecked then Global_Theory.add_defs_unchecked_cmd else Global_Theory.add_defs_cmd) 
47815  196 
overloaded 
197 
(map (fn ((b, ax), srcs) => ((b, ax), map (Attrib.attribute_cmd_global thy) srcs)) args) 

35852
4e3fe0b8687b
minor renovation of oldstyle 'axioms'  make it an alias of iterated 'axiomatization';
wenzelm
parents:
35141
diff
changeset

198 
> snd; 
21350  199 

200 

22087  201 
(* declarations *) 
202 

40784  203 
fun declaration {syntax, pervasive} (txt, pos) = 
37198
3af985b10550
replaced ML_Lex.read_antiq by more concise ML_Lex.read, which includes full read/report with explicit position information;
wenzelm
parents:
37146
diff
changeset

204 
ML_Lex.read pos txt 
3af985b10550
replaced ML_Lex.read_antiq by more concise ML_Lex.read, which includes full read/report with explicit position information;
wenzelm
parents:
37146
diff
changeset

205 
> ML_Context.expression pos 
26455  206 
"val declaration: Morphism.declaration" 
45291
57cd50f98fdc
uniform Local_Theory.declaration with explicit params;
wenzelm
parents:
44338
diff
changeset

207 
("Context.map_proof (Local_Theory.declaration {syntax = " ^ Bool.toString syntax ^ ", \ 
57cd50f98fdc
uniform Local_Theory.declaration with explicit params;
wenzelm
parents:
44338
diff
changeset

208 
\pervasive = " ^ Bool.toString pervasive ^ "} declaration)") 
26385
ae7564661e76
ML runtime compilation: pass position, tuned signature;
wenzelm
parents:
26336
diff
changeset

209 
> Context.proof_map; 
22087  210 

211 

22202  212 
(* simprocs *) 
213 

37198
3af985b10550
replaced ML_Lex.read_antiq by more concise ML_Lex.read, which includes full read/report with explicit position information;
wenzelm
parents:
37146
diff
changeset

214 
fun simproc_setup name lhss (txt, pos) identifier = 
3af985b10550
replaced ML_Lex.read_antiq by more concise ML_Lex.read, which includes full read/report with explicit position information;
wenzelm
parents:
37146
diff
changeset

215 
ML_Lex.read pos txt 
3af985b10550
replaced ML_Lex.read_antiq by more concise ML_Lex.read, which includes full read/report with explicit position information;
wenzelm
parents:
37146
diff
changeset

216 
> ML_Context.expression pos 
22239  217 
"val proc: Morphism.morphism > Simplifier.simpset > cterm > thm option" 
42464  218 
("Context.map_proof (Simplifier.def_simproc_cmd {name = " ^ ML_Syntax.make_binding name ^ ", \ 
37198
3af985b10550
replaced ML_Lex.read_antiq by more concise ML_Lex.read, which includes full read/report with explicit position information;
wenzelm
parents:
37146
diff
changeset

219 
\lhss = " ^ ML_Syntax.print_strings lhss ^ ", proc = proc, \ 
3af985b10550
replaced ML_Lex.read_antiq by more concise ML_Lex.read, which includes full read/report with explicit position information;
wenzelm
parents:
37146
diff
changeset

220 
\identifier = Library.maps ML_Context.thms " ^ ML_Syntax.print_strings identifier ^ "})") 
22202  221 
> Context.proof_map; 
222 

223 

26671
c95590e01df5
added hide_names command (formerly Sign.hide_names), support fact name space;
wenzelm
parents:
26626
diff
changeset

224 
(* hide names *) 
c95590e01df5
added hide_names command (formerly Sign.hide_names), support fact name space;
wenzelm
parents:
26626
diff
changeset

225 

36176
3fe7e97ccca8
replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact'  frees some popular keywords;
wenzelm
parents:
36174
diff
changeset

226 
fun hide_names intern check hide fully xnames thy = 
3fe7e97ccca8
replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact'  frees some popular keywords;
wenzelm
parents:
36174
diff
changeset

227 
let 
3fe7e97ccca8
replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact'  frees some popular keywords;
wenzelm
parents:
36174
diff
changeset

228 
val names = map (intern thy) xnames; 
3fe7e97ccca8
replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact'  frees some popular keywords;
wenzelm
parents:
36174
diff
changeset

229 
val bads = filter_out (check thy) names; 
3fe7e97ccca8
replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact'  frees some popular keywords;
wenzelm
parents:
36174
diff
changeset

230 
in 
3fe7e97ccca8
replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact'  frees some popular keywords;
wenzelm
parents:
36174
diff
changeset

231 
if null bads then fold (hide fully) names thy 
3fe7e97ccca8
replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact'  frees some popular keywords;
wenzelm
parents:
36174
diff
changeset

232 
else error ("Attempt to hide undeclared item(s): " ^ commas_quote bads) 
3fe7e97ccca8
replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact'  frees some popular keywords;
wenzelm
parents:
36174
diff
changeset

233 
end; 
26671
c95590e01df5
added hide_names command (formerly Sign.hide_names), support fact name space;
wenzelm
parents:
26626
diff
changeset

234 

36176
3fe7e97ccca8
replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact'  frees some popular keywords;
wenzelm
parents:
36174
diff
changeset

235 
val hide_class = hide_names Sign.intern_class (can o Sign.certify_class) Sign.hide_class; 
3fe7e97ccca8
replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact'  frees some popular keywords;
wenzelm
parents:
36174
diff
changeset

236 
val hide_type = hide_names Sign.intern_type Sign.declared_tyname Sign.hide_type; 
3fe7e97ccca8
replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact'  frees some popular keywords;
wenzelm
parents:
36174
diff
changeset

237 
val hide_const = hide_names Sign.intern_const Sign.declared_const Sign.hide_const; 
39557
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is globalonly;
wenzelm
parents:
39507
diff
changeset

238 
val hide_fact = 
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is globalonly;
wenzelm
parents:
39507
diff
changeset

239 
hide_names Global_Theory.intern_fact Global_Theory.defined_fact Global_Theory.hide_fact; 
26671
c95590e01df5
added hide_names command (formerly Sign.hide_names), support fact name space;
wenzelm
parents:
26626
diff
changeset

240 

c95590e01df5
added hide_names command (formerly Sign.hide_names), support fact name space;
wenzelm
parents:
26626
diff
changeset

241 

21350  242 
(* goals *) 
243 

244 
fun goal opt_chain goal stmt int = 

29383  245 
opt_chain #> goal NONE (K I) stmt int; 
21350  246 

36323
655e2d74de3a
modernized naming conventions of main Isar proof elements;
wenzelm
parents:
36178
diff
changeset

247 
val have = goal I Proof.have_cmd; 
655e2d74de3a
modernized naming conventions of main Isar proof elements;
wenzelm
parents:
36178
diff
changeset

248 
val hence = goal Proof.chain Proof.have_cmd; 
655e2d74de3a
modernized naming conventions of main Isar proof elements;
wenzelm
parents:
36178
diff
changeset

249 
val show = goal I Proof.show_cmd; 
655e2d74de3a
modernized naming conventions of main Isar proof elements;
wenzelm
parents:
36178
diff
changeset

250 
val thus = goal Proof.chain Proof.show_cmd; 
21350  251 

252 

253 
(* local endings *) 

254 

29383  255 
fun local_qed m = Toplevel.proof (Proof.local_qed (m, true)); 
32061
11f8ee55662d
parallel_proofs: more finegrained control with optional parallel checking of nested Isar proofs;
wenzelm
parents:
31819
diff
changeset

256 
val local_terminal_proof = Toplevel.proof' o Proof.local_future_terminal_proof; 
29383  257 
val local_default_proof = Toplevel.proof Proof.local_default_proof; 
258 
val local_immediate_proof = Toplevel.proof Proof.local_immediate_proof; 

259 
val local_done_proof = Toplevel.proof Proof.local_done_proof; 

260 
val local_skip_proof = Toplevel.proof' Proof.local_skip_proof; 

21350  261 

27562  262 
val skip_local_qed = Toplevel.skip_proof (fn i => if i > 1 then i  1 else raise Toplevel.UNDEF); 
21350  263 

264 

265 
(* global endings *) 

266 

267 
fun global_qed m = Toplevel.end_proof (K (Proof.global_qed (m, true))); 

268 
val global_terminal_proof = Toplevel.end_proof o K o Proof.global_terminal_proof; 

269 
val global_default_proof = Toplevel.end_proof (K Proof.global_default_proof); 

270 
val global_immediate_proof = Toplevel.end_proof (K Proof.global_immediate_proof); 

271 
val global_skip_proof = Toplevel.end_proof Proof.global_skip_proof; 

272 
val global_done_proof = Toplevel.end_proof (K Proof.global_done_proof); 

273 

28375  274 
val skip_global_qed = Toplevel.skip_proof_to_theory (fn n => n = 1); 
21350  275 

276 

277 
(* common endings *) 

278 

279 
fun qed m = local_qed m o global_qed m o skip_local_qed o skip_global_qed; 

280 
fun terminal_proof m = local_terminal_proof m o global_terminal_proof m; 

281 
val default_proof = local_default_proof o global_default_proof; 

282 
val immediate_proof = local_immediate_proof o global_immediate_proof; 

283 
val done_proof = local_done_proof o global_done_proof; 

284 
val skip_proof = local_skip_proof o global_skip_proof; 

285 

286 

26489  287 
(* diagnostic ML evaluation *) 
5831  288 

37305
9763792e4ac7
diagnostic commands 'ML_val' and 'ML_command' may refer to antiquotations @{Isar.state} and @{Isar.goal};
wenzelm
parents:
37216
diff
changeset

289 
structure Diag_State = Proof_Data 
9763792e4ac7
diagnostic commands 'ML_val' and 'ML_command' may refer to antiquotations @{Isar.state} and @{Isar.goal};
wenzelm
parents:
37216
diff
changeset

290 
( 
9763792e4ac7
diagnostic commands 'ML_val' and 'ML_command' may refer to antiquotations @{Isar.state} and @{Isar.goal};
wenzelm
parents:
37216
diff
changeset

291 
type T = Toplevel.state; 
9763792e4ac7
diagnostic commands 'ML_val' and 'ML_command' may refer to antiquotations @{Isar.state} and @{Isar.goal};
wenzelm
parents:
37216
diff
changeset

292 
fun init _ = Toplevel.toplevel; 
9763792e4ac7
diagnostic commands 'ML_val' and 'ML_command' may refer to antiquotations @{Isar.state} and @{Isar.goal};
wenzelm
parents:
37216
diff
changeset

293 
); 
9763792e4ac7
diagnostic commands 'ML_val' and 'ML_command' may refer to antiquotations @{Isar.state} and @{Isar.goal};
wenzelm
parents:
37216
diff
changeset

294 

26489  295 
fun ml_diag verbose (txt, pos) = Toplevel.keep (fn state => 
37305
9763792e4ac7
diagnostic commands 'ML_val' and 'ML_command' may refer to antiquotations @{Isar.state} and @{Isar.goal};
wenzelm
parents:
37216
diff
changeset

296 
let val opt_ctxt = 
9763792e4ac7
diagnostic commands 'ML_val' and 'ML_command' may refer to antiquotations @{Isar.state} and @{Isar.goal};
wenzelm
parents:
37216
diff
changeset

297 
try Toplevel.generic_theory_of state 
9763792e4ac7
diagnostic commands 'ML_val' and 'ML_command' may refer to antiquotations @{Isar.state} and @{Isar.goal};
wenzelm
parents:
37216
diff
changeset

298 
> Option.map (Context.proof_of #> Diag_State.put state) 
9763792e4ac7
diagnostic commands 'ML_val' and 'ML_command' may refer to antiquotations @{Isar.state} and @{Isar.goal};
wenzelm
parents:
37216
diff
changeset

299 
in ML_Context.eval_text_in opt_ctxt verbose pos txt end); 
9763792e4ac7
diagnostic commands 'ML_val' and 'ML_command' may refer to antiquotations @{Isar.state} and @{Isar.goal};
wenzelm
parents:
37216
diff
changeset

300 

48776
37cd53e69840
faster compilation of ML with antiquotations: static ML_context is bound once in auxiliary structure Isabelle;
wenzelm
parents:
47815
diff
changeset

301 
val diag_state = Diag_State.get; 
37305
9763792e4ac7
diagnostic commands 'ML_val' and 'ML_command' may refer to antiquotations @{Isar.state} and @{Isar.goal};
wenzelm
parents:
37216
diff
changeset

302 

48776
37cd53e69840
faster compilation of ML with antiquotations: static ML_context is bound once in auxiliary structure Isabelle;
wenzelm
parents:
47815
diff
changeset

303 
fun diag_goal ctxt = 
37cd53e69840
faster compilation of ML with antiquotations: static ML_context is bound once in auxiliary structure Isabelle;
wenzelm
parents:
47815
diff
changeset

304 
Proof.goal (Toplevel.proof_of (diag_state ctxt)) 
37305
9763792e4ac7
diagnostic commands 'ML_val' and 'ML_command' may refer to antiquotations @{Isar.state} and @{Isar.goal};
wenzelm
parents:
37216
diff
changeset

305 
handle Toplevel.UNDEF => error "No goal present"; 
9763792e4ac7
diagnostic commands 'ML_val' and 'ML_command' may refer to antiquotations @{Isar.state} and @{Isar.goal};
wenzelm
parents:
37216
diff
changeset

306 

43560
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
42464
diff
changeset

307 
val _ = 
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
42464
diff
changeset

308 
Context.>> (Context.map_theory 
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
42464
diff
changeset

309 
(ML_Antiquote.value (Binding.qualify true "Isar" (Binding.name "state")) 
48776
37cd53e69840
faster compilation of ML with antiquotations: static ML_context is bound once in auxiliary structure Isabelle;
wenzelm
parents:
47815
diff
changeset

310 
(Scan.succeed "Isar_Cmd.diag_state ML_context") #> 
43560
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
42464
diff
changeset

311 
ML_Antiquote.value (Binding.qualify true "Isar" (Binding.name "goal")) 
48776
37cd53e69840
faster compilation of ML with antiquotations: static ML_context is bound once in auxiliary structure Isabelle;
wenzelm
parents:
47815
diff
changeset

312 
(Scan.succeed "Isar_Cmd.diag_goal ML_context"))); 
5831  313 

314 

14934  315 
(* present draft files *) 
316 

48881
46e053eda5dd
clarified Parse.path vs. Parse.explode  prefer errors in proper transaction context;
wenzelm
parents:
48792
diff
changeset

317 
fun display_drafts names = Toplevel.imperative (fn () => 
46e053eda5dd
clarified Parse.path vs. Parse.explode  prefer errors in proper transaction context;
wenzelm
parents:
48792
diff
changeset

318 
let 
46e053eda5dd
clarified Parse.path vs. Parse.explode  prefer errors in proper transaction context;
wenzelm
parents:
48792
diff
changeset

319 
val paths = map Path.explode names; 
46e053eda5dd
clarified Parse.path vs. Parse.explode  prefer errors in proper transaction context;
wenzelm
parents:
48792
diff
changeset

320 
val outfile = File.shell_path (Present.drafts (getenv "ISABELLE_DOC_FORMAT") paths); 
40743  321 
in Isabelle_System.isabelle_tool "display" ("c " ^ outfile ^ " &"); () end); 
14934  322 

48881
46e053eda5dd
clarified Parse.path vs. Parse.explode  prefer errors in proper transaction context;
wenzelm
parents:
48792
diff
changeset

323 
fun print_drafts names = Toplevel.imperative (fn () => 
46e053eda5dd
clarified Parse.path vs. Parse.explode  prefer errors in proper transaction context;
wenzelm
parents:
48792
diff
changeset

324 
let 
46e053eda5dd
clarified Parse.path vs. Parse.explode  prefer errors in proper transaction context;
wenzelm
parents:
48792
diff
changeset

325 
val paths = map Path.explode names; 
46e053eda5dd
clarified Parse.path vs. Parse.explode  prefer errors in proper transaction context;
wenzelm
parents:
48792
diff
changeset

326 
val outfile = File.shell_path (Present.drafts "ps" paths); 
40743  327 
in Isabelle_System.isabelle_tool "print" ("c " ^ outfile); () end); 
14934  328 

329 

9513  330 
(* print parts of theory and proof context *) 
5831  331 

7308  332 
val print_context = Toplevel.keep Toplevel.print_state_context; 
9513  333 

20621  334 
fun print_theory verbose = Toplevel.unknown_theory o 
33389  335 
Toplevel.keep (Pretty.writeln o Proof_Display.pretty_full_theory verbose o Toplevel.theory_of); 
9513  336 

21663  337 
val print_syntax = Toplevel.unknown_context o 
42360  338 
Toplevel.keep (Proof_Context.print_syntax o Toplevel.context_of); 
9513  339 

21725  340 
val print_abbrevs = Toplevel.unknown_context o 
42360  341 
Toplevel.keep (Proof_Context.print_abbrevs o Toplevel.context_of); 
21725  342 

35141  343 
val print_facts = Toplevel.unknown_context o 
42360  344 
Toplevel.keep (Proof_Context.print_lthms o Toplevel.context_of); 
21003
37492b0062c6
renamed print_lthms to print_facts, do not insist on proof state;
wenzelm
parents:
20978
diff
changeset

345 

35141  346 
val print_configs = Toplevel.unknown_context o 
347 
Toplevel.keep (Attrib.print_configs o Toplevel.context_of); 

23989  348 

35141  349 
val print_theorems_proof = 
42360  350 
Toplevel.keep (Proof_Context.print_lthms o Proof.context_of o Toplevel.proof_of); 
17066  351 

33515
d066e8369a33
print_theorems: suppress concealed (global) facts, unless "!" option is given;
wenzelm
parents:
33456
diff
changeset

352 
fun print_theorems_theory verbose = Toplevel.keep (fn state => 
18588  353 
Toplevel.theory_of state > 
30801  354 
(case Toplevel.previous_context_of state of 
42360  355 
SOME prev => Proof_Display.print_theorems_diff verbose (Proof_Context.theory_of prev) 
33515
d066e8369a33
print_theorems: suppress concealed (global) facts, unless "!" option is given;
wenzelm
parents:
33456
diff
changeset

356 
 NONE => Proof_Display.print_theorems verbose)); 
18588  357 

33515
d066e8369a33
print_theorems: suppress concealed (global) facts, unless "!" option is given;
wenzelm
parents:
33456
diff
changeset

358 
fun print_theorems verbose = 
d066e8369a33
print_theorems: suppress concealed (global) facts, unless "!" option is given;
wenzelm
parents:
33456
diff
changeset

359 
Toplevel.unknown_context o print_theorems_theory verbose o print_theorems_proof; 
9513  360 

12060  361 
val print_locales = Toplevel.unknown_theory o 
29360  362 
Toplevel.keep (Locale.print_locales o Toplevel.theory_of); 
12060  363 

33515
d066e8369a33
print_theorems: suppress concealed (global) facts, unless "!" option is given;
wenzelm
parents:
33456
diff
changeset

364 
fun print_locale (verbose, name) = Toplevel.unknown_theory o 
d066e8369a33
print_theorems: suppress concealed (global) facts, unless "!" option is given;
wenzelm
parents:
33456
diff
changeset

365 
Toplevel.keep (fn state => Locale.print_locale (Toplevel.theory_of state) verbose name); 
15596  366 

32804
ca430e6aee1c
Propagation of mixins for interpretation; reactivated diagnostic command print_interps.
ballarin
parents:
32149
diff
changeset

367 
fun print_registrations name = Toplevel.unknown_context o 
ca430e6aee1c
Propagation of mixins for interpretation; reactivated diagnostic command print_interps.
ballarin
parents:
32149
diff
changeset

368 
Toplevel.keep (fn state => 
38109  369 
Locale.print_registrations (Toplevel.context_of state) name); 
32804
ca430e6aee1c
Propagation of mixins for interpretation; reactivated diagnostic command print_interps.
ballarin
parents:
32149
diff
changeset

370 

41435  371 
fun print_dependencies (clean, expression) = Toplevel.unknown_context o 
372 
Toplevel.keep (fn state => 

373 
Expression.print_dependencies (Toplevel.context_of state) clean expression); 

374 

9513  375 
val print_attributes = Toplevel.unknown_theory o 
376 
Toplevel.keep (Attrib.print_attributes o Toplevel.theory_of); 

377 

16026  378 
val print_simpset = Toplevel.unknown_context o 
30357  379 
Toplevel.keep (fn state => 
380 
let val ctxt = Toplevel.context_of state 

32149
ef59550a55d3
renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of  same for claset and clasimpset;
wenzelm
parents:
32091
diff
changeset

381 
in Pretty.writeln (Simplifier.pretty_ss ctxt (simpset_of ctxt)) end); 
16026  382 

12382  383 
val print_rules = Toplevel.unknown_context o 
33369  384 
Toplevel.keep (Context_Rules.print_rules o Toplevel.context_of); 
12382  385 

9513  386 
val print_trans_rules = Toplevel.unknown_context o 
18639  387 
Toplevel.keep (Calculation.print_rules o Toplevel.context_of); 
9513  388 

389 
val print_methods = Toplevel.unknown_theory o 

390 
Toplevel.keep (Method.print_methods o Toplevel.theory_of); 

391 

43564
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43560
diff
changeset

392 
val print_antiquotations = 
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43560
diff
changeset

393 
Toplevel.keep (Thy_Output.print_antiquotations o Toplevel.context_of); 
5831  394 

22485  395 
val thy_deps = Toplevel.unknown_theory o Toplevel.keep (fn state => 
396 
let 

397 
val thy = Toplevel.theory_of state; 

37866
cd1d1bc7684c
thy_deps: more direct comparison of sessions, which is presumably what "unfold" is meant to indicate here  also avoid referring to accidental theory loader state;
wenzelm
parents:
37305
diff
changeset

398 
val thy_session = Present.session_name thy; 
cd1d1bc7684c
thy_deps: more direct comparison of sessions, which is presumably what "unfold" is meant to indicate here  also avoid referring to accidental theory loader state;
wenzelm
parents:
37305
diff
changeset

399 

42425  400 
val gr = rev (Theory.nodes_of thy) > map (fn node => 
22602
a165d9ed08b8
simplified thy_deps using Theory.ancestors_of (in order of creation);
wenzelm
parents:
22573
diff
changeset

401 
let 
a165d9ed08b8
simplified thy_deps using Theory.ancestors_of (in order of creation);
wenzelm
parents:
22573
diff
changeset

402 
val name = Context.theory_name node; 
a165d9ed08b8
simplified thy_deps using Theory.ancestors_of (in order of creation);
wenzelm
parents:
22573
diff
changeset

403 
val parents = map Context.theory_name (Theory.parents_of node); 
37866
cd1d1bc7684c
thy_deps: more direct comparison of sessions, which is presumably what "unfold" is meant to indicate here  also avoid referring to accidental theory loader state;
wenzelm
parents:
37305
diff
changeset

404 
val session = Present.session_name node; 
cd1d1bc7684c
thy_deps: more direct comparison of sessions, which is presumably what "unfold" is meant to indicate here  also avoid referring to accidental theory loader state;
wenzelm
parents:
37305
diff
changeset

405 
val unfold = (session = thy_session); 
cd1d1bc7684c
thy_deps: more direct comparison of sessions, which is presumably what "unfold" is meant to indicate here  also avoid referring to accidental theory loader state;
wenzelm
parents:
37305
diff
changeset

406 
in {name = name, ID = name, parents = parents, dir = session, unfold = unfold, path = ""} end); 
22602
a165d9ed08b8
simplified thy_deps using Theory.ancestors_of (in order of creation);
wenzelm
parents:
22573
diff
changeset

407 
in Present.display_graph gr end); 
22485  408 

20574  409 
val class_deps = Toplevel.unknown_theory o Toplevel.keep (fn state => 
410 
let 

42358
b47d41d9f4b5
Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;
wenzelm
parents:
42247
diff
changeset

411 
val ctxt = Toplevel.context_of state; 
42360  412 
val {classes = (space, algebra), ...} = Type.rep_tsig (Proof_Context.tsig_of ctxt); 
36328
4d9deabf6474
replaced Sorts.rep_algebra by slightly more abstract selectors classes_of/arities_of;
wenzelm
parents:
36323
diff
changeset

413 
val classes = Sorts.classes_of algebra; 
20574  414 
fun entry (c, (i, (_, cs))) = 
44338
700008399ee5
refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists  order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents:
43564
diff
changeset

415 
(i, {name = Name_Space.extern ctxt space c, ID = c, parents = Graph.Keys.dest cs, 
20574  416 
dir = "", unfold = true, path = ""}); 
417 
val gr = 

418 
Graph.fold (cons o entry) classes [] 

419 
> sort (int_ord o pairself #1) > map #2; 

420 
in Present.display_graph gr end); 

421 

9513  422 
fun thm_deps args = Toplevel.unknown_theory o Toplevel.keep (fn state => 
37870
dd9cfc512b7f
thm_deps/unused_thms: Context.get_theory based on proper theory ancestry, not accidental theory loader state;
wenzelm
parents:
37866
diff
changeset

423 
Thm_Deps.thm_deps (Toplevel.theory_of state) 
38331
6e72f31999ac
prefer plain Attrib.eval_thms with plain Proof.context instead of Proof.state;
wenzelm
parents:
38139
diff
changeset

424 
(Attrib.eval_thms (Toplevel.context_of state) args)); 
9454  425 

5831  426 

26184  427 
(* find unused theorems *) 
428 

26186
9af968b694d9
unused_thms: print via official context (ProofContext.pretty_fact),
wenzelm
parents:
26184
diff
changeset

429 
fun unused_thms opt_range = Toplevel.keep (fn state => 
9af968b694d9
unused_thms: print via official context (ProofContext.pretty_fact),
wenzelm
parents:
26184
diff
changeset

430 
let 
9af968b694d9
unused_thms: print via official context (ProofContext.pretty_fact),
wenzelm
parents:
26184
diff
changeset

431 
val thy = Toplevel.theory_of state; 
9af968b694d9
unused_thms: print via official context (ProofContext.pretty_fact),
wenzelm
parents:
26184
diff
changeset

432 
val ctxt = Toplevel.context_of state; 
42360  433 
fun pretty_thm (a, th) = Proof_Context.pretty_fact ctxt (a, [th]); 
37870
dd9cfc512b7f
thm_deps/unused_thms: Context.get_theory based on proper theory ancestry, not accidental theory loader state;
wenzelm
parents:
37866
diff
changeset

434 
val get_theory = Context.get_theory thy; 
26186
9af968b694d9
unused_thms: print via official context (ProofContext.pretty_fact),
wenzelm
parents:
26184
diff
changeset

435 
in 
33391  436 
Thm_Deps.unused_thms 
26186
9af968b694d9
unused_thms: print via official context (ProofContext.pretty_fact),
wenzelm
parents:
26184
diff
changeset

437 
(case opt_range of 
26694  438 
NONE => (Theory.parents_of thy, [thy]) 
37870
dd9cfc512b7f
thm_deps/unused_thms: Context.get_theory based on proper theory ancestry, not accidental theory loader state;
wenzelm
parents:
37866
diff
changeset

439 
 SOME (xs, NONE) => (map get_theory xs, [thy]) 
dd9cfc512b7f
thm_deps/unused_thms: Context.get_theory based on proper theory ancestry, not accidental theory loader state;
wenzelm
parents:
37866
diff
changeset

440 
 SOME (xs, SOME ys) => (map get_theory xs, map get_theory ys)) 
26186
9af968b694d9
unused_thms: print via official context (ProofContext.pretty_fact),
wenzelm
parents:
26184
diff
changeset

441 
> map pretty_thm > Pretty.chunks > Pretty.writeln 
9af968b694d9
unused_thms: print via official context (ProofContext.pretty_fact),
wenzelm
parents:
26184
diff
changeset

442 
end); 
26184  443 

444 

5831  445 
(* print proof context contents *) 
446 

35141  447 
val print_binds = Toplevel.unknown_context o 
42360  448 
Toplevel.keep (Proof_Context.print_binds o Toplevel.context_of); 
9513  449 

35141  450 
val print_cases = Toplevel.unknown_context o 
42360  451 
Toplevel.keep (Proof_Context.print_cases o Toplevel.context_of); 
5831  452 

453 

19268  454 
(* print theorems, terms, types etc. *) 
455 

19385
c0f2f8224ea8
print_term etc.: actually observe print mode in final output;
wenzelm
parents:
19268
diff
changeset

456 
local 
c0f2f8224ea8
print_term etc.: actually observe print mode in final output;
wenzelm
parents:
19268
diff
changeset

457 

38331
6e72f31999ac
prefer plain Attrib.eval_thms with plain Proof.context instead of Proof.state;
wenzelm
parents:
38139
diff
changeset

458 
fun string_of_stmts ctxt args = 
6e72f31999ac
prefer plain Attrib.eval_thms with plain Proof.context instead of Proof.state;
wenzelm
parents:
38139
diff
changeset

459 
Attrib.eval_thms ctxt args 
6e72f31999ac
prefer plain Attrib.eval_thms with plain Proof.context instead of Proof.state;
wenzelm
parents:
38139
diff
changeset

460 
> map (Element.pretty_statement ctxt Thm.theoremK) 
19385
c0f2f8224ea8
print_term etc.: actually observe print mode in final output;
wenzelm
parents:
19268
diff
changeset

461 
> Pretty.chunks2 > Pretty.string_of; 
5880  462 

38331
6e72f31999ac
prefer plain Attrib.eval_thms with plain Proof.context instead of Proof.state;
wenzelm
parents:
38139
diff
changeset

463 
fun string_of_thms ctxt args = 
6e72f31999ac
prefer plain Attrib.eval_thms with plain Proof.context instead of Proof.state;
wenzelm
parents:
38139
diff
changeset

464 
Pretty.string_of (Display.pretty_thms ctxt (Attrib.eval_thms ctxt args)); 
5895  465 

19385
c0f2f8224ea8
print_term etc.: actually observe print mode in final output;
wenzelm
parents:
19268
diff
changeset

466 
fun string_of_prfs full state arg = 
32859
204f749f35a9
replaced Proof.get_goal state by Proof.flat_goal state, which provides the standard view on goals for (semi)automated tools;
wenzelm
parents:
32804
diff
changeset

467 
Pretty.string_of 
204f749f35a9
replaced Proof.get_goal state by Proof.flat_goal state, which provides the standard view on goals for (semi)automated tools;
wenzelm
parents:
32804
diff
changeset

468 
(case arg of 
15531  469 
NONE => 
12125
316d11f760f7
Commands prf and full_prf can now also be used to display proof term
berghofe
parents:
12069
diff
changeset

470 
let 
38331
6e72f31999ac
prefer plain Attrib.eval_thms with plain Proof.context instead of Proof.state;
wenzelm
parents:
38139
diff
changeset

471 
val {context = ctxt, goal = thm} = Proof.simple_goal (Toplevel.proof_of state); 
42360  472 
val thy = Proof_Context.theory_of ctxt; 
28814  473 
val prf = Thm.proof_of thm; 
17066  474 
val prop = Thm.full_prop_of thm; 
32859
204f749f35a9
replaced Proof.get_goal state by Proof.flat_goal state, which provides the standard view on goals for (semi)automated tools;
wenzelm
parents:
32804
diff
changeset

475 
val prf' = Proofterm.rewrite_proof_notypes ([], []) prf; 
12125
316d11f760f7
Commands prf and full_prf can now also be used to display proof term
berghofe
parents:
12069
diff
changeset

476 
in 
33388  477 
Proof_Syntax.pretty_proof ctxt 
17066  478 
(if full then Reconstruct.reconstruct_proof thy prop prf' else prf') 
12125
316d11f760f7
Commands prf and full_prf can now also be used to display proof term
berghofe
parents:
12069
diff
changeset

479 
end 
38331
6e72f31999ac
prefer plain Attrib.eval_thms with plain Proof.context instead of Proof.state;
wenzelm
parents:
38139
diff
changeset

480 
 SOME srcs => 
6e72f31999ac
prefer plain Attrib.eval_thms with plain Proof.context instead of Proof.state;
wenzelm
parents:
38139
diff
changeset

481 
let val ctxt = Toplevel.context_of state 
6e72f31999ac
prefer plain Attrib.eval_thms with plain Proof.context instead of Proof.state;
wenzelm
parents:
38139
diff
changeset

482 
in map (Proof_Syntax.pretty_proof_of ctxt full) (Attrib.eval_thms ctxt srcs) end 
6e72f31999ac
prefer plain Attrib.eval_thms with plain Proof.context instead of Proof.state;
wenzelm
parents:
38139
diff
changeset

483 
> Pretty.chunks); 
11524
197f2e14a714
Added functions for printing primitive proof terms.
berghofe
parents:
11017
diff
changeset

484 

38331
6e72f31999ac
prefer plain Attrib.eval_thms with plain Proof.context instead of Proof.state;
wenzelm
parents:
38139
diff
changeset

485 
fun string_of_prop ctxt s = 
5831  486 
let 
24508
c8b82fec6447
replaced ProofContext.read_term/prop by general Syntax.read_term/prop;
wenzelm
parents:
24314
diff
changeset

487 
val prop = Syntax.read_prop ctxt s; 
26704
51ee753cc2e3
token translations: context dependent, result Pretty.T;
wenzelm
parents:
26694
diff
changeset

488 
val ctxt' = Variable.auto_fixes prop ctxt; 
51ee753cc2e3
token translations: context dependent, result Pretty.T;
wenzelm
parents:
26694
diff
changeset

489 
in Pretty.string_of (Pretty.quote (Syntax.pretty_term ctxt' prop)) end; 
5831  490 

38331
6e72f31999ac
prefer plain Attrib.eval_thms with plain Proof.context instead of Proof.state;
wenzelm
parents:
38139
diff
changeset

491 
fun string_of_term ctxt s = 
5831  492 
let 
24508
c8b82fec6447
replaced ProofContext.read_term/prop by general Syntax.read_term/prop;
wenzelm
parents:
24314
diff
changeset

493 
val t = Syntax.read_term ctxt s; 
5831  494 
val T = Term.type_of t; 
26704
51ee753cc2e3
token translations: context dependent, result Pretty.T;
wenzelm
parents:
26694
diff
changeset

495 
val ctxt' = Variable.auto_fixes t ctxt; 
5831  496 
in 
19385
c0f2f8224ea8
print_term etc.: actually observe print mode in final output;
wenzelm
parents:
19268
diff
changeset

497 
Pretty.string_of 
26704
51ee753cc2e3
token translations: context dependent, result Pretty.T;
wenzelm
parents:
26694
diff
changeset

498 
(Pretty.block [Pretty.quote (Syntax.pretty_term ctxt' t), Pretty.fbrk, 
51ee753cc2e3
token translations: context dependent, result Pretty.T;
wenzelm
parents:
26694
diff
changeset

499 
Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' T)]) 
9128  500 
end; 
5831  501 

48792  502 
fun string_of_type ctxt (s, NONE) = 
503 
let val T = Syntax.read_typ ctxt s 

504 
in Pretty.string_of (Pretty.quote (Syntax.pretty_typ ctxt T)) end 

505 
 string_of_type ctxt (s1, SOME s2) = 

506 
let 

507 
val ctxt' = Config.put show_sorts true ctxt; 

508 
val raw_T = Syntax.parse_typ ctxt' s1; 

509 
val S = Syntax.read_sort ctxt' s2; 

510 
val T = 

511 
Syntax.check_term ctxt' 

512 
(Logic.mk_type raw_T > Type.constraint (Term.itselfT (Type_Infer.anyT S))) 

513 
> Logic.dest_type; 

514 
in Pretty.string_of (Pretty.quote (Syntax.pretty_typ ctxt' T)) end; 

9128  515 

23935  516 
fun print_item string_of (modes, arg) = Toplevel.keep (fn state => 
38331
6e72f31999ac
prefer plain Attrib.eval_thms with plain Proof.context instead of Proof.state;
wenzelm
parents:
38139
diff
changeset

517 
Print_Mode.with_modes modes (fn () => writeln (string_of state arg)) ()); 
19385
c0f2f8224ea8
print_term etc.: actually observe print mode in final output;
wenzelm
parents:
19268
diff
changeset

518 

c0f2f8224ea8
print_term etc.: actually observe print mode in final output;
wenzelm
parents:
19268
diff
changeset

519 
in 
9128  520 

38331
6e72f31999ac
prefer plain Attrib.eval_thms with plain Proof.context instead of Proof.state;
wenzelm
parents:
38139
diff
changeset

521 
val print_stmts = print_item (string_of_stmts o Toplevel.context_of); 
6e72f31999ac
prefer plain Attrib.eval_thms with plain Proof.context instead of Proof.state;
wenzelm
parents:
38139
diff
changeset

522 
val print_thms = print_item (string_of_thms o Toplevel.context_of); 
19385
c0f2f8224ea8
print_term etc.: actually observe print mode in final output;
wenzelm
parents:
19268
diff
changeset

523 
val print_prfs = print_item o string_of_prfs; 
38331
6e72f31999ac
prefer plain Attrib.eval_thms with plain Proof.context instead of Proof.state;
wenzelm
parents:
38139
diff
changeset

524 
val print_prop = print_item (string_of_prop o Toplevel.context_of); 
6e72f31999ac
prefer plain Attrib.eval_thms with plain Proof.context instead of Proof.state;
wenzelm
parents:
38139
diff
changeset

525 
val print_term = print_item (string_of_term o Toplevel.context_of); 
6e72f31999ac
prefer plain Attrib.eval_thms with plain Proof.context instead of Proof.state;
wenzelm
parents:
38139
diff
changeset

526 
val print_type = print_item (string_of_type o Toplevel.context_of); 
5831  527 

19385
c0f2f8224ea8
print_term etc.: actually observe print mode in final output;
wenzelm
parents:
19268
diff
changeset

528 
end; 
c0f2f8224ea8
print_term etc.: actually observe print mode in final output;
wenzelm
parents:
19268
diff
changeset

529 

12938
a646d0467d81
markup commands (from isar_thy.ML) with proper check of antiquotations;
wenzelm
parents:
12876
diff
changeset

530 

a646d0467d81
markup commands (from isar_thy.ML) with proper check of antiquotations;
wenzelm
parents:
12876
diff
changeset

531 
(* markup commands *) 
a646d0467d81
markup commands (from isar_thy.ML) with proper check of antiquotations;
wenzelm
parents:
12876
diff
changeset

532 

27853
916038f77be6
simplified markup commands  removed obsolete Present.results, always check text;
wenzelm
parents:
27730
diff
changeset

533 
fun header_markup txt = Toplevel.keep (fn state => 
48918
6e5fd4585512
check sidecomments of command spans (normally filtered out in Outer_Syntax.toplevel_source);
wenzelm
parents:
48881
diff
changeset

534 
if Toplevel.is_toplevel state then Thy_Output.check_text txt state 
27853
916038f77be6
simplified markup commands  removed obsolete Present.results, always check text;
wenzelm
parents:
27730
diff
changeset

535 
else raise Toplevel.UNDEF); 
12953
7d5bd53555d8
markup commands: proper theory/proof transactions!
wenzelm
parents:
12938
diff
changeset

536 

48918
6e5fd4585512
check sidecomments of command spans (normally filtered out in Outer_Syntax.toplevel_source);
wenzelm
parents:
48881
diff
changeset

537 
fun local_theory_markup (loc, txt) = Toplevel.present_local_theory loc (Thy_Output.check_text txt); 
6e5fd4585512
check sidecomments of command spans (normally filtered out in Outer_Syntax.toplevel_source);
wenzelm
parents:
48881
diff
changeset

538 
val proof_markup = Toplevel.present_proof o Thy_Output.check_text; 
12938
a646d0467d81
markup commands (from isar_thy.ML) with proper check of antiquotations;
wenzelm
parents:
12876
diff
changeset

539 

5831  540 
end; 