author  wenzelm 
Wed, 21 Jul 2010 15:23:46 +0200  
changeset 37870  dd9cfc512b7f 
parent 37866  cd1d1bc7684c 
child 37949  48a874444164 
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 

30573  16 
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

17 
val add_axioms: (Attrib.binding * string) list > theory > theory 
29579  18 
val add_defs: (bool * bool) * ((binding * string) * Attrib.src list) list > theory > theory 
33456
fbd47f9b9b12
allow "pervasive" local theory declarations, which are applied the background theory;
wenzelm
parents:
33391
diff
changeset

19 
val declaration: bool > Symbol_Pos.text * Position.T > local_theory > local_theory 
30575  20 
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

21 
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

22 
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

23 
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

24 
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

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

26 
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

27 
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

28 
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

29 
val thus: (Attrib.binding * (string * string list) list) list > bool > Proof.state > Proof.state 
21350  30 
val qed: Method.text option > Toplevel.transition > Toplevel.transition 
31 
val terminal_proof: Method.text * Method.text option > 

32 
Toplevel.transition > Toplevel.transition 

33 
val default_proof: Toplevel.transition > Toplevel.transition 

34 
val immediate_proof: Toplevel.transition > Toplevel.transition 

35 
val done_proof: Toplevel.transition > Toplevel.transition 

36 
val skip_proof: Toplevel.transition > Toplevel.transition 

27574
4adce8310643
renamed theory to init_theory, removed obsolete kill argument;
wenzelm
parents:
27562
diff
changeset

37 
val init_theory: string * string list * (string * bool) list > 
4adce8310643
renamed theory to init_theory, removed obsolete kill argument;
wenzelm
parents:
27562
diff
changeset

38 
Toplevel.transition > Toplevel.transition 
5831  39 
val exit: Toplevel.transition > Toplevel.transition 
40 
val quit: Toplevel.transition > Toplevel.transition 

9731  41 
val pr: string list * (int option * int option) > Toplevel.transition > Toplevel.transition 
8453  42 
val disable_pr: Toplevel.transition > Toplevel.transition 
43 
val enable_pr: Toplevel.transition > Toplevel.transition 

30575  44 
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

45 
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

46 
val diag_goal: unit > {context: Proof.context, facts: thm list, goal: thm} 
14950  47 
val cd: Path.T > Toplevel.transition > Toplevel.transition 
5831  48 
val pwd: Toplevel.transition > Toplevel.transition 
14950  49 
val display_drafts: Path.T list > Toplevel.transition > Toplevel.transition 
50 
val print_drafts: Path.T list > Toplevel.transition > Toplevel.transition 

7124  51 
val pretty_setmargin: int > Toplevel.transition > Toplevel.transition 
7308  52 
val print_context: Toplevel.transition > Toplevel.transition 
20621  53 
val print_theory: bool > Toplevel.transition > Toplevel.transition 
5831  54 
val print_syntax: Toplevel.transition > Toplevel.transition 
21725  55 
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

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

58 
val print_theorems: bool > Toplevel.transition > Toplevel.transition 
12060  59 
val print_locales: Toplevel.transition > Toplevel.transition 
29223  60 
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

61 
val print_registrations: string > Toplevel.transition > Toplevel.transition 
5831  62 
val print_attributes: Toplevel.transition > Toplevel.transition 
16026  63 
val print_simpset: Toplevel.transition > Toplevel.transition 
12382  64 
val print_rules: Toplevel.transition > Toplevel.transition 
9219  65 
val print_trans_rules: Toplevel.transition > Toplevel.transition 
5831  66 
val print_methods: Toplevel.transition > Toplevel.transition 
9219  67 
val print_antiquotations: Toplevel.transition > Toplevel.transition 
20574  68 
val class_deps: Toplevel.transition > Toplevel.transition 
22485  69 
val thy_deps: Toplevel.transition > Toplevel.transition 
26336
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26186
diff
changeset

70 
val thm_deps: (Facts.ref * Attrib.src list) list > Toplevel.transition > Toplevel.transition 
26184  71 
val unused_thms: (string list * string list option) option > 
72 
Toplevel.transition > Toplevel.transition 

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

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

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

79 
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

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

81 
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

82 
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

83 
val print_type: (string list * string) > Toplevel.transition > Toplevel.transition 
30573  84 
val header_markup: Symbol_Pos.text * Position.T > Toplevel.transition > Toplevel.transition 
85 
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

86 
Toplevel.transition > Toplevel.transition 
30573  87 
val proof_markup: Symbol_Pos.text * Position.T > Toplevel.transition > Toplevel.transition 
5831  88 
end; 
89 

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

90 
structure Isar_Cmd: ISAR_CMD = 
5831  91 
struct 
92 

93 

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

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

95 

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

97 

30461  98 
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

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: theory > theory" "Context.map_theory setup" 
26435  101 
> Context.theory_map; 
22116
6917be2e647d
added various ML setup functions (from sign.ML, pure_thy.ML);
wenzelm
parents:
22087
diff
changeset

102 

30461  103 
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

104 
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

105 
> ML_Context.expression pos "val setup: local_theory > local_theory" "Context.map_proof setup" 
30461  106 
> Context.proof_map; 
107 

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

108 

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

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

112 

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

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

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

115 

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

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

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

118 

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

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

120 

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

121 
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

122 
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

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

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

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

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

128 

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

129 
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

130 
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

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

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

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

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

136 

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

137 
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

138 
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

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

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

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

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

144 

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

145 
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

146 
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

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

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

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

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

152 

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

153 
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

154 
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

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

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

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

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

160 

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

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

162 

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

163 

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

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

165 

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

167 
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

168 
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

169 
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

170 
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

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

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

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

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

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

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

177 
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

178 

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

179 

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

180 
(* oldstyle axioms *) 
21350  181 

35894  182 
val add_axioms = fold (snd oo Specification.axiom_cmd); 
21350  183 

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

184 
fun add_defs ((unchecked, overloaded), args) thy = 
4e3fe0b8687b
minor renovation of oldstyle 'axioms'  make it an alias of iterated 'axiomatization';
wenzelm
parents:
35141
diff
changeset

185 
thy > (if unchecked then PureThy.add_defs_unchecked_cmd else PureThy.add_defs_cmd) overloaded 
4e3fe0b8687b
minor renovation of oldstyle 'axioms'  make it an alias of iterated 'axiomatization';
wenzelm
parents:
35141
diff
changeset

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

187 
> snd; 
21350  188 

189 

22087  190 
(* declarations *) 
191 

33456
fbd47f9b9b12
allow "pervasive" local theory declarations, which are applied the background theory;
wenzelm
parents:
33391
diff
changeset

192 
fun declaration 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

193 
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

194 
> ML_Context.expression pos 
26455  195 
"val declaration: Morphism.declaration" 
33671  196 
("Context.map_proof (Local_Theory.declaration " ^ Bool.toString pervasive ^ " declaration)") 
26385
ae7564661e76
ML runtime compilation: pass position, tuned signature;
wenzelm
parents:
26336
diff
changeset

197 
> Context.proof_map; 
22087  198 

199 

22202  200 
(* simprocs *) 
201 

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

203 
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

204 
> ML_Context.expression pos 
22239  205 
"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

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

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

208 
\identifier = Library.maps ML_Context.thms " ^ ML_Syntax.print_strings identifier ^ "})") 
22202  209 
> Context.proof_map; 
210 

211 

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

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

213 

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

214 
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

215 
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

216 
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

217 
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

218 
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

219 
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

220 
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

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

222 

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

223 
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

224 
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

225 
val hide_const = hide_names Sign.intern_const Sign.declared_const Sign.hide_const; 
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 
val hide_fact = hide_names PureThy.intern_fact PureThy.defined_fact PureThy.hide_fact; 
26671
c95590e01df5
added hide_names command (formerly Sign.hide_names), support fact name space;
wenzelm
parents:
26626
diff
changeset

227 

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

228 

21350  229 
(* goals *) 
230 

231 
fun goal opt_chain goal stmt int = 

29383  232 
opt_chain #> goal NONE (K I) stmt int; 
21350  233 

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

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

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

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

237 
val thus = goal Proof.chain Proof.show_cmd; 
21350  238 

239 

240 
(* local endings *) 

241 

29383  242 
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

243 
val local_terminal_proof = Toplevel.proof' o Proof.local_future_terminal_proof; 
29383  244 
val local_default_proof = Toplevel.proof Proof.local_default_proof; 
245 
val local_immediate_proof = Toplevel.proof Proof.local_immediate_proof; 

246 
val local_done_proof = Toplevel.proof Proof.local_done_proof; 

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

21350  248 

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

251 

252 
(* global endings *) 

253 

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

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

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

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

258 
val global_skip_proof = Toplevel.end_proof Proof.global_skip_proof; 

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

260 

28375  261 
val skip_global_qed = Toplevel.skip_proof_to_theory (fn n => n = 1); 
21350  262 

263 

264 
(* common endings *) 

265 

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

267 
fun terminal_proof m = local_terminal_proof m o global_terminal_proof m; 

268 
val default_proof = local_default_proof o global_default_proof; 

269 
val immediate_proof = local_immediate_proof o global_immediate_proof; 

270 
val done_proof = local_done_proof o global_done_proof; 

271 
val skip_proof = local_skip_proof o global_skip_proof; 

272 

273 

274 
(* init and exit *) 

275 

27574
4adce8310643
renamed theory to init_theory, removed obsolete kill argument;
wenzelm
parents:
27562
diff
changeset

276 
fun init_theory (name, imports, uses) = 
37216
3165bc303f66
modernized some structure names, keeping a few legacy aliases;
wenzelm
parents:
37198
diff
changeset

277 
Toplevel.init_theory name (Thy_Info.begin_theory name imports (map (apfst Path.explode) uses)) 
27574
4adce8310643
renamed theory to init_theory, removed obsolete kill argument;
wenzelm
parents:
27562
diff
changeset

278 
(fn thy => 
37216
3165bc303f66
modernized some structure names, keeping a few legacy aliases;
wenzelm
parents:
37198
diff
changeset

279 
if Thy_Info.check_known_thy (Context.theory_name thy) 
3165bc303f66
modernized some structure names, keeping a few legacy aliases;
wenzelm
parents:
37198
diff
changeset

280 
then Thy_Info.end_theory thy else ()); 
21350  281 

5831  282 
val exit = Toplevel.keep (fn state => 
26599  283 
(Context.set_thread_data (try Toplevel.generic_theory_of state); 
24071  284 
raise Toplevel.TERMINATE)); 
5831  285 

286 
val quit = Toplevel.imperative quit; 

287 

7101  288 

8453  289 
(* print state *) 
290 

15531  291 
fun set_limit _ NONE = () 
292 
 set_limit r (SOME n) = r := n; 

9731  293 

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

294 
fun pr (modes, (lim1, lim2)) = Toplevel.keep (fn state => 
9731  295 
(set_limit goals_limit lim1; set_limit ProofContext.prems_limit lim2; Toplevel.quiet := false; 
37146
f652333bbf8e
renamed structure PrintMode to Print_Mode, keeping the old name as legacy alias for some time;
wenzelm
parents:
36950
diff
changeset

296 
Print_Mode.with_modes modes (Toplevel.print_state true) state)); 
8453  297 

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

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

300 

301 

26489  302 
(* diagnostic ML evaluation *) 
5831  303 

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

304 
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

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

306 
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

307 
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

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

309 

26489  310 
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

311 
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

312 
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

313 
> 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

314 
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

315 

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

316 
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

317 

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

318 
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

319 
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

320 
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

321 

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

322 
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

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

325 

326 
(* current working directory *) 

327 

30805  328 
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

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

331 

14934  332 
(* present draft files *) 
333 

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

16258  335 
let val outfile = File.shell_path (Present.drafts (getenv "ISABELLE_DOC_FORMAT") files) 
31819  336 
in File.isabelle_tool "display" ("c " ^ outfile ^ " &"); () end); 
14934  337 

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

16258  339 
let val outfile = File.shell_path (Present.drafts "ps" files) 
31819  340 
in File.isabelle_tool "print" ("c " ^ outfile); () end); 
14934  341 

342 

7124  343 
(* pretty_setmargin *) 
344 

36745  345 
fun pretty_setmargin n = Toplevel.imperative (fn () => Pretty.margin_default := n); 
5831  346 

347 

9513  348 
(* print parts of theory and proof context *) 
5831  349 

7308  350 
val print_context = Toplevel.keep Toplevel.print_state_context; 
9513  351 

20621  352 
fun print_theory verbose = Toplevel.unknown_theory o 
33389  353 
Toplevel.keep (Pretty.writeln o Proof_Display.pretty_full_theory verbose o Toplevel.theory_of); 
9513  354 

21663  355 
val print_syntax = Toplevel.unknown_context o 
356 
Toplevel.keep (ProofContext.print_syntax o Toplevel.context_of); 

9513  357 

21725  358 
val print_abbrevs = Toplevel.unknown_context o 
359 
Toplevel.keep (ProofContext.print_abbrevs o Toplevel.context_of); 

360 

35141  361 
val print_facts = Toplevel.unknown_context o 
362 
Toplevel.keep (ProofContext.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

363 

35141  364 
val print_configs = Toplevel.unknown_context o 
365 
Toplevel.keep (Attrib.print_configs o Toplevel.context_of); 

23989  366 

35141  367 
val print_theorems_proof = 
368 
Toplevel.keep (ProofContext.print_lthms o Proof.context_of o Toplevel.proof_of); 

17066  369 

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

370 
fun print_theorems_theory verbose = Toplevel.keep (fn state => 
18588  371 
Toplevel.theory_of state > 
30801  372 
(case Toplevel.previous_context_of state of 
33515
d066e8369a33
print_theorems: suppress concealed (global) facts, unless "!" option is given;
wenzelm
parents:
33456
diff
changeset

373 
SOME prev => Proof_Display.print_theorems_diff verbose (ProofContext.theory_of prev) 
d066e8369a33
print_theorems: suppress concealed (global) facts, unless "!" option is given;
wenzelm
parents:
33456
diff
changeset

374 
 NONE => Proof_Display.print_theorems verbose)); 
18588  375 

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

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

377 
Toplevel.unknown_context o print_theorems_theory verbose o print_theorems_proof; 
9513  378 

12060  379 
val print_locales = Toplevel.unknown_theory o 
29360  380 
Toplevel.keep (Locale.print_locales o Toplevel.theory_of); 
12060  381 

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

382 
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

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

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

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

386 
Toplevel.keep (fn state => 
ca430e6aee1c
Propagation of mixins for interpretation; reactivated diagnostic command print_interps.
ballarin
parents:
32149
diff
changeset

387 
Locale.print_registrations (Toplevel.theory_of state) name); 
ca430e6aee1c
Propagation of mixins for interpretation; reactivated diagnostic command print_interps.
ballarin
parents:
32149
diff
changeset

388 

9513  389 
val print_attributes = Toplevel.unknown_theory o 
390 
Toplevel.keep (Attrib.print_attributes o Toplevel.theory_of); 

391 

16026  392 
val print_simpset = Toplevel.unknown_context o 
30357  393 
Toplevel.keep (fn state => 
394 
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

395 
in Pretty.writeln (Simplifier.pretty_ss ctxt (simpset_of ctxt)) end); 
16026  396 

12382  397 
val print_rules = Toplevel.unknown_context o 
33369  398 
Toplevel.keep (Context_Rules.print_rules o Toplevel.context_of); 
12382  399 

9513  400 
val print_trans_rules = Toplevel.unknown_context o 
18639  401 
Toplevel.keep (Calculation.print_rules o Toplevel.context_of); 
9513  402 

403 
val print_methods = Toplevel.unknown_theory o 

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

405 

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

406 
val print_antiquotations = Toplevel.imperative Thy_Output.print_antiquotations; 
5831  407 

22485  408 
val thy_deps = Toplevel.unknown_theory o Toplevel.keep (fn state => 
409 
let 

410 
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

411 
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

412 

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

413 
val all_thys = sort Thy_Info.thy_ord (thy :: Theory.ancestors_of thy); 
22604  414 
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

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

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

417 
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

418 
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

419 
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

420 
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

421 
in Present.display_graph gr end); 
22485  422 

20574  423 
val class_deps = Toplevel.unknown_theory o Toplevel.keep (fn state => 
424 
let 

425 
val thy = Toplevel.theory_of state; 

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

36328
4d9deabf6474
replaced Sorts.rep_algebra by slightly more abstract selectors classes_of/arities_of;
wenzelm
parents:
36323
diff
changeset

427 
val classes = Sorts.classes_of algebra; 
20574  428 
fun entry (c, (i, (_, cs))) = 
33095
bbd52d2f8696
renamed NameSpace to Name_Space  also to emphasize its subtle change in semantics;
wenzelm
parents:
32859
diff
changeset

429 
(i, {name = Name_Space.extern space c, ID = c, parents = cs, 
20574  430 
dir = "", unfold = true, path = ""}); 
431 
val gr = 

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

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

434 
in Present.display_graph gr end); 

435 

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

437 
Thm_Deps.thm_deps (Toplevel.theory_of state) 
dd9cfc512b7f
thm_deps/unused_thms: Context.get_theory based on proper theory ancestry, not accidental theory loader state;
wenzelm
parents:
37866
diff
changeset

438 
(Proof.get_thmss_cmd (Toplevel.enter_proof_body state) args)); 
9454  439 

5831  440 

26184  441 
(* find unused theorems *) 
442 

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

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

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

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

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

447 
fun pretty_thm (a, th) = ProofContext.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

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

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

451 
(case opt_range of 
26694  452 
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

453 
 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

454 
 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

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

456 
end); 
26184  457 

458 

5831  459 
(* print proof context contents *) 
460 

35141  461 
val print_binds = Toplevel.unknown_context o 
462 
Toplevel.keep (ProofContext.print_binds o Toplevel.context_of); 

9513  463 

35141  464 
val print_cases = Toplevel.unknown_context o 
465 
Toplevel.keep (ProofContext.print_cases o Toplevel.context_of); 

5831  466 

467 

19268  468 
(* print theorems, terms, types etc. *) 
469 

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

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

471 

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

472 
fun string_of_stmts state args = 
36323
655e2d74de3a
modernized naming conventions of main Isar proof elements;
wenzelm
parents:
36178
diff
changeset

473 
Proof.get_thmss_cmd state args 
21437  474 
> 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

475 
> Pretty.chunks2 > Pretty.string_of; 
5880  476 

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

477 
fun string_of_thms state args = 
36323
655e2d74de3a
modernized naming conventions of main Isar proof elements;
wenzelm
parents:
36178
diff
changeset

478 
Pretty.string_of (Display.pretty_thms (Proof.context_of state) (Proof.get_thmss_cmd state args)); 
5895  479 

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

480 
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

481 
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

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

484 
let 
33290  485 
val {context = ctxt, goal = thm} = Proof.simple_goal state; 
26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26599
diff
changeset

486 
val thy = ProofContext.theory_of ctxt; 
28814  487 
val prf = Thm.proof_of thm; 
17066  488 
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

489 
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

490 
in 
33388  491 
Proof_Syntax.pretty_proof ctxt 
17066  492 
(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

493 
end 
15531  494 
 SOME args => Pretty.chunks 
33388  495 
(map (Proof_Syntax.pretty_proof_of (Proof.context_of state) full) 
36323
655e2d74de3a
modernized naming conventions of main Isar proof elements;
wenzelm
parents:
36178
diff
changeset

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

497 

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

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

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

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

503 
in Pretty.string_of (Pretty.quote (Syntax.pretty_term ctxt' prop)) end; 
5831  504 

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

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

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

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

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

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

514 
Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' T)]) 
9128  515 
end; 
5831  516 

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

517 
fun string_of_type state s = 
5831  518 
let 
12055  519 
val ctxt = Proof.context_of state; 
25331  520 
val T = Syntax.read_typ ctxt s; 
24920  521 
in Pretty.string_of (Pretty.quote (Syntax.pretty_typ ctxt T)) end; 
9128  522 

23935  523 
fun print_item string_of (modes, arg) = Toplevel.keep (fn state => 
37146
f652333bbf8e
renamed structure PrintMode to Print_Mode, keeping the old name as legacy alias for some time;
wenzelm
parents:
36950
diff
changeset

524 
Print_Mode.with_modes modes (fn () => 
23935  525 
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

526 

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

527 
in 
9128  528 

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

530 
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

531 
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

532 
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

533 
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

534 
val print_type = print_item string_of_type; 
5831  535 

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

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

537 

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

538 

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

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

540 

30367  541 
fun check_text (txt, pos) state = 
27876  542 
(Position.report Markup.doc_source pos; 
37216
3165bc303f66
modernized some structure names, keeping a few legacy aliases;
wenzelm
parents:
37198
diff
changeset

543 
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

544 

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

545 
fun header_markup txt = Toplevel.keep (fn state => 
30367  546 
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

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

548 

30367  549 
fun local_theory_markup (loc, txt) = Toplevel.present_local_theory loc (check_text txt); 
550 
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

551 

5831  552 
end; 