author  wenzelm 
Sat, 16 Apr 2011 15:47:52 +0200  
changeset 42360  da8817d01e7c 
parent 42359  6ca5407863ed 
child 42425  2aa907d5ee4f 
permissions  rwrr 
5831  1 
(* Title: Pure/Isar/isar_cmd.ML 
2 
Author: Markus Wenzel, TU Muenchen 

3 

30805  4 
Miscellaneous Isar commands. 
5831  5 
*) 
6 

7 
signature ISAR_CMD = 

8 
sig 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

35 
Toplevel.transition > Toplevel.transition 

36 
val default_proof: Toplevel.transition > Toplevel.transition 

37 
val immediate_proof: Toplevel.transition > Toplevel.transition 

38 
val done_proof: Toplevel.transition > Toplevel.transition 

39 
val skip_proof: Toplevel.transition > Toplevel.transition 

30575  40 
val ml_diag: bool > Symbol_Pos.text * Position.T > Toplevel.transition > Toplevel.transition 
37305
9763792e4ac7
diagnostic commands 'ML_val' and 'ML_command' may refer to antiquotations @{Isar.state} and @{Isar.goal};
wenzelm
parents:
37216
diff
changeset

41 
val diag_state: unit > Toplevel.state 
9763792e4ac7
diagnostic commands 'ML_val' and 'ML_command' may refer to antiquotations @{Isar.state} and @{Isar.goal};
wenzelm
parents:
37216
diff
changeset

42 
val diag_goal: unit > {context: Proof.context, facts: thm list, goal: thm} 
14950  43 
val display_drafts: Path.T list > Toplevel.transition > Toplevel.transition 
44 
val print_drafts: Path.T list > Toplevel.transition > Toplevel.transition 

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

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

51 
val print_theorems: bool > Toplevel.transition > Toplevel.transition 
12060  52 
val print_locales: Toplevel.transition > Toplevel.transition 
29223  53 
val print_locale: bool * xstring > Toplevel.transition > Toplevel.transition 
32804
ca430e6aee1c
Propagation of mixins for interpretation; reactivated diagnostic command print_interps.
ballarin
parents:
32149
diff
changeset

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

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

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

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

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

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

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

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

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

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

78 
val print_type: (string list * string) > Toplevel.transition > Toplevel.transition 
30573  79 
val header_markup: Symbol_Pos.text * Position.T > Toplevel.transition > Toplevel.transition 
80 
val local_theory_markup: xstring option * (Symbol_Pos.text * Position.T) > 

17262
63cf42df2723
add_chapter/section/subsection/subsubsection/text: optional locale specification;
wenzelm
parents:
17228
diff
changeset

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

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

85 
structure Isar_Cmd: ISAR_CMD = 
5831  86 
struct 
87 

88 

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

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

90 

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

92 

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

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

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

97 

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

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

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

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

103 

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

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

105 

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

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

107 

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

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

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

110 

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

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

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

113 

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

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

115 

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

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

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

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

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

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

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

123 

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

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

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

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

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

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

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

131 

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

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

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

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

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

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

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

139 

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

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

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

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

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

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

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

147 

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

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

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

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

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

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

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

154 

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

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

156 

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

157 

42204  158 
(* translation rules *) 
159 

160 
fun read_trrules thy raw_rules = 

161 
let 

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

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

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

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

170 

171 

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

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

173 

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

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

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

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

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

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

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

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

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

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

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

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

186 

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

187 

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

188 
(* oldstyle axioms *) 
21350  189 

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

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

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

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

194 
(if unchecked then Global_Theory.add_defs_unchecked_cmd else Global_Theory.add_defs_cmd) 
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is globalonly;
wenzelm
parents:
39507
diff
changeset

195 
overloaded (map (fn ((b, ax), srcs) => ((b, ax), map (Attrib.attribute thy) srcs)) args) 
35852
4e3fe0b8687b
minor renovation of oldstyle 'axioms'  make it an alias of iterated 'axiomatization';
wenzelm
parents:
35141
diff
changeset

196 
> snd; 
21350  197 

198 

22087  199 
(* declarations *) 
200 

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

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

203 
> ML_Context.expression pos 
26455  204 
"val declaration: Morphism.declaration" 
40784  205 
("Context.map_proof (Local_Theory." ^ 
206 
(if syntax then "syntax_declaration" else "declaration") ^ " " ^ 

207 
Bool.toString pervasive ^ " declaration)") 

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

208 
> Context.proof_map; 
22087  209 

210 

22202  211 
(* simprocs *) 
212 

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

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

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

215 
> ML_Context.expression pos 
22239  216 
"val proc: Morphism.morphism > Simplifier.simpset > cterm > thm option" 
37198
3af985b10550
replaced ML_Lex.read_antiq by more concise ML_Lex.read, which includes full read/report with explicit position information;
wenzelm
parents:
37146
diff
changeset

217 
("Context.map_proof (Simplifier.def_simproc {name = " ^ ML_Syntax.print_string name ^ ", \ 
3af985b10550
replaced ML_Lex.read_antiq by more concise ML_Lex.read, which includes full read/report with explicit position information;
wenzelm
parents:
37146
diff
changeset

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

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

222 

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

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

224 

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

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

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

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

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

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

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

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

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

233 

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

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

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

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

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

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

239 

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

240 

21350  241 
(* goals *) 
242 

243 
fun goal opt_chain goal stmt int = 

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

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

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

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

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

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

251 

252 
(* local endings *) 

253 

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

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

258 
val local_done_proof = Toplevel.proof Proof.local_done_proof; 

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

21350  260 

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

263 

264 
(* global endings *) 

265 

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

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

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

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

270 
val global_skip_proof = Toplevel.end_proof Proof.global_skip_proof; 

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

272 

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

275 

276 
(* common endings *) 

277 

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

279 
fun terminal_proof m = local_terminal_proof m o global_terminal_proof m; 

280 
val default_proof = local_default_proof o global_default_proof; 

281 
val immediate_proof = local_immediate_proof o global_immediate_proof; 

282 
val done_proof = local_done_proof o global_done_proof; 

283 
val skip_proof = local_skip_proof o global_skip_proof; 

284 

285 

26489  286 
(* diagnostic ML evaluation *) 
5831  287 

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

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

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

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

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

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

293 

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

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

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

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

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

299 

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

300 
fun diag_state () = Diag_State.get (ML_Context.the_local_context ()); 
9763792e4ac7
diagnostic commands 'ML_val' and 'ML_command' may refer to antiquotations @{Isar.state} and @{Isar.goal};
wenzelm
parents:
37216
diff
changeset

301 

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

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

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

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

305 

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

306 
val _ = ML_Antiquote.value "Isar.state" (Scan.succeed "Isar_Cmd.diag_state ()"); 
9763792e4ac7
diagnostic commands 'ML_val' and 'ML_command' may refer to antiquotations @{Isar.state} and @{Isar.goal};
wenzelm
parents:
37216
diff
changeset

307 
val _ = ML_Antiquote.value "Isar.goal" (Scan.succeed "Isar_Cmd.diag_goal ()"); 
5831  308 

309 

14934  310 
(* present draft files *) 
311 

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

16258  313 
let val outfile = File.shell_path (Present.drafts (getenv "ISABELLE_DOC_FORMAT") files) 
40743  314 
in Isabelle_System.isabelle_tool "display" ("c " ^ outfile ^ " &"); () end); 
14934  315 

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

16258  317 
let val outfile = File.shell_path (Present.drafts "ps" files) 
40743  318 
in Isabelle_System.isabelle_tool "print" ("c " ^ outfile); () end); 
14934  319 

320 

9513  321 
(* print parts of theory and proof context *) 
5831  322 

7308  323 
val print_context = Toplevel.keep Toplevel.print_state_context; 
9513  324 

20621  325 
fun print_theory verbose = Toplevel.unknown_theory o 
33389  326 
Toplevel.keep (Pretty.writeln o Proof_Display.pretty_full_theory verbose o Toplevel.theory_of); 
9513  327 

21663  328 
val print_syntax = Toplevel.unknown_context o 
42360  329 
Toplevel.keep (Proof_Context.print_syntax o Toplevel.context_of); 
9513  330 

21725  331 
val print_abbrevs = Toplevel.unknown_context o 
42360  332 
Toplevel.keep (Proof_Context.print_abbrevs o Toplevel.context_of); 
21725  333 

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

336 

35141  337 
val print_configs = Toplevel.unknown_context o 
338 
Toplevel.keep (Attrib.print_configs o Toplevel.context_of); 

23989  339 

35141  340 
val print_theorems_proof = 
42360  341 
Toplevel.keep (Proof_Context.print_lthms o Proof.context_of o Toplevel.proof_of); 
17066  342 

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

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

347 
 NONE => Proof_Display.print_theorems verbose)); 
18588  348 

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

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

350 
Toplevel.unknown_context o print_theorems_theory verbose o print_theorems_proof; 
9513  351 

12060  352 
val print_locales = Toplevel.unknown_theory o 
29360  353 
Toplevel.keep (Locale.print_locales o Toplevel.theory_of); 
12060  354 

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

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

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

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

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

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

361 

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

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

365 

9513  366 
val print_attributes = Toplevel.unknown_theory o 
367 
Toplevel.keep (Attrib.print_attributes o Toplevel.theory_of); 

368 

16026  369 
val print_simpset = Toplevel.unknown_context o 
30357  370 
Toplevel.keep (fn state => 
371 
let val ctxt = Toplevel.context_of state 

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

372 
in Pretty.writeln (Simplifier.pretty_ss ctxt (simpset_of ctxt)) end); 
16026  373 

12382  374 
val print_rules = Toplevel.unknown_context o 
33369  375 
Toplevel.keep (Context_Rules.print_rules o Toplevel.context_of); 
12382  376 

9513  377 
val print_trans_rules = Toplevel.unknown_context o 
18639  378 
Toplevel.keep (Calculation.print_rules o Toplevel.context_of); 
9513  379 

380 
val print_methods = Toplevel.unknown_theory o 

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

382 

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

383 
val print_antiquotations = Toplevel.imperative Thy_Output.print_antiquotations; 
5831  384 

22485  385 
val thy_deps = Toplevel.unknown_theory o Toplevel.keep (fn state => 
386 
let 

387 
val thy = Toplevel.theory_of state; 

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

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

389 

38139
ac94ff28e9e1
eliminated Thy_Info.thy_ord, which is not really stable in interactive mode, since it depends on the somewhat accidental load order;
wenzelm
parents:
38109
diff
changeset

390 
val all_thys = rev (thy :: Theory.ancestors_of thy); 
22604  391 
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

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

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

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

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

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

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

398 
in Present.display_graph gr end); 
22485  399 

20574  400 
val class_deps = Toplevel.unknown_theory o Toplevel.keep (fn state => 
401 
let 

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

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

404 
val classes = Sorts.classes_of algebra; 
20574  405 
fun entry (c, (i, (_, cs))) = 
42358
b47d41d9f4b5
Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;
wenzelm
parents:
42247
diff
changeset

406 
(i, {name = Name_Space.extern ctxt space c, ID = c, parents = cs, 
20574  407 
dir = "", unfold = true, path = ""}); 
408 
val gr = 

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

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

411 
in Present.display_graph gr end); 

412 

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

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

415 
(Attrib.eval_thms (Toplevel.context_of state) args)); 
9454  416 

5831  417 

26184  418 
(* find unused theorems *) 
419 

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

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

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

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

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

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

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

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

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

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

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

433 
end); 
26184  434 

435 

5831  436 
(* print proof context contents *) 
437 

35141  438 
val print_binds = Toplevel.unknown_context o 
42360  439 
Toplevel.keep (Proof_Context.print_binds o Toplevel.context_of); 
9513  440 

35141  441 
val print_cases = Toplevel.unknown_context o 
42360  442 
Toplevel.keep (Proof_Context.print_cases o Toplevel.context_of); 
5831  443 

444 

19268  445 
(* print theorems, terms, types etc. *) 
446 

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

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

448 

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

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

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

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

452 
> Pretty.chunks2 > Pretty.string_of; 
5880  453 

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

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

455 
Pretty.string_of (Display.pretty_thms ctxt (Attrib.eval_thms ctxt args)); 
5895  456 

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

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

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

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

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

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

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

467 
in 
33388  468 
Proof_Syntax.pretty_proof ctxt 
17066  469 
(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

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

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

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

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

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

475 

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

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

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

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

480 
in Pretty.string_of (Pretty.quote (Syntax.pretty_term ctxt' prop)) end; 
5831  481 

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

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

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

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

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

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

490 
Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' T)]) 
9128  491 
end; 
5831  492 

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

493 
fun string_of_type ctxt s = 
6e72f31999ac
prefer plain Attrib.eval_thms with plain Proof.context instead of Proof.state;
wenzelm
parents:
38139
diff
changeset

494 
let val T = Syntax.read_typ ctxt s 
24920  495 
in Pretty.string_of (Pretty.quote (Syntax.pretty_typ ctxt T)) end; 
9128  496 

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

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

499 

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

500 
in 
9128  501 

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

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

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

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

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

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

507 
val print_type = print_item (string_of_type o Toplevel.context_of); 
5831  508 

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

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

510 

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

511 

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

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

513 

30367  514 
fun check_text (txt, pos) state = 
39507
839873937ddd
tuned signature of (Context_)Position.report variants;
wenzelm
parents:
39165
diff
changeset

515 
(Position.report pos Markup.doc_source; 
37216
3165bc303f66
modernized some structure names, keeping a few legacy aliases;
wenzelm
parents:
37198
diff
changeset

516 
ignore (Thy_Output.eval_antiquote (#1 (Keyword.get_lexicons ())) state (txt, pos))); 
12953
7d5bd53555d8
markup commands: proper theory/proof transactions!
wenzelm
parents:
12938
diff
changeset

517 

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

518 
fun header_markup txt = Toplevel.keep (fn state => 
30367  519 
if Toplevel.is_toplevel state then check_text txt state 
27853
916038f77be6
simplified markup commands  removed obsolete Present.results, always check text;
wenzelm
parents:
27730
diff
changeset

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

521 

30367  522 
fun local_theory_markup (loc, txt) = Toplevel.present_local_theory loc (check_text txt); 
523 
val proof_markup = Toplevel.present_proof o check_text; 

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

524 

5831  525 
end; 