author  wenzelm 
Wed, 04 Apr 2007 23:29:42 +0200  
changeset 22602  a165d9ed08b8 
parent 22573  2ac646ab2f6c 
child 22604  6419dcc822f1 
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 

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

10 
val generic_setup: string option > theory > theory 
6917be2e647d
added various ML setup functions (from sign.ML, pure_thy.ML);
wenzelm
parents:
22087
diff
changeset

11 
val parse_ast_translation: bool * string > theory > theory 
6917be2e647d
added various ML setup functions (from sign.ML, pure_thy.ML);
wenzelm
parents:
22087
diff
changeset

12 
val parse_translation: bool * string > theory > theory 
6917be2e647d
added various ML setup functions (from sign.ML, pure_thy.ML);
wenzelm
parents:
22087
diff
changeset

13 
val print_translation: bool * string > theory > theory 
6917be2e647d
added various ML setup functions (from sign.ML, pure_thy.ML);
wenzelm
parents:
22087
diff
changeset

14 
val typed_print_translation: bool * string > theory > theory 
6917be2e647d
added various ML setup functions (from sign.ML, pure_thy.ML);
wenzelm
parents:
22087
diff
changeset

15 
val print_ast_translation: bool * string > theory > theory 
6917be2e647d
added various ML setup functions (from sign.ML, pure_thy.ML);
wenzelm
parents:
22087
diff
changeset

16 
val token_translation: string > theory > theory 
22239  17 
val oracle: bstring > string > string > 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 

20 
val apply_theorems: (thmref * Attrib.src list) list > theory > thm list * theory 

21 
val apply_theorems_i: (thm list * attribute list) list > theory > thm list * theory 

22087  22 
val declaration: string > local_theory > local_theory 
22239  23 
val simproc_setup: string > string list > string > string list > local_theory > local_theory 
21350  24 
val have: ((string * Attrib.src list) * (string * string list) list) list > 
25 
bool > Proof.state > Proof.state 

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

27 
bool > Proof.state > Proof.state 

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

29 
bool > Proof.state > Proof.state 

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

31 
bool > Proof.state > Proof.state 

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

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

34 
Toplevel.transition > Toplevel.transition 

35 
val default_proof: Toplevel.transition > Toplevel.transition 

36 
val immediate_proof: Toplevel.transition > Toplevel.transition 

37 
val done_proof: Toplevel.transition > Toplevel.transition 

38 
val skip_proof: Toplevel.transition > Toplevel.transition 

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

40 
val end_theory: theory > theory 

41 
val kill_theory: string > unit 

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

43 
> Toplevel.transition > Toplevel.transition 

7462  44 
val welcome: Toplevel.transition > Toplevel.transition 
45 
val init_toplevel: Toplevel.transition > Toplevel.transition 

5831  46 
val exit: Toplevel.transition > Toplevel.transition 
47 
val quit: Toplevel.transition > Toplevel.transition 

7908  48 
val touch_child_thys: string > Toplevel.transition > Toplevel.transition 
7101  49 
val touch_all_thys: Toplevel.transition > Toplevel.transition 
50 
val touch_thy: string > Toplevel.transition > Toplevel.transition 

51 
val remove_thy: string > Toplevel.transition > Toplevel.transition 

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

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

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

6686  61 
val undo: Toplevel.transition > Toplevel.transition 
21955  62 
val cannot_undo: string > Toplevel.transition > Toplevel.transition 
8498  63 
val kill: Toplevel.transition > Toplevel.transition 
17066  64 
val back: Toplevel.transition > Toplevel.transition 
14950  65 
val use: Path.T > Toplevel.transition > Toplevel.transition 
12876
a70df1e5bf10
got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents:
12758
diff
changeset

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

67 
val use_mltext: bool > string > Toplevel.transition > Toplevel.transition 
5831  68 
val use_commit: Toplevel.transition > Toplevel.transition 
14950  69 
val cd: Path.T > Toplevel.transition > Toplevel.transition 
5831  70 
val pwd: Toplevel.transition > Toplevel.transition 
71 
val use_thy: string > Toplevel.transition > Toplevel.transition 

6694  72 
val use_thy_only: string > Toplevel.transition > Toplevel.transition 
6195  73 
val update_thy: string > Toplevel.transition > Toplevel.transition 
7101  74 
val update_thy_only: string > Toplevel.transition > Toplevel.transition 
14950  75 
val display_drafts: Path.T list > Toplevel.transition > Toplevel.transition 
76 
val print_drafts: Path.T list > Toplevel.transition > Toplevel.transition 

7124  77 
val pretty_setmargin: int > Toplevel.transition > Toplevel.transition 
7308  78 
val print_context: Toplevel.transition > Toplevel.transition 
20621  79 
val print_theory: bool > Toplevel.transition > Toplevel.transition 
5831  80 
val print_syntax: Toplevel.transition > Toplevel.transition 
21725  81 
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

82 
val print_facts: Toplevel.transition > Toplevel.transition 
5880  83 
val print_theorems: Toplevel.transition > Toplevel.transition 
12060  84 
val print_locales: Toplevel.transition > Toplevel.transition 
18135  85 
val print_locale: bool * (Locale.expr * Element.context list) 
12758  86 
> Toplevel.transition > Toplevel.transition 
17139
165c97f9bb63
Printing of interpretations: option to show witness theorems;
ballarin
parents:
17066
diff
changeset

87 
val print_registrations: bool > string > Toplevel.transition > Toplevel.transition 
5831  88 
val print_attributes: Toplevel.transition > Toplevel.transition 
16026  89 
val print_simpset: Toplevel.transition > Toplevel.transition 
12382  90 
val print_rules: Toplevel.transition > Toplevel.transition 
11666  91 
val print_induct_rules: Toplevel.transition > Toplevel.transition 
9219  92 
val print_trans_rules: Toplevel.transition > Toplevel.transition 
5831  93 
val print_methods: Toplevel.transition > Toplevel.transition 
9219  94 
val print_antiquotations: Toplevel.transition > Toplevel.transition 
20574  95 
val class_deps: Toplevel.transition > Toplevel.transition 
22485  96 
val thy_deps: Toplevel.transition > Toplevel.transition 
20574  97 
val thm_deps: (thmref * Attrib.src list) list > Toplevel.transition > Toplevel.transition 
22340
275802767bf3
Remove duplicates from printed theorems in find_theorems
kleing
parents:
22239
diff
changeset

98 
val find_theorems: (int option * bool) * (bool * string FindTheorems.criterion) list 
13284  99 
> Toplevel.transition > Toplevel.transition 
5831  100 
val print_binds: Toplevel.transition > Toplevel.transition 
8369  101 
val print_cases: Toplevel.transition > Toplevel.transition 
19268  102 
val print_stmts: string list * (thmref * Attrib.src list) list 
103 
> Toplevel.transition > Toplevel.transition 

15703  104 
val print_thms: string list * (thmref * Attrib.src list) list 
10581  105 
> Toplevel.transition > Toplevel.transition 
15703  106 
val print_prfs: bool > string list * (thmref * Attrib.src list) list option 
11524
197f2e14a714
Added functions for printing primitive proof terms.
berghofe
parents:
11017
diff
changeset

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

108 
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

109 
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

110 
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

111 
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

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

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

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

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

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

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

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

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

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

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

122 
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

123 
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

124 
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

125 
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

126 
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

127 
val add_txt_raw: string * Position.T > Toplevel.transition > Toplevel.transition 
5831  128 
end; 
129 

130 
structure IsarCmd: ISAR_CMD = 

131 
struct 

132 

133 

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

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

135 

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

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

137 

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

138 
fun generic_setup NONE = (fn thy => thy > Context.setup ()) 
6917be2e647d
added various ML setup functions (from sign.ML, pure_thy.ML);
wenzelm
parents:
22087
diff
changeset

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

140 
ML_Context.use_let "val setup: theory > theory" "Context.map_theory setup" txt 
6917be2e647d
added various ML setup functions (from sign.ML, pure_thy.ML);
wenzelm
parents:
22087
diff
changeset

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

142 

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 
(* translation functions *) 
6917be2e647d
added various ML setup functions (from sign.ML, pure_thy.ML);
wenzelm
parents:
22087
diff
changeset

145 

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

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

147 

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

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

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

150 

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

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

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

153 

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

154 
in 
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 
fun parse_ast_translation (a, txt) = 
6917be2e647d
added various ML setup functions (from sign.ML, pure_thy.ML);
wenzelm
parents:
22087
diff
changeset

157 
txt > ML_Context.use_let ("val parse_ast_translation: (string * (" ^ advancedT a ^ 
6917be2e647d
added various ML setup functions (from sign.ML, pure_thy.ML);
wenzelm
parents:
22087
diff
changeset

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

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

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

161 

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

162 
fun parse_translation (a, txt) = 
6917be2e647d
added various ML setup functions (from sign.ML, pure_thy.ML);
wenzelm
parents:
22087
diff
changeset

163 
txt > ML_Context.use_let ("val parse_translation: (string * (" ^ advancedT a ^ 
6917be2e647d
added various ML setup functions (from sign.ML, pure_thy.ML);
wenzelm
parents:
22087
diff
changeset

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

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

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

167 

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

168 
fun print_translation (a, txt) = 
6917be2e647d
added various ML setup functions (from sign.ML, pure_thy.ML);
wenzelm
parents:
22087
diff
changeset

169 
txt > ML_Context.use_let ("val print_translation: (string * (" ^ advancedT a ^ 
6917be2e647d
added various ML setup functions (from sign.ML, pure_thy.ML);
wenzelm
parents:
22087
diff
changeset

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

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

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

173 

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

174 
fun print_ast_translation (a, txt) = 
6917be2e647d
added various ML setup functions (from sign.ML, pure_thy.ML);
wenzelm
parents:
22087
diff
changeset

175 
txt > ML_Context.use_let ("val print_ast_translation: (string * (" ^ advancedT a ^ 
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 

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

180 
fun typed_print_translation (a, txt) = 
6917be2e647d
added various ML setup functions (from sign.ML, pure_thy.ML);
wenzelm
parents:
22087
diff
changeset

181 
txt > ML_Context.use_let ("val typed_print_translation: (string * (" ^ advancedT a ^ 
6917be2e647d
added various ML setup functions (from sign.ML, pure_thy.ML);
wenzelm
parents:
22087
diff
changeset

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

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

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

185 

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

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

187 
ML_Context.use_let "val token_translation: (string * string * (string > string * real)) list" 
6917be2e647d
added various ML setup functions (from sign.ML, pure_thy.ML);
wenzelm
parents:
22087
diff
changeset

188 
"Context.map_theory (Sign.add_tokentrfuns token_translation)" 
6917be2e647d
added various ML setup functions (from sign.ML, pure_thy.ML);
wenzelm
parents:
22087
diff
changeset

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

190 

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

191 
end; 
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 

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

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

195 

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

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

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

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

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

202 
\ exception Arg of T;\n\ 
6917be2e647d
added various ML setup functions (from sign.ML, pure_thy.ML);
wenzelm
parents:
22087
diff
changeset

203 
\ val _ = ML_Context.>> (Theory.add_oracle (name, fn (thy, Arg x) => oracle thy x));\n\ 
6917be2e647d
added various ML setup functions (from sign.ML, pure_thy.ML);
wenzelm
parents:
22087
diff
changeset

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

205 
\ 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

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

207 
\ 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

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

209 
in ML_Context.use_mltext_update txt false end 
6917be2e647d
added various ML setup functions (from sign.ML, pure_thy.ML);
wenzelm
parents:
22087
diff
changeset

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

211 

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

212 

21350  213 
(* axioms *) 
214 

215 
fun add_axms f args thy = 

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

217 

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

219 

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

221 
add_axms 

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

223 

224 

225 
(* facts *) 

226 

227 
fun apply_theorems args thy = 

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

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

230 

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

232 

233 

22087  234 
(* declarations *) 
235 

236 
val declaration = 

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

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

238 
"val declaration: Morphism.morphism > Context.generic > Context.generic" 
22087  239 
"Context.map_proof (LocalTheory.declaration declaration)" 
240 
#> Context.proof_map; 

241 

242 

22202  243 
(* simprocs *) 
244 

22239  245 
fun simproc_setup name lhss proc identifier = 
22202  246 
ML_Context.use_let 
22239  247 
"val proc: Morphism.morphism > Simplifier.simpset > cterm > thm option" 
248 
("Context.map_proof (Simplifier.def_simproc {name = " ^ ML_Syntax.print_string name ^ ", \ 

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

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

22202  251 
> Context.proof_map; 
252 

253 

21350  254 
(* goals *) 
255 

256 
fun goal opt_chain goal stmt int = 

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

258 

259 
val have = goal I Proof.have; 

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

261 
val show = goal I Proof.show; 

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

263 

264 

265 
(* local endings *) 

266 

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

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

269 
val local_default_proof = Toplevel.proofs Proof.local_default_proof; 

270 
val local_immediate_proof = Toplevel.proofs Proof.local_immediate_proof; 

271 
val local_done_proof = Toplevel.proofs Proof.local_done_proof; 

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

273 

274 
val skip_local_qed = 

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

276 

277 

278 
(* global endings *) 

279 

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

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

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

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

284 
val global_skip_proof = Toplevel.end_proof Proof.global_skip_proof; 

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

286 

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

288 

289 

290 
(* common endings *) 

291 

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

293 
fun terminal_proof m = local_terminal_proof m o global_terminal_proof m; 

294 
val default_proof = local_default_proof o global_default_proof; 

295 
val immediate_proof = local_immediate_proof o global_immediate_proof; 

296 
val done_proof = local_done_proof o global_done_proof; 

297 
val skip_proof = local_skip_proof o global_skip_proof; 

298 

299 

300 
(* init and exit *) 

301 

302 
fun begin_theory name imports uses = 

21858
05f57309170c
avoid conflict with Alice keywords: renamed pack > implode, unpack > explode, any > many, avoided assert;
wenzelm
parents:
21725
diff
changeset

303 
ThyInfo.begin_theory Present.begin_theory name imports (map (apfst Path.explode) uses); 
21350  304 

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

21350  307 

308 
val kill_theory = ThyInfo.if_known_thy ThyInfo.remove_thy; 

309 

310 
fun theory (name, imports, uses) = 

311 
Toplevel.init_theory (begin_theory name imports uses) 

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

313 
(kill_theory o Context.theory_name); 

314 

7462  315 
val init_toplevel = Toplevel.imperative (fn () => raise Toplevel.RESTART); 
21350  316 

7462  317 
val welcome = Toplevel.imperative (writeln o Session.welcome); 
5831  318 

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

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

320 
(ML_Context.set_context (try Toplevel.generic_theory_of state); raise Toplevel.TERMINATE)); 
5831  321 

322 
val quit = Toplevel.imperative quit; 

323 

7101  324 

325 
(* touch theories *) 

326 

7908  327 
fun touch_child_thys name = Toplevel.imperative (fn () => ThyInfo.touch_child_thys name); 
7101  328 
val touch_all_thys = Toplevel.imperative ThyInfo.touch_all_thys; 
329 
fun touch_thy name = Toplevel.imperative (fn () => ThyInfo.touch_thy name); 

330 
fun remove_thy name = Toplevel.imperative (fn () => ThyInfo.remove_thy name); 

21350  331 
fun kill_thy name = Toplevel.imperative (fn () => kill_theory name); 
7101  332 

5831  333 

8453  334 
(* print state *) 
335 

8463  336 
fun with_modes modes e = 
337 
Library.setmp print_mode (modes @ ! print_mode) e (); 

338 

15531  339 
fun set_limit _ NONE = () 
340 
 set_limit r (SOME n) = r := n; 

9731  341 

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

342 
fun pr (modes, (lim1, lim2)) = Toplevel.keep (fn state => 
9731  343 
(set_limit goals_limit lim1; set_limit ProofContext.prems_limit lim2; Toplevel.quiet := false; 
19385
c0f2f8224ea8
print_term etc.: actually observe print mode in final output;
wenzelm
parents:
19268
diff
changeset

344 
with_modes modes (fn () => Toplevel.print_state true state))); 
8453  345 

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

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

348 

349 

6686  350 
(* history commands *) 
351 

16812  352 
val redo = 
353 
Toplevel.history History.redo o 

354 
Toplevel.actual_proof ProofHistory.redo o 

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

355 
Toplevel.skip_proof History.redo; 
6686  356 

16812  357 
fun undos_proof n = 
358 
Toplevel.actual_proof (fn prf => 

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

359 
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

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

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

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

7936  366 

367 
val kill_proof = kill_proof_notify (K ()); 

6686  368 

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

6686  371 

21955  372 
val undo = Toplevel.kill o undos_proof 1 o undo_theory o Toplevel.undo_exit; 
373 

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

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

376 

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

377 
val kill = Toplevel.kill o kill_proof; 
17899  378 

379 
val back = 

380 
Toplevel.actual_proof ProofHistory.back o 

381 
Toplevel.skip_proof (History.apply I); 

9273  382 

6686  383 

5831  384 
(* use ML text *) 
385 

16045  386 
fun use path = Toplevel.keep (fn state => 
22116
6917be2e647d
added various ML setup functions (from sign.ML, pure_thy.ML);
wenzelm
parents:
22087
diff
changeset

387 
ML_Context.setmp (try Toplevel.generic_theory_of state) (ThyInfo.load_file false) path); 
5831  388 

389 
(*passes changes of theory context*) 

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

390 
val use_mltext_theory = Toplevel.theory' o (Context.theory_map oo ML_Context.use_mltext_update); 
5831  391 

392 
(*ignore result theory context*) 

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

393 
fun use_mltext v txt = Toplevel.keep' (fn verb => fn state => 
22116
6917be2e647d
added various ML setup functions (from sign.ML, pure_thy.ML);
wenzelm
parents:
22087
diff
changeset

394 
(ML_Context.use_mltext txt (v andalso verb) (try Toplevel.generic_theory_of state))); 
5831  395 

20927  396 
val use_commit = Toplevel.imperative Secure.commit; 
5831  397 

398 

399 
(* current working directory *) 

400 

14950  401 
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

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

404 

405 
(* load theory files *) 

406 

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

407 
fun use_thy name = Toplevel.imperative (fn () => ML_Context.save ThyInfo.use_thy name); 
6917be2e647d
added various ML setup functions (from sign.ML, pure_thy.ML);
wenzelm
parents:
22087
diff
changeset

408 
fun use_thy_only name = Toplevel.imperative (fn () => ML_Context.save ThyInfo.use_thy_only name); 
6917be2e647d
added various ML setup functions (from sign.ML, pure_thy.ML);
wenzelm
parents:
22087
diff
changeset

409 
fun update_thy name = Toplevel.imperative (fn () => ML_Context.save ThyInfo.update_thy name); 
7124  410 
fun update_thy_only name = 
22116
6917be2e647d
added various ML setup functions (from sign.ML, pure_thy.ML);
wenzelm
parents:
22087
diff
changeset

411 
Toplevel.imperative (fn () => ML_Context.save ThyInfo.update_thy_only name); 
7124  412 

413 

14934  414 
(* present draft files *) 
415 

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

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

14934  419 

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

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

14934  423 

424 

7124  425 
(* pretty_setmargin *) 
426 

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

5831  428 

429 

9513  430 
(* print parts of theory and proof context *) 
5831  431 

7308  432 
val print_context = Toplevel.keep Toplevel.print_state_context; 
9513  433 

20621  434 
fun print_theory verbose = Toplevel.unknown_theory o 
435 
Toplevel.keep (ProofDisplay.print_full_theory verbose o Toplevel.theory_of); 

9513  436 

21663  437 
val print_syntax = Toplevel.unknown_context o 
438 
Toplevel.keep (ProofContext.print_syntax o Toplevel.context_of); 

9513  439 

21725  440 
val print_abbrevs = Toplevel.unknown_context o 
441 
Toplevel.keep (ProofContext.print_abbrevs o Toplevel.context_of); 

442 

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

443 
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

444 
ProofContext.setmp_verbose 
21506  445 
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

446 

17066  447 
val print_theorems_proof = Toplevel.keep (fn state => 
448 
ProofContext.setmp_verbose 

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

450 

18588  451 
val print_theorems_theory = Toplevel.keep (fn state => 
452 
Toplevel.theory_of state > 

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

20957  454 
SOME (SOME prev_thy) => ProofDisplay.print_theorems_diff (Context.theory_of prev_thy) 
19430  455 
 _ => ProofDisplay.print_theorems)); 
18588  456 

21663  457 
val print_theorems = Toplevel.unknown_context o print_theorems_theory o print_theorems_proof; 
9513  458 

12060  459 
val print_locales = Toplevel.unknown_theory o 
460 
Toplevel.keep (Locale.print_locales o Toplevel.theory_of); 

461 

22573  462 
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

463 
Toplevel.keep (fn state => 
22573  464 
Locale.print_locale (Toplevel.theory_of state) show_facts imports body); 
15596  465 

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

466 
fun print_registrations show_wits name = Toplevel.unknown_context o 
20957  467 
Toplevel.keep (Toplevel.node_case 
468 
(Context.cases (Locale.print_global_registrations show_wits name) 

469 
(Locale.print_local_registrations show_wits name)) 

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

470 
(Locale.print_local_registrations show_wits name o Proof.context_of)); 
12060  471 

9513  472 
val print_attributes = Toplevel.unknown_theory o 
473 
Toplevel.keep (Attrib.print_attributes o Toplevel.theory_of); 

474 

16026  475 
val print_simpset = Toplevel.unknown_context o 
20957  476 
Toplevel.keep (Toplevel.node_case 
477 
(Context.cases Simplifier.print_simpset Simplifier.print_local_simpset) 

16026  478 
(Simplifier.print_local_simpset o Proof.context_of)); 
479 

12382  480 
val print_rules = Toplevel.unknown_context o 
18639  481 
Toplevel.keep (ContextRules.print_rules o Toplevel.context_of); 
12382  482 

11666  483 
val print_induct_rules = Toplevel.unknown_context o 
18639  484 
Toplevel.keep (InductAttrib.print_rules o Toplevel.context_of); 
11666  485 

9513  486 
val print_trans_rules = Toplevel.unknown_context o 
18639  487 
Toplevel.keep (Calculation.print_rules o Toplevel.context_of); 
9513  488 

489 
val print_methods = Toplevel.unknown_theory o 

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

491 

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

492 
val print_antiquotations = Toplevel.imperative ThyOutput.print_antiquotations; 
5831  493 

22485  494 
val thy_deps = Toplevel.unknown_theory o Toplevel.keep (fn state => 
495 
let 

496 
val thy = Toplevel.theory_of state; 

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

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

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

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

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

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

502 
in Present.display_graph gr end); 
22485  503 

20574  504 
val class_deps = Toplevel.unknown_theory o Toplevel.keep (fn state => 
505 
let 

506 
val thy = Toplevel.theory_of state; 

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

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

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

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

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

512 
val gr = 

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

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

515 
in Present.display_graph gr end); 

516 

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

517 

16026  518 
(* retrieve theorems *) 
7615  519 

9513  520 
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

521 
ThmDeps.thm_deps (Proof.get_thmss (Toplevel.enter_proof_body state) args)); 
9454  522 

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

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

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

526 
val proof_state = Toplevel.enter_proof_body state; 
16026  527 
val ctxt = Proof.context_of proof_state; 
528 
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

529 
in FindTheorems.print_theorems ctxt opt_goal opt_lim rem_dups spec end); 
16026  530 

5831  531 

532 
(* print proof context contents *) 

533 

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

9513  536 

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

5831  539 

540 

19268  541 
(* print theorems, terms, types etc. *) 
542 

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

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

544 

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

545 
fun string_of_stmts state args = 
19268  546 
Proof.get_thmss state args 
21437  547 
> 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

548 
> Pretty.chunks2 > Pretty.string_of; 
5880  549 

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

550 
fun string_of_thms state args = 
12055  551 
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

552 
(Proof.get_thmss state args)); 
5895  553 

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

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

557 
let 
17066  558 
val (ctxt, (_, thm)) = Proof.get_goal state; 
559 
val {thy, der = (_, prf), ...} = Thm.rep_thm thm; 

560 
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

561 
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

562 
in 
17066  563 
ProofContext.pretty_proof ctxt 
564 
(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

565 
end 
15531  566 
 SOME args => Pretty.chunks 
17066  567 
(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

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

569 

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

570 
fun string_of_prop state s = 
5831  571 
let 
12055  572 
val ctxt = Proof.context_of state; 
573 
val prop = ProofContext.read_prop ctxt s; 

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

574 
in Pretty.string_of (Pretty.quote (ProofContext.pretty_term ctxt prop)) end; 
5831  575 

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

576 
fun string_of_term state s = 
5831  577 
let 
12055  578 
val ctxt = Proof.context_of state; 
579 
val t = ProofContext.read_term ctxt s; 

5831  580 
val T = Term.type_of t; 
581 
in 

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

582 
Pretty.string_of 
12055  583 
(Pretty.block [Pretty.quote (ProofContext.pretty_term ctxt t), Pretty.fbrk, 
19385
c0f2f8224ea8
print_term etc.: actually observe print mode in final output;
wenzelm
parents:
19268
diff
changeset

584 
Pretty.str "::", Pretty.brk 1, Pretty.quote (ProofContext.pretty_typ ctxt T)]) 
9128  585 
end; 
5831  586 

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

587 
fun string_of_type state s = 
5831  588 
let 
12055  589 
val ctxt = Proof.context_of state; 
590 
val T = ProofContext.read_typ ctxt s; 

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

591 
in Pretty.string_of (Pretty.quote (ProofContext.pretty_typ ctxt T)) end; 
9128  592 

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

593 
fun print_item string_of (modes, arg) = Toplevel.keep (fn state => with_modes modes (fn () => 
21003
37492b0062c6
renamed print_lthms to print_facts, do not insist on proof state;
wenzelm
parents:
20978
diff
changeset

594 
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

595 

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

596 
in 
9128  597 

19268  598 
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

599 
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

600 
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

601 
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

602 
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

603 
val print_type = print_item string_of_type; 
5831  604 

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

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

606 

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

607 

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

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

609 

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

610 
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

611 
(if Toplevel.is_toplevel state then () else raise Toplevel.UNDEF; 
19057  612 
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

613 

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

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

615 

19057  616 
fun present _ txt true node = OuterSyntax.check_text txt (SOME node) 
617 
 present f (s, _) false node = 

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

618 
ML_Context.setmp (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

619 

19057  620 
fun present_local_theory f (loc, txt) = Toplevel.present_local_theory loc (present f txt); 
621 
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

622 

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

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

624 

19057  625 
val add_chapter = present_local_theory Present.section; 
626 
val add_section = present_local_theory Present.section; 

627 
val add_subsection = present_local_theory Present.subsection; 

628 
val add_subsubsection = present_local_theory Present.subsubsection; 

629 
val add_text = present_local_theory (K ()); 

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

631 
val add_txt = present_proof (K ()); 

632 
val add_txt_raw = add_txt; 

633 
val add_sect = add_txt; 

634 
val add_subsect = add_txt; 

635 
val add_subsubsect = add_txt; 

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

636 

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

638 

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

639 
end; 