author  wenzelm 
Thu, 17 Apr 2008 16:30:50 +0200  
changeset 26704  51ee753cc2e3 
parent 26694  29f5c1a296bc 
child 27200  00b7b55b61bd 
permissions  rwrr 
5831  1 
(* Title: Pure/Isar/isar_cmd.ML 
2 
ID: $Id$ 

3 
Author: Markus Wenzel, TU Muenchen 

4 

21350  5 
Derived Isar commands. 
5831  6 
*) 
7 

8 
signature ISAR_CMD = 

9 
sig 

26435  10 
val generic_setup: string * Position.T > theory > theory 
26385
ae7564661e76
ML runtime compilation: pass position, tuned signature;
wenzelm
parents:
26336
diff
changeset

11 
val parse_ast_translation: bool * (string * Position.T) > theory > theory 
ae7564661e76
ML runtime compilation: pass position, tuned signature;
wenzelm
parents:
26336
diff
changeset

12 
val parse_translation: bool * (string * Position.T) > theory > theory 
ae7564661e76
ML runtime compilation: pass position, tuned signature;
wenzelm
parents:
26336
diff
changeset

13 
val print_translation: bool * (string * Position.T) > theory > theory 
ae7564661e76
ML runtime compilation: pass position, tuned signature;
wenzelm
parents:
26336
diff
changeset

14 
val typed_print_translation: bool * (string * Position.T) > theory > theory 
ae7564661e76
ML runtime compilation: pass position, tuned signature;
wenzelm
parents:
26336
diff
changeset

15 
val print_ast_translation: bool * (string * Position.T) > theory > theory 
ae7564661e76
ML runtime compilation: pass position, tuned signature;
wenzelm
parents:
26336
diff
changeset

16 
val token_translation: string * Position.T > theory > theory 
ae7564661e76
ML runtime compilation: pass position, tuned signature;
wenzelm
parents:
26336
diff
changeset

17 
val oracle: bstring > string > string * Position.T > theory > theory 
21350  18 
val add_axioms: ((bstring * string) * Attrib.src list) list > theory > theory 
19 
val add_defs: (bool * bool) * ((bstring * string) * Attrib.src list) list > theory > theory 

26336
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26186
diff
changeset

20 
val apply_theorems: (Facts.ref * Attrib.src list) list > theory > thm list * theory 
21350  21 
val apply_theorems_i: (thm list * attribute list) list > theory > thm list * theory 
26385
ae7564661e76
ML runtime compilation: pass position, tuned signature;
wenzelm
parents:
26336
diff
changeset

22 
val declaration: string * Position.T > local_theory > local_theory 
ae7564661e76
ML runtime compilation: pass position, tuned signature;
wenzelm
parents:
26336
diff
changeset

23 
val simproc_setup: string > string list > string * Position.T > string list > 
ae7564661e76
ML runtime compilation: pass position, tuned signature;
wenzelm
parents:
26336
diff
changeset

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

25 
val hide_names: bool > string * xstring list > theory > theory 
21350  26 
val have: ((string * Attrib.src list) * (string * string list) list) list > 
27 
bool > Proof.state > Proof.state 

28 
val hence: ((string * Attrib.src list) * (string * string list) list) list > 

29 
bool > Proof.state > Proof.state 

30 
val show: ((string * Attrib.src list) * (string * string list) list) list > 

31 
bool > Proof.state > Proof.state 

32 
val thus: ((string * Attrib.src list) * (string * string list) list) list > 

33 
bool > Proof.state > Proof.state 

34 
val qed: Method.text option > Toplevel.transition > Toplevel.transition 

35 
val terminal_proof: Method.text * Method.text option > 

36 
Toplevel.transition > Toplevel.transition 

37 
val default_proof: Toplevel.transition > Toplevel.transition 

38 
val immediate_proof: Toplevel.transition > Toplevel.transition 

39 
val done_proof: Toplevel.transition > Toplevel.transition 

40 
val skip_proof: Toplevel.transition > Toplevel.transition 

41 
val begin_theory: string > string list > (string * bool) list > bool > theory 

42 
val end_theory: theory > theory 

43 
val kill_theory: string > unit 

44 
val theory: string * string list * (string * bool) list 

45 
> Toplevel.transition > Toplevel.transition 

7462  46 
val welcome: Toplevel.transition > Toplevel.transition 
47 
val init_toplevel: Toplevel.transition > Toplevel.transition 

5831  48 
val exit: Toplevel.transition > Toplevel.transition 
49 
val quit: Toplevel.transition > Toplevel.transition 

7908  50 
val touch_child_thys: string > Toplevel.transition > Toplevel.transition 
7101  51 
val touch_thy: string > Toplevel.transition > Toplevel.transition 
52 
val remove_thy: string > Toplevel.transition > Toplevel.transition 

7931  53 
val kill_thy: string > Toplevel.transition > Toplevel.transition 
9731  54 
val pr: string list * (int option * int option) > Toplevel.transition > Toplevel.transition 
8453  55 
val disable_pr: Toplevel.transition > Toplevel.transition 
56 
val enable_pr: Toplevel.transition > Toplevel.transition 

6742  57 
val redo: Toplevel.transition > Toplevel.transition 
58 
val undos_proof: int > Toplevel.transition > Toplevel.transition 

7936  59 
val kill_proof_notify: (unit > unit) > Toplevel.transition > Toplevel.transition 
6742  60 
val kill_proof: Toplevel.transition > Toplevel.transition 
61 
val undo_theory: Toplevel.transition > Toplevel.transition 

6686  62 
val undo: Toplevel.transition > Toplevel.transition 
21955  63 
val cannot_undo: string > Toplevel.transition > Toplevel.transition 
8498  64 
val kill: Toplevel.transition > Toplevel.transition 
17066  65 
val back: Toplevel.transition > Toplevel.transition 
26489  66 
val ml_diag: bool > string * Position.T > Toplevel.transition > Toplevel.transition 
25793
6c2adbf41c7c
added nested_command (with explicit position argument via properties);
wenzelm
parents:
25331
diff
changeset

67 
val nested_command: Markup.property list > string * Position.T > Toplevel.transition 
14950  68 
val cd: Path.T > Toplevel.transition > Toplevel.transition 
5831  69 
val pwd: Toplevel.transition > Toplevel.transition 
14950  70 
val display_drafts: Path.T list > Toplevel.transition > Toplevel.transition 
71 
val print_drafts: Path.T list > Toplevel.transition > Toplevel.transition 

7124  72 
val pretty_setmargin: int > Toplevel.transition > Toplevel.transition 
7308  73 
val print_context: Toplevel.transition > Toplevel.transition 
20621  74 
val print_theory: bool > Toplevel.transition > Toplevel.transition 
5831  75 
val print_syntax: Toplevel.transition > Toplevel.transition 
21725  76 
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

77 
val print_facts: Toplevel.transition > Toplevel.transition 
24115  78 
val print_configs: Toplevel.transition > Toplevel.transition 
5880  79 
val print_theorems: Toplevel.transition > Toplevel.transition 
12060  80 
val print_locales: Toplevel.transition > Toplevel.transition 
18135  81 
val print_locale: bool * (Locale.expr * Element.context list) 
12758  82 
> Toplevel.transition > Toplevel.transition 
17139
165c97f9bb63
Printing of interpretations: option to show witness theorems;
ballarin
parents:
17066
diff
changeset

83 
val print_registrations: bool > string > Toplevel.transition > Toplevel.transition 
5831  84 
val print_attributes: Toplevel.transition > Toplevel.transition 
16026  85 
val print_simpset: Toplevel.transition > Toplevel.transition 
12382  86 
val print_rules: Toplevel.transition > Toplevel.transition 
9219  87 
val print_trans_rules: Toplevel.transition > Toplevel.transition 
5831  88 
val print_methods: Toplevel.transition > Toplevel.transition 
9219  89 
val print_antiquotations: Toplevel.transition > Toplevel.transition 
20574  90 
val class_deps: Toplevel.transition > Toplevel.transition 
22485  91 
val thy_deps: Toplevel.transition > Toplevel.transition 
26336
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26186
diff
changeset

92 
val thm_deps: (Facts.ref * Attrib.src list) list > Toplevel.transition > Toplevel.transition 
22340
275802767bf3
Remove duplicates from printed theorems in find_theorems
kleing
parents:
22239
diff
changeset

93 
val find_theorems: (int option * bool) * (bool * string FindTheorems.criterion) list 
13284  94 
> Toplevel.transition > Toplevel.transition 
26184  95 
val unused_thms: (string list * string list option) option > 
96 
Toplevel.transition > Toplevel.transition 

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

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

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

103 
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

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

105 
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

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

107 
val print_type: (string list * string) > Toplevel.transition > Toplevel.transition 
12938
a646d0467d81
markup commands (from isar_thy.ML) with proper check of antiquotations;
wenzelm
parents:
12876
diff
changeset

108 
val add_header: string * Position.T > Toplevel.transition > Toplevel.transition 
17262
63cf42df2723
add_chapter/section/subsection/subsubsection/text: optional locale specification;
wenzelm
parents:
17228
diff
changeset

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

110 
Toplevel.transition > Toplevel.transition 
63cf42df2723
add_chapter/section/subsection/subsubsection/text: optional locale specification;
wenzelm
parents:
17228
diff
changeset

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

112 
Toplevel.transition > Toplevel.transition 
63cf42df2723
add_chapter/section/subsection/subsubsection/text: optional locale specification;
wenzelm
parents:
17228
diff
changeset

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

114 
Toplevel.transition > Toplevel.transition 
63cf42df2723
add_chapter/section/subsection/subsubsection/text: optional locale specification;
wenzelm
parents:
17228
diff
changeset

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

116 
Toplevel.transition > Toplevel.transition 
63cf42df2723
add_chapter/section/subsection/subsubsection/text: optional locale specification;
wenzelm
parents:
17228
diff
changeset

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

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

119 
val add_text_raw: string * Position.T > Toplevel.transition > Toplevel.transition 
a646d0467d81
markup commands (from isar_thy.ML) with proper check of antiquotations;
wenzelm
parents:
12876
diff
changeset

120 
val add_sect: string * Position.T > Toplevel.transition > Toplevel.transition 
a646d0467d81
markup commands (from isar_thy.ML) with proper check of antiquotations;
wenzelm
parents:
12876
diff
changeset

121 
val add_subsect: string * Position.T > Toplevel.transition > Toplevel.transition 
a646d0467d81
markup commands (from isar_thy.ML) with proper check of antiquotations;
wenzelm
parents:
12876
diff
changeset

122 
val add_subsubsect: string * Position.T > Toplevel.transition > Toplevel.transition 
a646d0467d81
markup commands (from isar_thy.ML) with proper check of antiquotations;
wenzelm
parents:
12876
diff
changeset

123 
val add_txt: string * Position.T > Toplevel.transition > Toplevel.transition 
a646d0467d81
markup commands (from isar_thy.ML) with proper check of antiquotations;
wenzelm
parents:
12876
diff
changeset

124 
val add_txt_raw: string * Position.T > Toplevel.transition > Toplevel.transition 
5831  125 
end; 
126 

127 
structure IsarCmd: ISAR_CMD = 

128 
struct 

129 

130 

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

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

132 

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

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

134 

26435  135 
fun generic_setup (txt, pos) = 
26455  136 
ML_Context.expression pos "val setup: theory > theory" "Context.map_theory setup" txt 
26435  137 
> Context.theory_map; 
22116
6917be2e647d
added various ML setup functions (from sign.ML, pure_thy.ML);
wenzelm
parents:
22087
diff
changeset

138 

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

139 

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

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

141 

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

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

143 

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

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

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

146 

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

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

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

149 

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

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

151 

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

152 
fun parse_ast_translation (a, (txt, pos)) = 
26455  153 
txt > ML_Context.expression pos 
154 
("val parse_ast_translation: (string * (" ^ advancedT a ^ 

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

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

156 
("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

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

158 

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

159 
fun parse_translation (a, (txt, pos)) = 
26455  160 
txt > ML_Context.expression pos 
161 
("val parse_translation: (string * (" ^ advancedT a ^ 

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

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

163 
("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

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

165 

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

166 
fun print_translation (a, (txt, pos)) = 
26455  167 
txt > ML_Context.expression pos 
168 
("val print_translation: (string * (" ^ advancedT a ^ 

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

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

170 
("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

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

172 

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

173 
fun print_ast_translation (a, (txt, pos)) = 
26455  174 
txt > ML_Context.expression pos 
175 
("val print_ast_translation: (string * (" ^ advancedT a ^ 

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

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

177 
("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

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

179 

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

180 
fun typed_print_translation (a, (txt, pos)) = 
26455  181 
txt > ML_Context.expression pos 
182 
("val typed_print_translation: (string * (" ^ advancedT a ^ 

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

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

184 
("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

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

186 

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

187 
fun token_translation (txt, pos) = 
26455  188 
txt > ML_Context.expression pos 
26704
51ee753cc2e3
token translations: context dependent, result Pretty.T;
wenzelm
parents:
26694
diff
changeset

189 
"val token_translation: (string * string * (Proof.context > string > Pretty.T)) list" 
26385
ae7564661e76
ML runtime compilation: pass position, tuned signature;
wenzelm
parents:
26336
diff
changeset

190 
"Context.map_theory (Sign.add_tokentrfuns token_translation)" 
ae7564661e76
ML runtime compilation: pass position, tuned signature;
wenzelm
parents:
26336
diff
changeset

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

192 

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

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

194 

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

195 

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

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

197 

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

198 
fun oracle name typ (oracle, pos) = 
22116
6917be2e647d
added various ML setup functions (from sign.ML, pure_thy.ML);
wenzelm
parents:
22087
diff
changeset

199 
let val txt = 
26385
ae7564661e76
ML runtime compilation: pass position, tuned signature;
wenzelm
parents:
26336
diff
changeset

200 
"local\ 
ae7564661e76
ML runtime compilation: pass position, tuned signature;
wenzelm
parents:
26336
diff
changeset

201 
\ type T = " ^ typ ^ ";\ 
22116
6917be2e647d
added various ML setup functions (from sign.ML, pure_thy.ML);
wenzelm
parents:
22087
diff
changeset

202 
\ val oracle: theory > T > term = " ^ oracle ^ ";\n\ 
6917be2e647d
added various ML setup functions (from sign.ML, pure_thy.ML);
wenzelm
parents:
22087
diff
changeset

203 
\ val name = " ^ quote name ^ ";\n\ 
6917be2e647d
added various ML setup functions (from sign.ML, pure_thy.ML);
wenzelm
parents:
22087
diff
changeset

204 
\ exception Arg of T;\n\ 
26463  205 
\ val _ = Context.>> (Context.map_theory\n\ 
206 
\ (Theory.add_oracle (name, fn (thy, Arg x) => oracle thy x)));\n\ 

26425
6561665c5cb1
renamed ML_Context.the_context to ML_Context.the_global_context;
wenzelm
parents:
26415
diff
changeset

207 
\ val thy = ML_Context.the_global_context ();\n\ 
22116
6917be2e647d
added various ML setup functions (from sign.ML, pure_thy.ML);
wenzelm
parents:
22087
diff
changeset

208 
\ val invoke_" ^ name ^ " = Thm.invoke_oracle_i thy (Sign.full_name thy name);\n\ 
6917be2e647d
added various ML setup functions (from sign.ML, pure_thy.ML);
wenzelm
parents:
22087
diff
changeset

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

210 
\ fun " ^ name ^ " thy x = invoke_" ^ name ^ " (thy, Arg x);\n\ 
6917be2e647d
added various ML setup functions (from sign.ML, pure_thy.ML);
wenzelm
parents:
22087
diff
changeset

211 
\end;\n"; 
26455  212 
in Context.theory_map (ML_Context.exec (fn () => ML_Context.eval false pos txt)) end; 
22116
6917be2e647d
added various ML setup functions (from sign.ML, pure_thy.ML);
wenzelm
parents:
22087
diff
changeset

213 

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

214 

21350  215 
(* axioms *) 
216 

217 
fun add_axms f args thy = 

218 
f (map (fn (x, srcs) => (x, map (Attrib.attribute thy) srcs)) args) thy; 

219 

220 
val add_axioms = add_axms (snd oo PureThy.add_axioms); 

221 

222 
fun add_defs ((unchecked, overloaded), args) = 

223 
add_axms 

224 
(snd oo (if unchecked then PureThy.add_defs_unchecked else PureThy.add_defs) overloaded) args; 

225 

226 

227 
(* facts *) 

228 

229 
fun apply_theorems args thy = 

230 
let val facts = Attrib.map_facts (Attrib.attribute thy) [(("", []), args)] 

231 
in apfst (maps snd) (PureThy.note_thmss "" facts thy) end; 

232 

233 
fun apply_theorems_i args = apfst (maps snd) o PureThy.note_thmss_i "" [(("", []), args)]; 

234 

235 

22087  236 
(* declarations *) 
237 

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

238 
fun declaration (txt, pos) = 
26455  239 
txt > ML_Context.expression pos 
240 
"val declaration: Morphism.declaration" 

24020  241 
"Context.map_proof (LocalTheory.declaration declaration)" 
26385
ae7564661e76
ML runtime compilation: pass position, tuned signature;
wenzelm
parents:
26336
diff
changeset

242 
> Context.proof_map; 
22087  243 

244 

22202  245 
(* simprocs *) 
246 

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

247 
fun simproc_setup name lhss (proc, pos) identifier = 
26455  248 
ML_Context.expression pos 
22239  249 
"val proc: Morphism.morphism > Simplifier.simpset > cterm > thm option" 
250 
("Context.map_proof (Simplifier.def_simproc {name = " ^ ML_Syntax.print_string name ^ ", \ 

251 
\lhss = " ^ ML_Syntax.print_strings lhss ^ ", proc = proc, \ 

252 
\identifier = Library.maps ML_Context.thms " ^ ML_Syntax.print_strings identifier ^ "})") proc 

22202  253 
> Context.proof_map; 
254 

255 

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

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

257 

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

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

259 
[("class", (Sign.intern_class, can o Sign.certify_class, Sign.hide_class)), 
c95590e01df5
added hide_names command (formerly Sign.hide_names), support fact name space;
wenzelm
parents:
26626
diff
changeset

260 
("type", (Sign.intern_type, Sign.declared_tyname, Sign.hide_type)), 
c95590e01df5
added hide_names command (formerly Sign.hide_names), support fact name space;
wenzelm
parents:
26626
diff
changeset

261 
("const", (Sign.intern_const, Sign.declared_const, Sign.hide_const)), 
26694  262 
("fact", (PureThy.intern_fact, PureThy.defined_fact, PureThy.hide_fact))]; 
26671
c95590e01df5
added hide_names command (formerly Sign.hide_names), support fact name space;
wenzelm
parents:
26626
diff
changeset

263 

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

264 
fun hide_names b (kind, xnames) thy = 
c95590e01df5
added hide_names command (formerly Sign.hide_names), support fact name space;
wenzelm
parents:
26626
diff
changeset

265 
(case AList.lookup (op =) hide_kinds kind of 
c95590e01df5
added hide_names command (formerly Sign.hide_names), support fact name space;
wenzelm
parents:
26626
diff
changeset

266 
SOME (intern, check, hide) => 
c95590e01df5
added hide_names command (formerly Sign.hide_names), support fact name space;
wenzelm
parents:
26626
diff
changeset

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

268 
val names = map (intern thy) xnames; 
c95590e01df5
added hide_names command (formerly Sign.hide_names), support fact name space;
wenzelm
parents:
26626
diff
changeset

269 
val bads = filter_out (check thy) names; 
c95590e01df5
added hide_names command (formerly Sign.hide_names), support fact name space;
wenzelm
parents:
26626
diff
changeset

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

271 
if null bads then fold (hide b) names thy 
c95590e01df5
added hide_names command (formerly Sign.hide_names), support fact name space;
wenzelm
parents:
26626
diff
changeset

272 
else error ("Attempt to hide undeclared item(s): " ^ commas_quote bads) 
c95590e01df5
added hide_names command (formerly Sign.hide_names), support fact name space;
wenzelm
parents:
26626
diff
changeset

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

274 
 NONE => error ("Bad name space specification: " ^ quote kind)); 
c95590e01df5
added hide_names command (formerly Sign.hide_names), support fact name space;
wenzelm
parents:
26626
diff
changeset

275 

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

276 

21350  277 
(* goals *) 
278 

279 
fun goal opt_chain goal stmt int = 

280 
opt_chain #> goal NONE (K Seq.single) stmt int; 

281 

282 
val have = goal I Proof.have; 

283 
val hence = goal Proof.chain Proof.have; 

284 
val show = goal I Proof.show; 

285 
val thus = goal Proof.chain Proof.show; 

286 

287 

288 
(* local endings *) 

289 

290 
fun local_qed m = Toplevel.proofs (Proof.local_qed (m, true)); 

291 
val local_terminal_proof = Toplevel.proofs o Proof.local_terminal_proof; 

292 
val local_default_proof = Toplevel.proofs Proof.local_default_proof; 

293 
val local_immediate_proof = Toplevel.proofs Proof.local_immediate_proof; 

294 
val local_done_proof = Toplevel.proofs Proof.local_done_proof; 

295 
val local_skip_proof = Toplevel.proofs' Proof.local_skip_proof; 

296 

297 
val skip_local_qed = 

298 
Toplevel.skip_proof (History.apply (fn i => if i > 1 then i  1 else raise Toplevel.UNDEF)); 

299 

300 

301 
(* global endings *) 

302 

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

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

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

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

307 
val global_skip_proof = Toplevel.end_proof Proof.global_skip_proof; 

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

309 

310 
val skip_global_qed = Toplevel.skip_proof_to_theory (equal 1); 

311 

312 

313 
(* common endings *) 

314 

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

316 
fun terminal_proof m = local_terminal_proof m o global_terminal_proof m; 

317 
val default_proof = local_default_proof o global_default_proof; 

318 
val immediate_proof = local_immediate_proof o global_immediate_proof; 

319 
val done_proof = local_done_proof o global_done_proof; 

320 
val skip_proof = local_skip_proof o global_skip_proof; 

321 

322 

323 
(* init and exit *) 

324 

325 
fun begin_theory name imports uses = 

23897  326 
ThyInfo.begin_theory name imports (map (apfst Path.explode) uses); 
21350  327 

21566  328 
fun end_theory thy = 
329 
if ThyInfo.check_known_thy (Context.theory_name thy) then ThyInfo.end_theory thy else thy; 

21350  330 

331 
val kill_theory = ThyInfo.if_known_thy ThyInfo.remove_thy; 

332 

333 
fun theory (name, imports, uses) = 

334 
Toplevel.init_theory (begin_theory name imports uses) 

335 
(fn thy => (end_theory thy; ())) 

336 
(kill_theory o Context.theory_name); 

337 

7462  338 
val init_toplevel = Toplevel.imperative (fn () => raise Toplevel.RESTART); 
21350  339 

7462  340 
val welcome = Toplevel.imperative (writeln o Session.welcome); 
5831  341 

342 
val exit = Toplevel.keep (fn state => 

26599  343 
(Context.set_thread_data (try Toplevel.generic_theory_of state); 
24071  344 
raise Toplevel.TERMINATE)); 
5831  345 

346 
val quit = Toplevel.imperative quit; 

347 

7101  348 

349 
(* touch theories *) 

350 

7908  351 
fun touch_child_thys name = Toplevel.imperative (fn () => ThyInfo.touch_child_thys name); 
7101  352 
fun touch_thy name = Toplevel.imperative (fn () => ThyInfo.touch_thy name); 
353 
fun remove_thy name = Toplevel.imperative (fn () => ThyInfo.remove_thy name); 

21350  354 
fun kill_thy name = Toplevel.imperative (fn () => kill_theory name); 
7101  355 

5831  356 

8453  357 
(* print state *) 
358 

15531  359 
fun set_limit _ NONE = () 
360 
 set_limit r (SOME n) = r := n; 

9731  361 

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

362 
fun pr (modes, (lim1, lim2)) = Toplevel.keep (fn state => 
9731  363 
(set_limit goals_limit lim1; set_limit ProofContext.prems_limit lim2; Toplevel.quiet := false; 
23935  364 
PrintMode.with_modes modes (Toplevel.print_state true) state)); 
8453  365 

366 
val disable_pr = Toplevel.imperative (fn () => Toplevel.quiet := true); 

367 
val enable_pr = Toplevel.imperative (fn () => Toplevel.quiet := false); 

368 

369 

6686  370 
(* history commands *) 
371 

16812  372 
val redo = 
373 
Toplevel.history History.redo o 

374 
Toplevel.actual_proof ProofHistory.redo o 

15237
250e9be7a09d
Some changes to allow skipping of proof scripts.
berghofe
parents:
15222
diff
changeset

375 
Toplevel.skip_proof History.redo; 
6686  376 

16812  377 
fun undos_proof n = 
378 
Toplevel.actual_proof (fn prf => 

15237
250e9be7a09d
Some changes to allow skipping of proof scripts.
berghofe
parents:
15222
diff
changeset

379 
if ProofHistory.is_initial prf then raise Toplevel.UNDEF else funpow n ProofHistory.undo prf) o 
250e9be7a09d
Some changes to allow skipping of proof scripts.
berghofe
parents:
15222
diff
changeset

380 
Toplevel.skip_proof (fn h => 
250e9be7a09d
Some changes to allow skipping of proof scripts.
berghofe
parents:
15222
diff
changeset

381 
if History.is_initial h then raise Toplevel.UNDEF else funpow n History.undo h); 
6686  382 

7936  383 
fun kill_proof_notify (f: unit > unit) = Toplevel.history (fn hist => 
18588  384 
if is_some (Toplevel.theory_node (History.current hist)) then raise Toplevel.UNDEF 
385 
else (f (); History.undo hist)); 

7936  386 

387 
val kill_proof = kill_proof_notify (K ()); 

6686  388 

6742  389 
val undo_theory = Toplevel.history (fn hist => 
390 
if History.is_initial hist then raise Toplevel.UNDEF else History.undo hist); 

6686  391 

23500  392 
val undo = Toplevel.kill o undo_theory o Toplevel.undo_exit o undos_proof 1; 
21955  393 

394 
fun cannot_undo "end" = undo (*ProofGeneral legacy*) 

395 
 cannot_undo txt = Toplevel.imperative (fn () => error ("Cannot undo " ^ quote txt)); 

396 

21003
37492b0062c6
renamed print_lthms to print_facts, do not insist on proof state;
wenzelm
parents:
20978
diff
changeset

397 
val kill = Toplevel.kill o kill_proof; 
17899  398 

399 
val back = 

400 
Toplevel.actual_proof ProofHistory.back o 

401 
Toplevel.skip_proof (History.apply I); 

9273  402 

6686  403 

26489  404 
(* diagnostic ML evaluation *) 
5831  405 

26489  406 
fun ml_diag verbose (txt, pos) = Toplevel.keep (fn state => 
407 
(ML_Context.eval_in (try Toplevel.generic_theory_of state) verbose pos txt)); 

5831  408 

409 

25793
6c2adbf41c7c
added nested_command (with explicit position argument via properties);
wenzelm
parents:
25331
diff
changeset

410 
(* nested commands *) 
6c2adbf41c7c
added nested_command (with explicit position argument via properties);
wenzelm
parents:
25331
diff
changeset

411 

6c2adbf41c7c
added nested_command (with explicit position argument via properties);
wenzelm
parents:
25331
diff
changeset

412 
fun nested_command props (str, pos) = 
26053  413 
let val pos' = Position.of_properties (props > Position.default_properties pos) in 
25793
6c2adbf41c7c
added nested_command (with explicit position argument via properties);
wenzelm
parents:
25331
diff
changeset

414 
(case OuterSyntax.parse pos' str of 
25956  415 
[transition] => transition 
25793
6c2adbf41c7c
added nested_command (with explicit position argument via properties);
wenzelm
parents:
25331
diff
changeset

416 
 _ => error "exactly one command expected") 
6c2adbf41c7c
added nested_command (with explicit position argument via properties);
wenzelm
parents:
25331
diff
changeset

417 
end; 
6c2adbf41c7c
added nested_command (with explicit position argument via properties);
wenzelm
parents:
25331
diff
changeset

418 

6c2adbf41c7c
added nested_command (with explicit position argument via properties);
wenzelm
parents:
25331
diff
changeset

419 

5831  420 
(* current working directory *) 
421 

14950  422 
fun cd path = Toplevel.imperative (fn () => (File.cd path)); 
21858
05f57309170c
avoid conflict with Alice keywords: renamed pack > implode, unpack > explode, any > many, avoided assert;
wenzelm
parents:
21725
diff
changeset

423 
val pwd = Toplevel.imperative (fn () => writeln (Path.implode (File.pwd ()))); 
5831  424 

425 

14934  426 
(* present draft files *) 
427 

428 
fun display_drafts files = Toplevel.imperative (fn () => 

16258  429 
let val outfile = File.shell_path (Present.drafts (getenv "ISABELLE_DOC_FORMAT") files) 
430 
in File.isatool ("display c " ^ outfile ^ " &"); () end); 

14934  431 

432 
fun print_drafts files = Toplevel.imperative (fn () => 

16258  433 
let val outfile = File.shell_path (Present.drafts "ps" files) 
434 
in File.isatool ("print c " ^ outfile); () end); 

14934  435 

436 

7124  437 
(* pretty_setmargin *) 
438 

439 
fun pretty_setmargin n = Toplevel.imperative (fn () => Pretty.setmargin n); 

5831  440 

441 

9513  442 
(* print parts of theory and proof context *) 
5831  443 

7308  444 
val print_context = Toplevel.keep Toplevel.print_state_context; 
9513  445 

20621  446 
fun print_theory verbose = Toplevel.unknown_theory o 
22872  447 
Toplevel.keep (Pretty.writeln o ProofDisplay.pretty_full_theory verbose o Toplevel.theory_of); 
9513  448 

21663  449 
val print_syntax = Toplevel.unknown_context o 
450 
Toplevel.keep (ProofContext.print_syntax o Toplevel.context_of); 

9513  451 

21725  452 
val print_abbrevs = Toplevel.unknown_context o 
453 
Toplevel.keep (ProofContext.print_abbrevs o Toplevel.context_of); 

454 

21003
37492b0062c6
renamed print_lthms to print_facts, do not insist on proof state;
wenzelm
parents:
20978
diff
changeset

455 
val print_facts = Toplevel.unknown_context o Toplevel.keep (fn state => 
37492b0062c6
renamed print_lthms to print_facts, do not insist on proof state;
wenzelm
parents:
20978
diff
changeset

456 
ProofContext.setmp_verbose 
21506  457 
ProofContext.print_lthms (Toplevel.context_of state)); 
21003
37492b0062c6
renamed print_lthms to print_facts, do not insist on proof state;
wenzelm
parents:
20978
diff
changeset

458 

24115  459 
val print_configs = Toplevel.unknown_context o Toplevel.keep (fn state => 
460 
Attrib.print_configs (Toplevel.context_of state)); 

23989  461 

17066  462 
val print_theorems_proof = Toplevel.keep (fn state => 
463 
ProofContext.setmp_verbose 

464 
ProofContext.print_lthms (Proof.context_of (Toplevel.proof_of state))); 

465 

18588  466 
val print_theorems_theory = Toplevel.keep (fn state => 
467 
Toplevel.theory_of state > 

468 
(case Option.map Toplevel.theory_node (History.previous (Toplevel.node_history_of state)) of 

20957  469 
SOME (SOME prev_thy) => ProofDisplay.print_theorems_diff (Context.theory_of prev_thy) 
19430  470 
 _ => ProofDisplay.print_theorems)); 
18588  471 

21663  472 
val print_theorems = Toplevel.unknown_context o print_theorems_theory o print_theorems_proof; 
9513  473 

12060  474 
val print_locales = Toplevel.unknown_theory o 
475 
Toplevel.keep (Locale.print_locales o Toplevel.theory_of); 

476 

22573  477 
fun print_locale (show_facts, (imports, body)) = Toplevel.unknown_theory o 
19385
c0f2f8224ea8
print_term etc.: actually observe print mode in final output;
wenzelm
parents:
19268
diff
changeset

478 
Toplevel.keep (fn state => 
22573  479 
Locale.print_locale (Toplevel.theory_of state) show_facts imports body); 
15596  480 

17139
165c97f9bb63
Printing of interpretations: option to show witness theorems;
ballarin
parents:
17066
diff
changeset

481 
fun print_registrations show_wits name = Toplevel.unknown_context o 
20957  482 
Toplevel.keep (Toplevel.node_case 
24789
33b7fbc07361
Simplified interface for printing of interpretations.
ballarin
parents:
24560
diff
changeset

483 
(Context.cases (Locale.print_registrations show_wits name o ProofContext.init) 
33b7fbc07361
Simplified interface for printing of interpretations.
ballarin
parents:
24560
diff
changeset

484 
(Locale.print_registrations show_wits name)) 
33b7fbc07361
Simplified interface for printing of interpretations.
ballarin
parents:
24560
diff
changeset

485 
(Locale.print_registrations show_wits name o Proof.context_of)); 
12060  486 

9513  487 
val print_attributes = Toplevel.unknown_theory o 
488 
Toplevel.keep (Attrib.print_attributes o Toplevel.theory_of); 

489 

16026  490 
val print_simpset = Toplevel.unknown_context o 
26498  491 
Toplevel.keep (Simplifier.print_ss o Simplifier.local_simpset_of o Toplevel.context_of); 
16026  492 

12382  493 
val print_rules = Toplevel.unknown_context o 
18639  494 
Toplevel.keep (ContextRules.print_rules o Toplevel.context_of); 
12382  495 

9513  496 
val print_trans_rules = Toplevel.unknown_context o 
18639  497 
Toplevel.keep (Calculation.print_rules o Toplevel.context_of); 
9513  498 

499 
val print_methods = Toplevel.unknown_theory o 

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

501 

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

502 
val print_antiquotations = Toplevel.imperative ThyOutput.print_antiquotations; 
5831  503 

22485  504 
val thy_deps = Toplevel.unknown_theory o Toplevel.keep (fn state => 
505 
let 

506 
val thy = Toplevel.theory_of state; 

24560
2693220bd77f
thy_deps: ThyInfo.thy_ord, improved dir/unfold entry;
wenzelm
parents:
24508
diff
changeset

507 
val all_thys = sort ThyInfo.thy_ord (thy :: Theory.ancestors_of thy); 
22604  508 
val gr = all_thys > map (fn node => 
22602
a165d9ed08b8
simplified thy_deps using Theory.ancestors_of (in order of creation);
wenzelm
parents:
22573
diff
changeset

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

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

511 
val parents = map Context.theory_name (Theory.parents_of node); 
24560
2693220bd77f
thy_deps: ThyInfo.thy_ord, improved dir/unfold entry;
wenzelm
parents:
24508
diff
changeset

512 
val dir = Present.session_name node; 
2693220bd77f
thy_deps: ThyInfo.thy_ord, improved dir/unfold entry;
wenzelm
parents:
24508
diff
changeset

513 
val unfold = not (ThyInfo.known_thy name andalso ThyInfo.is_finished name); 
2693220bd77f
thy_deps: ThyInfo.thy_ord, improved dir/unfold entry;
wenzelm
parents:
24508
diff
changeset

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

515 
in Present.display_graph gr end); 
22485  516 

20574  517 
val class_deps = Toplevel.unknown_theory o Toplevel.keep (fn state => 
518 
let 

519 
val thy = Toplevel.theory_of state; 

520 
val {classes = (space, algebra), ...} = Type.rep_tsig (Sign.tsig_of thy); 

521 
val {classes, ...} = Sorts.rep_algebra algebra; 

522 
fun entry (c, (i, (_, cs))) = 

523 
(i, {name = NameSpace.extern space c, ID = c, parents = cs, 

524 
dir = "", unfold = true, path = ""}); 

525 
val gr = 

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

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

528 
in Present.display_graph gr end); 

529 

15964
f2074e12d1d4
searching for thms by combination of criteria (intro, elim, dest, name, term pattern)
kleing
parents:
15799
diff
changeset

530 

16026  531 
(* retrieve theorems *) 
7615  532 

9513  533 
fun thm_deps args = Toplevel.unknown_theory o Toplevel.keep (fn state => 
21003
37492b0062c6
renamed print_lthms to print_facts, do not insist on proof state;
wenzelm
parents:
20978
diff
changeset

534 
ThmDeps.thm_deps (Proof.get_thmss (Toplevel.enter_proof_body state) args)); 
9454  535 

24560
2693220bd77f
thy_deps: ThyInfo.thy_ord, improved dir/unfold entry;
wenzelm
parents:
24508
diff
changeset

536 
fun find_theorems ((opt_lim, rem_dups), spec) = 
22340
275802767bf3
Remove duplicates from printed theorems in find_theorems
kleing
parents:
22239
diff
changeset

537 
Toplevel.unknown_theory o Toplevel.keep (fn state => 
16026  538 
let 
21003
37492b0062c6
renamed print_lthms to print_facts, do not insist on proof state;
wenzelm
parents:
20978
diff
changeset

539 
val proof_state = Toplevel.enter_proof_body state; 
16026  540 
val ctxt = Proof.context_of proof_state; 
541 
val opt_goal = try Proof.get_goal proof_state > Option.map (Thm.prop_of o #2 o #2); 

22340
275802767bf3
Remove duplicates from printed theorems in find_theorems
kleing
parents:
22239
diff
changeset

542 
in FindTheorems.print_theorems ctxt opt_goal opt_lim rem_dups spec end); 
16026  543 

5831  544 

26184  545 
(* find unused theorems *) 
546 

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

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

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

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

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

551 
fun pretty_thm (a, th) = ProofContext.pretty_fact ctxt (a, [th]); 
9af968b694d9
unused_thms: print via official context (ProofContext.pretty_fact),
wenzelm
parents:
26184
diff
changeset

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

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

554 
(case opt_range of 
26694  555 
NONE => (Theory.parents_of thy, [thy]) 
556 
 SOME (xs, NONE) => (map ThyInfo.get_theory xs, [thy]) 

557 
 SOME (xs, SOME ys) => (map ThyInfo.get_theory xs, map ThyInfo.get_theory ys)) 

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

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

559 
end); 
26184  560 

561 

5831  562 
(* print proof context contents *) 
563 

21663  564 
val print_binds = Toplevel.unknown_context o Toplevel.keep (fn state => 
565 
ProofContext.setmp_verbose ProofContext.print_binds (Toplevel.context_of state)); 

9513  566 

21663  567 
val print_cases = Toplevel.unknown_context o Toplevel.keep (fn state => 
568 
ProofContext.setmp_verbose ProofContext.print_cases (Toplevel.context_of state)); 

5831  569 

570 

19268  571 
(* print theorems, terms, types etc. *) 
572 

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

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

574 

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

575 
fun string_of_stmts state args = 
19268  576 
Proof.get_thmss state args 
21437  577 
> map (Element.pretty_statement (Proof.context_of state) Thm.theoremK) 
19385
c0f2f8224ea8
print_term etc.: actually observe print mode in final output;
wenzelm
parents:
19268
diff
changeset

578 
> Pretty.chunks2 > Pretty.string_of; 
5880  579 

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

580 
fun string_of_thms state args = 
12055  581 
Pretty.string_of (ProofContext.pretty_thms (Proof.context_of state) 
19385
c0f2f8224ea8
print_term etc.: actually observe print mode in final output;
wenzelm
parents:
19268
diff
changeset

582 
(Proof.get_thmss state args)); 
5895  583 

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

584 
fun string_of_prfs full state arg = 
17066  585 
Pretty.string_of (case arg of 
15531  586 
NONE => 
12125
316d11f760f7
Commands prf and full_prf can now also be used to display proof term
berghofe
parents:
12069
diff
changeset

587 
let 
17066  588 
val (ctxt, (_, thm)) = Proof.get_goal state; 
26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26599
diff
changeset

589 
val thy = ProofContext.theory_of ctxt; 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26599
diff
changeset

590 
val prf = Thm.proof_of thm; 
17066  591 
val prop = Thm.full_prop_of thm; 
12125
316d11f760f7
Commands prf and full_prf can now also be used to display proof term
berghofe
parents:
12069
diff
changeset

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

593 
in 
17066  594 
ProofContext.pretty_proof ctxt 
595 
(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

596 
end 
15531  597 
 SOME args => Pretty.chunks 
17066  598 
(map (ProofContext.pretty_proof_of (Proof.context_of state) full) 
19385
c0f2f8224ea8
print_term etc.: actually observe print mode in final output;
wenzelm
parents:
19268
diff
changeset

599 
(Proof.get_thmss state args))); 
11524
197f2e14a714
Added functions for printing primitive proof terms.
berghofe
parents:
11017
diff
changeset

600 

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

601 
fun string_of_prop state s = 
5831  602 
let 
12055  603 
val ctxt = Proof.context_of state; 
24508
c8b82fec6447
replaced ProofContext.read_term/prop by general Syntax.read_term/prop;
wenzelm
parents:
24314
diff
changeset

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

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

606 
in Pretty.string_of (Pretty.quote (Syntax.pretty_term ctxt' prop)) end; 
5831  607 

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

608 
fun string_of_term state s = 
5831  609 
let 
12055  610 
val ctxt = Proof.context_of state; 
24508
c8b82fec6447
replaced ProofContext.read_term/prop by general Syntax.read_term/prop;
wenzelm
parents:
24314
diff
changeset

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

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

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

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

617 
Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' T)]) 
9128  618 
end; 
5831  619 

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

620 
fun string_of_type state s = 
5831  621 
let 
12055  622 
val ctxt = Proof.context_of state; 
25331  623 
val T = Syntax.read_typ ctxt s; 
24920  624 
in Pretty.string_of (Pretty.quote (Syntax.pretty_typ ctxt T)) end; 
9128  625 

23935  626 
fun print_item string_of (modes, arg) = Toplevel.keep (fn state => 
627 
PrintMode.with_modes modes (fn () => 

628 
writeln (string_of (Toplevel.enter_proof_body state) arg)) ()); 

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

629 

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

630 
in 
9128  631 

19268  632 
val print_stmts = print_item string_of_stmts; 
12876
a70df1e5bf10
got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents:
12758
diff
changeset

633 
val print_thms = print_item string_of_thms; 
19385
c0f2f8224ea8
print_term etc.: actually observe print mode in final output;
wenzelm
parents:
19268
diff
changeset

634 
val print_prfs = print_item o string_of_prfs; 
12876
a70df1e5bf10
got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents:
12758
diff
changeset

635 
val print_prop = print_item string_of_prop; 
a70df1e5bf10
got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents:
12758
diff
changeset

636 
val print_term = print_item string_of_term; 
a70df1e5bf10
got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents:
12758
diff
changeset

637 
val print_type = print_item string_of_type; 
5831  638 

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

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

640 

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

641 

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

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

643 

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

644 
fun add_header s = Toplevel.keep' (fn int => fn state => 
21858
05f57309170c
avoid conflict with Alice keywords: renamed pack > implode, unpack > explode, any > many, avoided assert;
wenzelm
parents:
21725
diff
changeset

645 
(if Toplevel.is_toplevel state then () else raise Toplevel.UNDEF; 
19057  646 
if int then OuterSyntax.check_text s NONE else ())); 
12938
a646d0467d81
markup commands (from isar_thy.ML) with proper check of antiquotations;
wenzelm
parents:
12876
diff
changeset

647 

12953
7d5bd53555d8
markup commands: proper theory/proof transactions!
wenzelm
parents:
12938
diff
changeset

648 
local 
7d5bd53555d8
markup commands: proper theory/proof transactions!
wenzelm
parents:
12938
diff
changeset

649 

19057  650 
fun present _ txt true node = OuterSyntax.check_text txt (SOME node) 
26415  651 
 present f (s, _) false node = Context.setmp_thread_data 
652 
(try (Toplevel.cases_node I (Context.Proof o Proof.context_of)) node) f s; 

12953
7d5bd53555d8
markup commands: proper theory/proof transactions!
wenzelm
parents:
12938
diff
changeset

653 

19057  654 
fun present_local_theory f (loc, txt) = Toplevel.present_local_theory loc (present f txt); 
655 
fun present_proof f txt = Toplevel.print o Toplevel.present_proof (present f txt); 

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

656 

12953
7d5bd53555d8
markup commands: proper theory/proof transactions!
wenzelm
parents:
12938
diff
changeset

657 
in 
7d5bd53555d8
markup commands: proper theory/proof transactions!
wenzelm
parents:
12938
diff
changeset

658 

19057  659 
val add_chapter = present_local_theory Present.section; 
660 
val add_section = present_local_theory Present.section; 

661 
val add_subsection = present_local_theory Present.subsection; 

662 
val add_subsubsection = present_local_theory Present.subsubsection; 

663 
val add_text = present_local_theory (K ()); 

664 
fun add_text_raw txt = present_local_theory (K ()) (NONE, txt); 

665 
val add_txt = present_proof (K ()); 

666 
val add_txt_raw = add_txt; 

667 
val add_sect = add_txt; 

668 
val add_subsect = add_txt; 

669 
val add_subsubsect = add_txt; 

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

670 

5831  671 
end; 
12953
7d5bd53555d8
markup commands: proper theory/proof transactions!
wenzelm
parents:
12938
diff
changeset

672 

7d5bd53555d8
markup commands: proper theory/proof transactions!
wenzelm
parents:
12938
diff
changeset

673 
end; 