author  berghofe 
Tue, 25 Mar 2003 10:03:11 +0100  
changeset 13884  5affbaee6b18 
parent 13801  6c5c5bdfae84 
child 14557  31ae4a47267c 
permissions  rwrr 
12780  1 
(* Title: Pure/proof_general.ML 
12778  2 
ID: $Id$ 
3 
Author: Markus Wenzel, TU Muenchen 

4 
License: GPL (GNU GENERAL PUBLIC LICENSE) 

5 

6 
Isabelle configuration for Proof General (see http://www.proofgeneral.org). 

7 
*) 

8 

9 
signature PROOF_GENERAL = 

10 
sig 

11 
val setup: (theory > theory) list 

12 
val update_thy_only: string > unit 

13 
val try_update_thy_only: string > unit 

13391  14 
val inform_file_retracted: string > unit 
12778  15 
val inform_file_processed: string > unit 
13728
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset

16 
val options: (string * (string * (string * (unit > string) * (string > unit)))) list ref 
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset

17 
val process_pgip: string > unit 
12778  18 
val thms_containing: string list > unit 
19 
val help: unit > unit 

20 
val show_context: unit > theory 

21 
val kill_goal: unit > unit 

22 
val repeat_undo: int > unit 

23 
val isa_restart: unit > unit 

12833  24 
val full_proofs: bool > unit 
12778  25 
val init: bool > unit 
26 
val write_keywords: string > unit 

27 
end; 

28 

29 
structure ProofGeneral: PROOF_GENERAL = 

30 
struct 

31 

32 
(* print modes *) 

33 

34 
val proof_generalN = "ProofGeneral"; 

35 
val xsymbolsN = "xsymbols"; 

13538  36 
val thm_depsN = "thm_deps"; 
12778  37 

13728
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset

38 

8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset

39 
val pgml_version_supported = "1.0"; 
12778  40 
val pgmlN = "PGML"; 
41 
fun pgml () = pgmlN mem_string ! print_mode; 

42 

43 

44 
(* text output *) 

45 

46 
local 

47 

48 
fun xsymbols_output s = 

49 
if xsymbolsN mem_string ! print_mode andalso exists_string (equal "\\") s then 

50 
let val syms = Symbol.explode s 

51 
in (implode (map (fn "\\" => "\\\\"  c => c) syms), real (Symbol.length syms)) end 

52 
else (s, real (size s)); 

53 

54 
fun pgml_output (s, len) = 

55 
if pgml () then (XML.text s, len) 

56 
else (s, len); 

57 

58 
in 

59 

60 
fun setup_xsymbols_output () = 

61 
Symbol.add_mode proof_generalN (pgml_output o xsymbols_output, Symbol.default_indent); 

62 

63 
end; 

64 

65 

66 
(* token translations *) 

67 

68 
local 

69 

70 
val end_tag = oct_char "350"; 

71 
val class_tag = ("class", oct_char "351"); 

72 
val tfree_tag = ("tfree", oct_char "352"); 

73 
val tvar_tag = ("tvar", oct_char "353"); 

74 
val free_tag = ("free", oct_char "354"); 

75 
val bound_tag = ("bound", oct_char "355"); 

76 
val var_tag = ("var", oct_char "356"); 

77 
val skolem_tag = ("skolem", oct_char "357"); 

78 

79 
fun xml_atom kind x = XML.element "atom" [("kind", kind)] [XML.text x]; 

80 

81 
fun tagit (kind, bg_tag) x = 

82 
(if pgml () then xml_atom kind x else bg_tag ^ x ^ end_tag, 

83 
real (Symbol.length (Symbol.explode x))); 

84 

85 
fun free_or_skolem x = 

86 
(case try Syntax.dest_skolem x of 

87 
None => tagit free_tag x 

88 
 Some x' => tagit skolem_tag x'); 

89 

90 
fun var_or_skolem s = 

91 
(case Syntax.read_var s of 

92 
Var ((x, i), _) => 

93 
(case try Syntax.dest_skolem x of 

94 
None => tagit var_tag s 

95 
 Some x' => tagit skolem_tag (Syntax.string_of_vname (x', i))) 

96 
 _ => tagit var_tag s); 

97 

98 
val proof_general_trans = 

99 
Syntax.tokentrans_mode proof_generalN 

100 
[("class", tagit class_tag), 

101 
("tfree", tagit tfree_tag), 

102 
("tvar", tagit tvar_tag), 

103 
("free", free_or_skolem), 

104 
("bound", tagit bound_tag), 

105 
("var", var_or_skolem)]; 

106 

107 
in val setup = [Theory.add_tokentrfuns proof_general_trans] end; 

108 

109 

110 

111 
(* messages and notification *) 

112 

113 
local 

114 

115 
fun decorated_output bg en prfx = 

116 
writeln_default o enclose bg en o prefix_lines prfx; 

117 

118 
fun message kind bg en prfx s = 

119 
if pgml () then writeln_default (XML.element kind [] [prefix_lines prfx s]) 

120 
else decorated_output bg en prfx s; 

121 

13526  122 
in 
12778  123 

13526  124 
val notify = message "notify" (oct_char "360") (oct_char "361") ""; 
12778  125 

126 
fun setup_messages () = 

127 
(writeln_fn := message "output" "" "" ""; 

128 
priority_fn := message "information" (oct_char "360") (oct_char "361") ""; 

129 
tracing_fn := message "tracing" (oct_char "360" ^ oct_char "375") (oct_char "361") ""; 

130 
warning_fn := message "warning" (oct_char "362") (oct_char "363") "### "; 

131 
error_fn := message "error" (oct_char "364") (oct_char "365") "*** "); 

132 

133 
fun tell_clear_goals () = notify "Proof General, please clear the goals buffer."; 

134 
fun tell_clear_response () = notify "Proof General, please clear the response buffer."; 

135 
fun tell_file msg path = notify ("Proof General, " ^ msg ^ " " ^ quote (File.sysify_path path)); 

136 

137 
end; 

138 

139 

140 
(* theory / proof state output *) 

141 

142 
local 

143 

144 
fun tmp_markers f = 

145 
setmp Display.current_goals_markers (oct_char "366", oct_char "367", "") f (); 

146 

147 
fun statedisplay prts = 

148 
writeln_default (XML.element "statedisplay" [] [Pretty.string_of (Pretty.chunks prts)]); 

149 

150 
fun print_current_goals n m st = 

151 
if pgml () then statedisplay (Display.pretty_current_goals n m st) 

152 
else tmp_markers (fn () => Display.print_current_goals_default n m st); 

153 

154 
fun print_state b st = 

155 
if pgml () then statedisplay (Toplevel.pretty_state b st) 

156 
else tmp_markers (fn () => Toplevel.print_state_default b st); 

157 

158 
in 

159 

160 
fun setup_state () = 

161 
(Display.print_current_goals_fn := print_current_goals; 

162 
Toplevel.print_state_fn := print_state; 

163 
Toplevel.prompt_state_fn := (suffix (oct_char "372") o Toplevel.prompt_state_default)); 

164 

165 
end; 

166 

167 

13538  168 
(* theorem dependency output *) 
13526  169 

170 
local 

171 

13545  172 
val spaces_quote = space_implode " " o map quote; 
173 

13526  174 
fun tell_thm_deps ths = 
13538  175 
conditional (thm_depsN mem_string ! print_mode) (fn () => 
176 
let 

13545  177 
val names = map Thm.name_of_thm ths \ ""; 
178 
val deps = Symtab.keys (foldl (uncurry Proofterm.thms_of_proof) 

179 
(Symtab.empty, map Thm.proof_of ths)) \ ""; 

13538  180 
in 
13545  181 
if null names orelse null deps then () 
182 
else notify ("Proof General, theorem dependencies of " ^ spaces_quote names ^ " are " 

183 
^ spaces_quote deps) 

13538  184 
end); 
13526  185 

186 
in 

187 

188 
fun setup_present_hook () = 

189 
Present.add_hook (fn _ => fn res => tell_thm_deps (flat (map #2 res))); 

190 

191 
end; 

192 

193 

12778  194 
(* theory loader actions *) 
195 

196 
local 

197 

198 
fun add_master_files name files = 

199 
let val masters = [ThyLoad.thy_path name, ThyLoad.ml_path name] 

200 
in masters @ gen_rems (op = o pairself Path.base) (files, masters) end; 

201 

202 
fun trace_action action name = 

203 
if action = ThyInfo.Update then 

204 
seq (tell_file "this file is loaded:") (ThyInfo.loaded_files name) 

205 
else if action = ThyInfo.Outdate orelse action = ThyInfo.Remove then 

206 
seq (tell_file "you can unlock the file") (add_master_files name (ThyInfo.loaded_files name)) 

207 
else (); 

208 

209 
in 

210 
fun setup_thy_loader () = ThyInfo.add_hook trace_action; 

211 
fun sync_thy_loader () = seq (trace_action ThyInfo.Update) (ThyInfo.names ()); 

212 
end; 

213 

214 

215 
(* prepare theory context *) 

216 

217 
val thy_name = Path.pack o Path.drop_ext o Path.base o Path.unpack; 

218 
val update_thy_only = setmp MetaSimplifier.trace_simp false ThyInfo.update_thy_only; 

219 

220 
fun which_context () = 

221 
(case Context.get_context () of 

222 
Some thy => " Using current (dynamic!) one: " ^ 

223 
(case try PureThy.get_name thy of Some name => quote name  None => "<unnamed>") 

224 
 None => ""); 

225 

226 
fun try_update_thy_only file = 

227 
ThyLoad.cond_add_path (Path.dir (Path.unpack file)) (fn () => 

228 
let val name = thy_name file in 

229 
if is_some (ThyLoad.check_file (ThyLoad.thy_path name)) then update_thy_only name 

230 
else warning ("Unkown theory context of ML file." ^ which_context ()) 

231 
end) (); 

232 

233 

234 
(* get informed about files *) 

235 

13391  236 
val inform_file_retracted = ThyInfo.if_known_thy ThyInfo.remove_thy o thy_name; 
237 
val inform_file_processed = ThyInfo.if_known_thy ThyInfo.touch_child_thys o thy_name; 

12778  238 

239 
fun proper_inform_file_processed file state = 

240 
let val name = thy_name file in 

13391  241 
ThyInfo.if_known_thy ThyInfo.touch_child_thys name; 
12778  242 
if not (Toplevel.is_toplevel state) then 
243 
warning ("Not at toplevel  cannot register theory " ^ quote name) 

244 
else Library.transform_error ThyInfo.pretend_use_thy_only name handle ERROR_MESSAGE msg => 

245 
(warning msg; warning ("Failed to register theory " ^ quote name)) 

246 
end; 

247 

248 

13728
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset

249 
(* options *) 
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset

250 

8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset

251 
fun nat_option r = ("nat", 
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset

252 
(fn () => string_of_int (!r)), 
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset

253 
(fn s => (case Syntax.read_nat s of 
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset

254 
None => error "nat_option: illegal value" 
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset

255 
 Some i => r := i))); 
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset

256 

8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset

257 
fun bool_option r = ("boolean", 
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset

258 
(fn () => Bool.toString (!r)), 
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset

259 
(fn "false" => r := false  "true" => r := true 
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset

260 
 _ => error "bool_option: illegal value")); 
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset

261 

8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset

262 
val proof_option = ("boolean", 
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset

263 
(fn () => Bool.toString (!proofs >= 2)), 
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset

264 
(fn "false" => proofs := 1  "true" => proofs := 2 
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset

265 
 _ => error "proof_option: illegal value")); 
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset

266 

8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset

267 
val thm_deps_option = ("boolean", 
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset

268 
(fn () => Bool.toString ("thm_deps" mem !print_mode)), 
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset

269 
(fn "false" => print_mode := Library.gen_rems (op =) (!print_mode, ["thm_deps"]) 
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset

270 
 "true" => print_mode := (["thm_deps"] @ !print_mode) 
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset

271 
 _ => error "thm_deps_option: illegal value")); 
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset

272 

8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset

273 
val print_depth_option = ("nat", 
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset

274 
(fn () => "10"), 
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset

275 
(fn s => (case Syntax.read_nat s of 
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset

276 
None => error "print_depth_option: illegal value" 
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset

277 
 Some i => print_depth i))); 
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset

278 

8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset

279 
val options = ref 
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset

280 
[("showtypes", ("Whether to show types in Isabelle.", 
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset

281 
bool_option show_types)), 
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset

282 
("showsorts", ("Whether to show sorts in Isabelle.", 
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset

283 
bool_option show_sorts)), 
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset

284 
("showconsts", ("Whether to show types of consts in Isabelle goals.", 
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset

285 
bool_option show_consts)), 
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset

286 
("longnames", ("Whether to show fully qualified names in Isabelle.", 
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset

287 
bool_option long_names)), 
13884  288 
("showbrackets", ("Whether to show full bracketing in Isabelle.", 
289 
bool_option show_brackets)), 

13728
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset

290 
("etacontract", ("Whether to print terms etacontracted in Isabelle.", 
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset

291 
bool_option Syntax.eta_contract)), 
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset

292 
("tracesimplifier", ("Whether to trace the Simplifier in Isabelle.", 
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset

293 
bool_option trace_simp)), 
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset

294 
("tracerules", ("Whether to trace the standard rules in Isabelle.", 
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset

295 
bool_option trace_rules)), 
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset

296 
("quickanddirty", ("Whether to take a few short cuts occasionally.", 
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset

297 
bool_option quick_and_dirty)), 
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset

298 
("fullproofs", ("Whether to record full proof objects internally.", 
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset

299 
proof_option)), 
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset

300 
("traceunification", ("Whether to output error diagnostics during unification.", 
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset

301 
bool_option Pattern.trace_unify_fail)), 
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset

302 
("showmaingoal", ("Whether to show main goal.", 
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset

303 
bool_option Proof.show_main_goal)), 
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset

304 
("globaltiming", ("Whether to enable timing in Isabelle.", 
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset

305 
bool_option Library.timing)), 
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset

306 
("theoremdependencies", ("Whether to track theorem dependencies within Proof General.", 
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset

307 
thm_deps_option)), 
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset

308 
("goalslimit", ("Setting for maximum number of goals printed in Isabelle.", 
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset

309 
nat_option goals_limit)), 
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset

310 
("premslimit", ("Setting for maximum number of premises printed in Isabelle/Isar.", 
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset

311 
nat_option ProofContext.prems_limit)), 
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset

312 
("printdepth", ("Setting for the ML print depth in Isabelle.", 
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset

313 
print_depth_option))]; 
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset

314 

8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset

315 

8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset

316 
(* Sending PGIP commands to the interface *) 
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset

317 

8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset

318 
fun issue_pgip pgips = notify (XML.element "pgip" [] pgips); 
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset

319 

8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset

320 
fun usespgml () = 
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset

321 
issue_pgip [XML.element "usespgml" [("version", pgml_version_supported)] []]; 
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset

322 

8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset

323 
(* NB: the default returned here is actually the current value, so 
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset

324 
repeated uses of <askprefs> will not work correctly. *) 
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset

325 
fun show_options () = issue_pgip (map 
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset

326 
(fn (name, (descr, (ty, get, _))) => (XML.element "haspref" 
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset

327 
[("type", ty), ("descr", descr), ("default", get ())] [name])) (!options)); 
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset

328 

8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset

329 
fun set_option name value = (case assoc (!options, name) of 
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset

330 
None => warning ("Unknown option: " ^ quote name) 
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset

331 
 Some (_, (_, _, set)) => set value); 
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset

332 

8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset

333 
fun get_option name = (case assoc (!options, name) of 
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset

334 
None => warning ("Unknown option: " ^ quote name) 
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset

335 
 Some (_, (_, get, _)) => 
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset

336 
issue_pgip [XML.element "prefval" [("name", name)] [get ()]]); 
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset

337 

8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset

338 

8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset

339 
(* Processing PGIP commands from the interface *) 
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset

340 

8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset

341 
(* FIXME: matching on attributes is a bit too strict here *) 
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset

342 

8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset

343 
fun process_pgip_element pgip = (case pgip of 
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset

344 
XML.Elem ("askpgml", _, []) => usespgml () 
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset

345 
 XML.Elem ("askprefs", _, []) => show_options () 
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset

346 
 XML.Elem ("getpref", [("name", name)], []) => get_option name 
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset

347 
 XML.Elem ("setpref", [("name", name)], [XML.Text value]) => 
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset

348 
set_option name value 
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset

349 
 XML.Elem (e, _, _) => warning ("Unrecognized PGIP command: " ^ e) 
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset

350 
 XML.Text t => warning ("Unrecognized PGIP command:\n" ^ t)); 
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset

351 

8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset

352 
fun process_pgip s = (case XML.tree_of_string s of 
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset

353 
XML.Elem ("pgip", _, pgips) => seq process_pgip_element pgips 
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset

354 
 _ => warning ("Invalid PGIP packet received\n" ^ s)); 
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset

355 

8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset

356 

12778  357 
(* misc commands for ProofGeneral/isa *) 
358 

359 
fun thms_containing ss = 

13284  360 
ProofContext.print_thms_containing (ProofContext.init (the_context ())) None ss; 
12778  361 

362 
val welcome = priority o Session.welcome; 

363 
val help = welcome; 

364 
val show_context = Context.the_context; 

365 

366 
fun kill_goal () = (Goals.reset_goals (); tell_clear_goals ()); 

367 

368 
fun no_print_goals f = setmp Display.print_current_goals_fn (fn _ => fn _ => fn _ => ()) f; 

369 

370 
fun repeat_undo 0 = () 

371 
 repeat_undo 1 = undo () 

372 
 repeat_undo n = (no_print_goals undo (); repeat_undo (n  1)); 

373 

374 

375 
(* restart toplevel loop (keeps most state information) *) 

376 

377 
local 

378 

379 
fun restart isar = 

380 
(if isar then tell_clear_goals () else kill_goal (); 

381 
tell_clear_response (); 

382 
welcome ()); 

383 

384 
in 

385 

386 
fun isa_restart () = restart false; 

387 
fun isar_restart () = (sync_thy_loader (); restart true; raise Toplevel.RESTART); 

388 

389 
end; 

390 

391 

12833  392 
fun full_proofs true = proofs := 2 
393 
 full_proofs false = proofs := 1; 

394 

395 

12778  396 
(* outer syntax *) 
397 

398 
local structure P = OuterParse and K = OuterSyntax.Keyword in 

399 

400 
val old_undoP = (*same name for compatibility with PG/Isabelle99*) 

401 
OuterSyntax.improper_command "undo" "undo last command (no output)" K.control 

402 
(Scan.succeed (Toplevel.no_timing o IsarCmd.undo)); 

403 

404 
val undoP = 

405 
OuterSyntax.improper_command "ProofGeneral.undo" "(internal)" K.control 

406 
(Scan.succeed (Toplevel.no_timing o IsarCmd.undo)); 

407 

408 
val context_thy_onlyP = 

409 
OuterSyntax.improper_command "ProofGeneral.context_thy_only" "(internal)" K.control 

410 
(P.name >> (Toplevel.no_timing oo IsarThy.init_context update_thy_only)); 

411 

412 
val try_context_thy_onlyP = 

413 
OuterSyntax.improper_command "ProofGeneral.try_context_thy_only" "(internal)" K.control 

414 
(P.name >> (Toplevel.no_timing oo 

415 
(Toplevel.imperative (K ()) oo IsarThy.init_context try_update_thy_only))); 

416 

417 
val restartP = 

418 
OuterSyntax.improper_command "ProofGeneral.restart" "(internal)" K.control 

419 
(P.opt_unit >> (Toplevel.no_timing oo K (Toplevel.imperative isar_restart))); 

420 

421 
val kill_proofP = 

422 
OuterSyntax.improper_command "ProofGeneral.kill_proof" "(internal)" K.control 

423 
(Scan.succeed (Toplevel.no_timing o IsarCmd.kill_proof_notify tell_clear_goals)); 

424 

425 
val inform_file_processedP = 

426 
OuterSyntax.improper_command "ProofGeneral.inform_file_processed" "(internal)" K.control 

427 
(P.name >> (Toplevel.no_timing oo 

428 
(fn name => Toplevel.keep (proper_inform_file_processed name)))); 

429 

430 
val inform_file_retractedP = 

431 
OuterSyntax.improper_command "ProofGeneral.inform_file_retracted" "(internal)" K.control 

432 
(P.name >> (Toplevel.no_timing oo 

433 
(fn name => Toplevel.imperative (fn () => inform_file_retracted name)))); 

434 

435 
fun init_outer_syntax () = OuterSyntax.add_parsers 

436 
[old_undoP, undoP, restartP, kill_proofP, context_thy_onlyP, try_context_thy_onlyP, 

437 
inform_file_processedP, inform_file_retractedP]; 

438 

439 
end; 

440 

441 

442 
(* init *) 

443 

444 
val initialized = ref false; 

445 

446 
fun init isar = 

447 
(conditional (not (! initialized)) (fn () => 

448 
(if isar then setmp warning_fn (K ()) init_outer_syntax () else (); 

449 
setup_xsymbols_output (); 

450 
setup_messages (); 

451 
setup_state (); 

452 
setup_thy_loader (); 

13526  453 
setup_present_hook (); 
12778  454 
set initialized; ())); 
455 
sync_thy_loader (); 

456 
print_mode := proof_generalN :: (! print_mode \ proof_generalN); 

457 
set quick_and_dirty; 

458 
ThmDeps.enable (); 

459 
if isar then ml_prompts "ML> " "ML# " 

460 
else ml_prompts ("> " ^ oct_char "372") (" " ^ oct_char "373"); 

461 
if isar then (welcome (); Isar.sync_main ()) else isa_restart ()); 

462 

463 

464 

465 
(** generate keyword classification file **) 

466 

467 
local 

468 

469 
val regexp_meta = explode ".*+?[]^$"; 

470 
val regexp_quote = implode o map (fn c => if c mem regexp_meta then "\\\\" ^ c else c) o explode; 

471 

472 
fun defconst name strs = 

473 
"\n(defconst isarkeywords" ^ name ^ 

474 
"\n '(" ^ space_implode "\n " (map (quote o regexp_quote) strs) ^ "))\n"; 

475 

476 
fun make_elisp_commands commands kind = 

477 
defconst kind (mapfilter (fn (c, _, k, _) => if k = kind then Some c else None) commands); 

478 

479 
fun make_elisp_syntax (keywords, commands) = 

480 
";;\n\ 

481 
\;; Keyword classification tables for Isabelle/Isar.\n\ 

482 
\;; This file was generated by " ^ Session.name () ^ "  DO NOT EDIT!\n\ 

483 
\;;\n\ 

484 
\;; $" ^ "Id$\n\ 

485 
\;;\n" ^ 

486 
defconst "major" (map #1 commands) ^ 

487 
defconst "minor" (filter Syntax.is_identifier keywords) ^ 

488 
implode (map (make_elisp_commands commands) OuterSyntax.Keyword.kinds) ^ 

489 
"\n(provide 'isarkeywords)\n"; 

490 

491 
in 

492 

493 
fun write_keywords s = 

494 
(init_outer_syntax (); 

495 
File.write (Path.unpack ("isarkeywords" ^ (if s = "" then "" else "" ^ s) ^".el")) 

496 
(make_elisp_syntax (OuterSyntax.dest_keywords (), OuterSyntax.dest_parsers ()))); 

497 

498 
end; 

499 

500 

501 
end; 

502 

503 
(*a hack for Proof General 3.2 to avoid problems with escapes in ML commands*) 

504 
infix \\\\ val op \\\\ = op \\; 