refined theorem dependency output: previous state needs to contain a theory (not empty toplevel);
new_thms_deps: explicity theory values;
1 (* Title: Pure/ProofGeneral/proof_general_pgip.ML
3 Author: David Aspinall and Markus Wenzel
5 Isabelle configuration for Proof General using PGIP protocol.
6 See http://proofgeneral.inf.ed.ac.uk/kit
9 signature PROOF_GENERAL_PGIP =
11 val new_thms_deps: theory -> theory -> string list * string list
12 val init_pgip: bool -> unit (* main PGIP loop with true; fail with false *)
14 (* These two are just to support the semi-PGIP Emacs mode *)
15 val init_pgip_channel: (string -> unit) -> unit
16 val process_pgip: string -> unit
18 (* More message functions... *)
19 val nonfatal_error : string -> unit (* recoverable (batch) error: carry on scripting *)
20 val log_msg : string -> unit (* for internal log messages *)
21 val error_with_pos : PgipTypes.displayarea -> PgipTypes.fatality -> Position.T -> string -> unit
23 val get_currently_open_file : unit -> Path.T option (* interface focus *)
24 val add_preference: string -> Preferences.isa_preference -> unit
27 structure ProofGeneralPgip : PROOF_GENERAL_PGIP =
35 val proof_generalN = "ProofGeneral";
36 val pgmlsymbols_flag = ref true;
39 (* assembling and issuing PGIP packets *)
41 val pgip_refid = ref NONE: string option ref;
42 val pgip_refseq = ref NONE: int option ref;
46 val pgip_tag = "Isabelle/Isar"
49 fun pgip_serial () = inc pgip_seq
51 fun assemble_pgips pgips =
52 Pgip { tag = SOME pgip_tag,
56 destid = ! pgip_refid,
57 (* destid=refid since Isabelle only communicates back to sender *)
59 refseq = ! pgip_refseq,
63 fun init_pgip_session_id () =
64 pgip_id := getenv "HOSTNAME" ^ "/" ^ getenv "USER" ^ "/" ^
65 getenv "ISABELLE_PID" ^ "/" ^ Time.toString (Time.now ())
67 fun matching_pgip_id id = (id = ! pgip_id)
69 val output_xml_fn = ref Output.writeln_default
70 fun output_xml s = ! output_xml_fn (XML.string_of s);
72 val output_pgips = XML.string_of o PgipOutput.output o assemble_pgips o map PgipOutput.output;
74 val output_pgmlterm = XML.string_of o Pgml.pgmlterm_to_xml;
75 val output_pgmltext = XML.string_of o Pgml.pgml_to_xml;
78 fun issue_pgip_rawtext str =
79 output_xml (PgipOutput.output (assemble_pgips (YXML.parse_body str)));
81 fun issue_pgip pgipop =
82 output_xml (PgipOutput.output (assemble_pgips [PgipOutput.output pgipop]));
88 (** messages and notification **)
95 if ! pgmlsymbols_flag then
96 (case Symbol.decode s of
97 Symbol.Sym name => Pgml.Sym {name = name, content = s}
101 val pgml_syms = map pgml_sym o Symbol.explode;
104 [Markup.tclassN, Markup.tfreeN, Markup.tvarN, Markup.freeN,
105 Markup.boundN, Markup.varN, Markup.skolemN];
109 fun pgml_terms (XML.Elem (name, atts, body)) =
110 if member (op =) token_markups name then
111 let val content = pgml_syms (Buffer.content (fold XML.add_content body Buffer.empty))
112 in [Pgml.Atoms {kind = SOME name, content = content}] end
114 let val content = maps pgml_terms body in
115 if name = Markup.blockN then
116 [Pgml.Box {orient = NONE, indent = Properties.get_int atts Markup.indentN, content = content}]
117 else if name = Markup.breakN then
118 [Pgml.Break {mandatory = NONE, indent = Properties.get_int atts Markup.widthN}]
119 else if name = Markup.fbreakN then
120 [Pgml.Break {mandatory = SOME true, indent = NONE}]
123 | pgml_terms (XML.Text text) = map (Pgml.Raw o Pgml.atom_to_xml) (pgml_syms text);
130 fun pgml area content =
131 Pgml.Pgml {version = NONE, systemid = NONE, area = SOME area, content = content};
133 fun message_content default_area s =
135 val body = YXML.parse_body s;
138 [XML.Elem (name, _, _)] =>
139 if name = Markup.stateN then PgipTypes.Display else default_area
140 | _ => default_area);
141 in Pgml.pgml_to_xml (pgml area (maps pgml_terms body)) end;
144 fun normalmsg area s = issue_pgip
145 (Normalresponse {content = [message_content area s]});
147 fun errormsg area fatality s = issue_pgip
148 (Errorresponse {fatality = fatality, location = NONE, content = [message_content area s]});
150 (*error responses with useful locations*)
151 fun error_with_pos area fatality pos s = issue_pgip
154 location = SOME (PgipIsabelle.location_of_position pos),
155 content = [message_content area s]});
157 fun panic s = (errormsg Message Panic ("## SYSTEM EXIT ##\n" ^ s); exit 1);
158 fun nonfatal_error s = errormsg Message Nonfatal s;
159 fun log_msg s = errormsg Message Log s;
161 (* NB: all of standard functions print strings terminated with new lines, but we don't
162 add new lines explicitly in PGIP: they are left implicit. It means that PGIP messages
163 can't be written without newlines. *)
164 fun setup_messages () =
165 (Output.writeln_fn := (fn s => normalmsg Message s);
166 Output.status_fn := (fn _ => ());
167 Output.priority_fn := (fn s => normalmsg Status s);
168 Output.tracing_fn := (fn s => normalmsg Tracing s);
169 Output.warning_fn := (fn s => errormsg Message Warning s);
170 Output.error_fn := (fn s => errormsg Message Fatal s);
171 Output.debug_fn := (fn s => errormsg Message Debug s));
174 (* immediate messages *)
176 fun tell_clear_goals () =
177 issue_pgip (Normalresponse { content = [Pgml.pgml_to_xml (pgml Display [])] })
178 fun tell_clear_response () =
179 issue_pgip (Normalresponse { content = [Pgml.pgml_to_xml (pgml Message [])] })
181 fun tell_file_loaded completed path =
182 issue_pgip (Informfileloaded {url=PgipTypes.pgipurl_of_path path,
183 completed=completed})
184 fun tell_file_outdated completed path =
185 issue_pgip (Informfileoutdated {url=PgipTypes.pgipurl_of_path path,
186 completed=completed})
187 fun tell_file_retracted completed path =
188 issue_pgip (Informfileretracted {url=PgipTypes.pgipurl_of_path path,
189 completed=completed})
192 (* theory loader actions *)
195 (* da: TODO: PGIP has a completed flag so the prover can indicate to the
196 interface which files are busy performing a particular action.
197 To make use of this we need to adjust the hook in thy_info.ML
198 (may actually be difficult to tell the interface *which* action is in
199 progress, but we could add a generic "Lock" action which uses
200 informfileloaded: the broker/UI should not infer too much from incomplete
203 fun trace_action action name =
204 if action = ThyInfo.Update then
205 List.app (tell_file_loaded true) (ThyInfo.loaded_files name)
206 else if action = ThyInfo.Outdate then
207 List.app (tell_file_outdated true) (ThyInfo.loaded_files name)
208 else if action = ThyInfo.Remove then
209 List.app (tell_file_retracted true) (ThyInfo.loaded_files name)
214 fun setup_thy_loader () = ThyInfo.add_hook trace_action;
215 fun sync_thy_loader () = List.app (trace_action ThyInfo.Update) (ThyInfo.get_names ());
219 (* get informed about files *)
221 val thy_name = Path.implode o #1 o Path.split_ext o Path.base;
223 val inform_file_retracted = ThyInfo.if_known_thy ThyInfo.remove_thy o thy_name;
224 val inform_file_processed = ThyInfo.if_known_thy ThyInfo.touch_child_thys o thy_name;
226 fun proper_inform_file_processed path state =
227 let val name = thy_name path in
228 if Toplevel.is_toplevel state andalso ThyInfo.known_thy name then
229 (ThyInfo.touch_child_thys name;
230 ThyInfo.register_thy name handle ERROR msg =>
231 (warning (cat_lines [msg, "Failed to register theory: " ^ quote name]);
232 tell_file_retracted true (Path.base path)))
233 else raise Toplevel.UNDEF
237 (* restart top-level loop (keeps most state information) *)
239 val welcome = priority o Session.welcome;
244 tell_clear_response ();
249 (* theorem dependencies *)
254 (case Thm.proof_of th of
255 PThm (name, prf, _, _) =>
256 if Thm.has_name_hint th andalso Thm.get_name_hint th = name then
257 Proofterm.thms_of_proof' prf
259 | prf => Proofterm.thms_of_proof' prf);
263 (* FIXME proper derivation names!? *)
264 val names = map Thm.get_name_hint (filter Thm.has_name_hint ths);
265 val deps = Symtab.keys (fold thm_deps ths Symtab.empty);
266 in (names, deps) end;
270 fun new_thms_deps thy thy' =
272 val prev_facts = PureThy.facts_of thy;
273 val facts = PureThy.facts_of thy';
274 in thms_deps (maps #2 (Facts.dest_static [prev_facts] facts)) end;
279 (* theorem dependeny output *)
281 val show_theorem_dependencies = ref false;
285 val spaces_quote = space_implode " " o map quote;
287 fun thm_deps_message (thms, deps) =
289 val valuethms = XML.Elem ("value", [("name", "thms")], [XML.Text thms]);
290 val valuedeps = XML.Elem ("value", [("name", "deps")], [XML.Text deps]);
292 issue_pgip (Metainforesponse
293 {attrs = [("infotype", "isabelle_theorem_dependencies")],
294 content = [valuethms, valuedeps]})
299 fun setup_present_hook () = Toplevel.add_hook (fn _ => fn state => fn (state', opt_err) =>
300 if ! show_theorem_dependencies andalso
301 can Toplevel.theory_of state andalso
302 Toplevel.is_theory state' andalso is_none opt_err
304 let val (names, deps) = new_thms_deps (Toplevel.theory_of state) (Toplevel.theory_of state') in
305 if null names orelse null deps then ()
306 else thm_deps_message (spaces_quote names, spaces_quote deps)
313 (** lexicalstructure element with keywords (PGIP version of elisp keywords file) **)
315 fun lexicalstructure_keywords () =
316 let val keywords = OuterKeyword.dest_keywords ()
317 val commands = OuterKeyword.dest_commands ()
318 fun keyword_elt kind keyword =
319 XML.Elem("keyword", [("word", keyword), ("category", kind)], [])
321 (* Also, note we don't call init_outer_syntax here to add interface commands,
322 but they should never appear in scripts anyway so it shouldn't matter *)
324 {content = map (keyword_elt "minor") keywords @ map (keyword_elt "major") commands}
327 (* TODO: we can issue a lexicalstructure/keyword when the syntax gets extended dynamically;
328 hooks needed in outer_syntax.ML to do that. *)
331 (* Configuration: GUI config, proverinfo messages *)
334 val isabellewww = "http://isabelle.in.tum.de/"
335 val staticconfig = "~~/lib/ProofGeneral/pgip_isar.xml"
336 fun orenv v d = case getenv v of "" => d | s => s
337 fun config_file() = orenv "ISABELLE_PGIPCONFIG" staticconfig
338 fun isabelle_www() = orenv "ISABELLE_HOMEPAGE" isabellewww
340 fun send_pgip_config () =
342 val path = Path.explode (config_file())
343 val ex = File.exists path
346 (Url.explode (isabelle_www()))
348 (panic ("Error in URL in environment variable ISABELLE_HOMEPAGE.");
349 Url.explode isabellewww)
352 Proverinfo { name = "Isabelle",
353 version = Distribution.version,
354 instance = Session.name(),
355 descr = "The Isabelle/Isar theorem prover",
357 filenameextns = ".thy;" }
360 (issue_pgip proverinfo;
361 issue_pgip_rawtext (File.read path);
362 issue_pgip (lexicalstructure_keywords()))
363 else panic ("PGIP configuration file \"" ^ config_file() ^ "\" not found")
368 (* Preferences: tweak for PGIP interfaces *)
370 val preferences = ref Preferences.preferences;
372 fun add_preference cat pref =
373 preferences := Preferences.add cat pref (!preferences);
375 fun setup_preferences_tweak() =
377 (!preferences |> Preferences.set_default ("show-question-marks","false")
378 |> Preferences.remove "show-question-marks" (* we use markup, not ?s *)
379 |> Preferences.remove "theorem-dependencies" (* set internally *)
380 |> Preferences.remove "full-proofs") (* set internally *)
384 (* Sending commands to Isar *)
386 fun isarcmd s = Isar.>>> (OuterSyntax.parse Position.none s);
389 - apply a command given a transition function;
390 - fix position from path of currently open file [line numbers risk garbling though].
393 (* load an arbitrary file (must be .thy or .ML) *)
395 fun use_thy_or_ml_file file =
397 val (path,extn) = Path.split_ext (Path.explode file)
400 "" => isarcmd ("use_thy " ^ quote (Path.implode path))
401 | "thy" => isarcmd ("use_thy " ^ quote (Path.implode path))
402 | "ML" => isarcmd ("use " ^ quote file)
403 | other => error ("Don't know how to read a file with extension " ^ quote other)
407 (******* PGIP actions *******)
410 (* Responses to each of the PGIP input commands.
411 These are programmed uniformly for extensibility. *)
413 fun askpgip (Askpgip _) =
415 (Usespgip { version = PgipIsabelle.isabelle_pgip_version_supported,
416 pgipelems = PgipIsabelle.accepted_inputs });
419 fun askpgml (Askpgml _) =
421 (Usespgml { version = PgipIsabelle.isabelle_pgml_version_supported })
423 fun askprefs (Askprefs _) =
425 fun preference_of {name, descr, default, pgiptype, get, set } =
426 { name = name, descr = SOME descr, default = SOME default,
427 pgiptype = pgiptype }
429 List.app (fn (prefcat, prefs) =>
430 issue_pgip (Hasprefs {prefcategory=SOME prefcat,
431 prefs=map preference_of prefs}))
435 fun askconfig (Askconfig _) = () (* TODO: add config response *)
438 fun lookuppref pref =
439 case AList.lookup (op =)
440 (map (fn p => (#name p,p))
441 (maps snd (!preferences))) pref of
442 NONE => error ("Unknown prover preference: " ^ quote pref)
445 fun setpref (Setpref vs) =
448 val value = #value vs
449 val set = #set (lookuppref name)
454 fun getpref (Getpref vs) =
457 val get = #get (lookuppref name)
459 issue_pgip (Prefval {name=name, value=get ()})
463 fun proverinit _ = restart ()
465 fun proverexit _ = isarcmd "quit"
467 fun set_proverflag_quiet b =
468 isarcmd (if b then "disable_pr" else "enable_pr")
470 fun set_proverflag_pgmlsymbols b =
471 (pgmlsymbols_flag := b;
472 NAMED_CRITICAL "print_mode" (fn () =>
475 remove (op =) Symbol.xsymbolsN mode @ (if b then [Symbol.xsymbolsN] else []))))
477 fun set_proverflag_thmdeps b =
478 (show_theorem_dependencies := b;
479 Proofterm.proofs := (if b then 1 else 2))
481 fun setproverflag (Setproverflag vs) =
483 val flagname = #flagname vs
484 val value = #value vs
487 "quiet" => set_proverflag_quiet value
488 | "pgmlsymbols" => set_proverflag_pgmlsymbols value
489 | "metainfo:thmdeps" => set_proverflag_thmdeps value
490 | _ => log_msg ("Unrecognised prover control flag: " ^
491 (quote flagname) ^ " ignored."))
495 fun dostep (Dostep vs) =
502 fun undostep (Undostep vs) =
504 val times = #times vs
506 isarcmd ("undos_proof " ^ Int.toString times)
509 fun redostep _ = sys_error "redo unavailable"
511 fun abortgoal _ = isarcmd "kill" (* was: ProofGeneral.kill_proof *)
514 (*** PGIP identifier tables ***)
516 (* TODO: these ones should be triggered by hooks after a
517 declaration addition/removal, to be sent automatically. *)
519 fun addids t = issue_pgip (Addids {idtables = [t]})
520 fun delids t = issue_pgip (Delids {idtables = [t]})
525 fun theory_facts name =
526 let val thy = ThyInfo.get_theory name
527 in (map PureThy.facts_of (Theory.parents_of thy), PureThy.facts_of thy) end;
529 fun thms_of_thy name = map fst (theory_facts name |-> Facts.extern_static);
530 fun qualified_thms_of_thy name = map fst (theory_facts name |-> Facts.dest_static);
534 fun askids (Askids vs) =
536 val url = #url vs (* ask for identifiers within a file *)
537 val thyname = #thyname vs (* ask for identifiers within a theory *)
538 val objtype = #objtype vs (* ask for identifiers of a particular type *)
540 fun idtable ty ctx ids = {objtype=ty,context=ctx,ids=ids}
542 fun setids t = issue_pgip (Setids {idtables = [t]})
544 (* fake one-level nested "subtheories" by picking apart names. *)
545 val immed_thms_of_thy = filter_out NameSpace.is_qualified o thms_of_thy
546 fun thy_prefix s = case space_explode NameSpace.separator s of
547 x::_::_ => SOME x (* String.find? *)
549 fun subthys_of_thy s =
550 List.foldl (fn (NONE,xs) => xs | (SOME x,xs) => insert op= x xs) []
551 (map thy_prefix (thms_of_thy s))
552 fun subthms_of_thy thy =
553 (case thy_prefix thy of
554 NONE => immed_thms_of_thy thy
555 | SOME prf => filter (String.isPrefix (unprefix (prf ^ NameSpace.separator) thy))
558 case (thyname,objtype) of
560 setids (idtable ObjFile NONE (ThyInfo.get_names())) (*FIXME: uris*)
561 | (NONE, SOME ObjFile) =>
562 setids (idtable ObjFile NONE (ThyInfo.get_names())) (*FIXME: uris*)
563 | (SOME fi, SOME ObjFile) =>
564 setids (idtable ObjTheory (SOME fi) [fi]) (* TODO: check exists *)
565 | (NONE, SOME ObjTheory) =>
566 setids (idtable ObjTheory NONE (ThyInfo.get_names()))
567 | (SOME thy, SOME ObjTheory) =>
568 setids (idtable ObjTheory (SOME thy) (subthys_of_thy thy))
569 | (SOME thy, SOME ObjTheorem) =>
570 setids (idtable ObjTheorem (SOME thy) (subthms_of_thy thy))
571 | (NONE, SOME ObjTheorem) =>
572 (* A large query, but not unreasonable. ~5000 results for HOL.*)
573 (* Several setids should be allowed, but Eclipse code is currently broken:
574 List.app (fn thy => setids (idtable ObjTheorem (SOME thy) (subthms_of_thy thy)))
575 (ThyInfo.get_names()) *)
576 setids (idtable ObjTheorem NONE (* this one gives ~7000 for HOL *)
577 (maps qualified_thms_of_thy (ThyInfo.get_names())))
578 | _ => warning ("askids: ignored argument combination")
583 fun askrefs (Askrefs vs) =
585 val url = #url vs (* ask for references of a file (i.e. immediate pre-requisites) *)
586 val thyname = #thyname vs (* ask for references of a theory (other theories) *)
587 val objtype = #objtype vs (* ask for references of a particular type... *)
588 val name = #name vs (* ... with this name *)
590 fun idtable ty ctx ids = {objtype=ty,context=ctx,ids=ids}
592 val thy_name = Path.implode o #1 o Path.split_ext o Path.base
595 let val thy = thy_name f
596 val filerefs = #uses (ThyLoad.deps_thy (Path.dir f) thy)
598 issue_pgip (Setrefs {url=url, thyname=NONE, objtype=SOME PgipTypes.ObjFile,
599 name=NONE, idtables=[], fileurls=filerefs})
603 let val thyrefs = #imports (ThyLoad.deps_thy Path.current thy)
605 issue_pgip (Setrefs {url=url, thyname=thyname, objtype=SOME PgipTypes.ObjTheory,
606 name=NONE, idtables=[{context=NONE, objtype=PgipTypes.ObjTheory,
607 ids=thyrefs}], fileurls=[]})
610 fun thmrefs thmname =
612 (* TODO: interim: this is probably not right.
613 What we want is mapping onto simple PGIP name/context model. *)
614 val ctx = Toplevel.context_of (Isar.state ()) (* NB: raises UNDEF *)
615 val thy = Context.theory_of_proof ctx
616 val ths = [PureThy.get_thm thy thmname]
617 val deps = filter_out (equal "")
618 (Symtab.keys (fold Proofterm.thms_of_proof
619 (map Thm.proof_of ths) Symtab.empty))
622 else issue_pgip (Setrefs {url=url, thyname=thyname, name=name,
623 objtype=SOME PgipTypes.ObjTheorem,
624 idtables=[{context=NONE, objtype=PgipTypes.ObjTheorem,
625 ids=deps}], fileurls=[]})
628 case (url,thyname,objtype,name) of
629 (SOME file, NONE, _, _) => filerefs file
630 | (_,SOME thy,_,_) => thyrefs thy
631 | (_,_,SOME PgipTypes.ObjTheorem,SOME thmname) => thmrefs thmname
632 | _ => error ("Unimplemented/invalid case of <askrefs>")
637 fun showid (Showid vs) =
639 val thyname = #thyname vs
640 val objtype = #objtype vs
643 val topthy = Toplevel.theory_of o Isar.state
646 let val comps = NameSpace.explode id
648 (thy::(rest as _::_)) => (ThyInfo.get_theory thy, space_implode "." rest)
649 | [plainid] => (topthy(),plainid)
650 | _ => raise Toplevel.UNDEF (* assert false *)
654 fun idvalue strings =
655 issue_pgip (Idvalue { thyname=thyname, objtype=objtype, name=name,
656 text=[XML.Elem("pgml",[],
657 maps YXML.parse_body strings)] })
659 fun string_of_thm th = Pretty.string_of
660 (Display.pretty_thm_aux
661 (Syntax.pp_global (Thm.theory_of_thm th))
663 false (* show hyps *)
667 fun strings_of_thm (thy, name) = map string_of_thm (PureThy.get_thms thy name)
669 val string_of_thy = Pretty.string_of o ProofDisplay.pretty_full_theory false
671 case (thyname, objtype) of
672 (_, ObjTheory) => idvalue [string_of_thy (ThyInfo.get_theory name)]
673 | (SOME thy, ObjTheorem) => idvalue (strings_of_thm (ThyInfo.get_theory thy, name))
674 | (NONE, ObjTheorem) => idvalue (strings_of_thm (splitthy name))
675 | (_, ot) => error ("Cannot show objects of type "^(PgipTypes.name_of_objtype ot))
678 (*** Inspecting state ***)
680 (* The file which is currently being processed interactively.
681 In the pre-PGIP code, this was informed to Isabelle and the theory loader
682 on completion, but that allows for circularity in case we read
683 ourselves. So PGIP opens the filename at the start of a script.
684 We ought to prevent problems by modifying the theory loader to know
685 about this special status, but for now we just keep a local reference.
688 val currently_open_file = ref (NONE : pgipurl option)
690 fun get_currently_open_file () = ! currently_open_file;
693 (* The "guise" is the PGIP abstraction of the prover's state.
694 The <informguise> message is merely used for consistency checking. *)
696 val openfile = !currently_open_file
698 val topthy = Toplevel.theory_of o Isar.state
699 val topthy_name = Context.theory_name o topthy
701 val opentheory = SOME (topthy_name()) handle Toplevel.UNDEF => NONE
703 fun topproofpos () = try Toplevel.proof_position_of (Isar.state ());
704 val openproofpos = topproofpos()
706 issue_pgip (Informguise { file = openfile,
708 (* would be nice to get thm name... *)
710 proofpos = openproofpos })
713 fun parsescript (Parsescript vs) =
716 val systemdata = #systemdata vs
717 val location = #location vs (* TODO: extract position *)
719 val doc = PgipParser.pgip_parser Position.none text
721 val sysattrs = PgipTypes.opt_attr "systemdata" systemdata
722 val locattrs = PgipTypes.attrs_of_location location
724 issue_pgip (Parseresult { attrs= sysattrs@locattrs,
729 fun showproofstate _ = isarcmd "pr"
731 fun showctxt _ = isarcmd "print_context"
733 fun searchtheorems (Searchtheorems vs) =
737 isarcmd ("find_theorems " ^ arg)
740 fun setlinewidth (Setlinewidth vs) =
742 val width = #width vs
744 isarcmd ("pretty_setmargin " ^ Int.toString width) (* FIXME: conversion back/forth! *)
747 fun viewdoc (Viewdoc vs) =
751 isarcmd ("print_" ^ arg) (* FIXME: isatool doc?. Return URLs, maybe? *)
756 fun doitem (Doitem vs) =
770 isarcmd "kill" (* was: "init_toplevel" *)
772 fun retracttheory (Retracttheory vs) =
774 val thyname = #thyname vs
776 isarcmd ("kill_thy " ^ quote thyname)
782 (* Path management: we allow theory files to have dependencies in
783 their own directory, but when we change directory for a new file we
784 remove the path. Leaving it there can cause confusion with
785 difference in batch mode.
786 NB: PGIP does not assume that the prover has a load path.
790 val current_working_dir = ref (NONE : string option)
792 fun changecwd_dir newdirpath =
794 val newdir = File.platform_path newdirpath
796 (case (!current_working_dir) of
798 | SOME dir => ThyLoad.del_path dir;
799 ThyLoad.add_path newdir;
800 current_working_dir := SOME newdir)
804 fun changecwd (Changecwd vs) =
807 val newdir = PgipTypes.path_of_pgipurl url
812 fun openfile (Openfile vs) =
815 val filepath = PgipTypes.path_of_pgipurl url
816 val filedir = Path.dir filepath
817 val thy_name = Path.implode o #1 o Path.split_ext o Path.base
818 val openfile_retract = Output.no_warnings (ThyInfo.if_known_thy ThyInfo.remove_thy) o thy_name;
820 case !currently_open_file of
821 SOME f => raise PGIP ("<openfile> when a file is already open!\nCurrently open file: " ^
822 PgipTypes.string_of_pgipurl url)
823 | NONE => (openfile_retract filepath;
824 changecwd_dir filedir;
825 priority ("Working in file: " ^ PgipTypes.string_of_pgipurl url);
826 currently_open_file := SOME url)
830 case !currently_open_file of
831 SOME f => (proper_inform_file_processed f (Isar.state());
832 priority ("Finished working in file: " ^ PgipTypes.string_of_pgipurl f);
833 currently_open_file := NONE)
834 | NONE => raise PGIP ("<closefile> when no file is open!")
836 fun loadfile (Loadfile vs) =
840 (* da: this doesn't seem to cause a problem, batch loading uses
841 a different state context. Of course confusion is still possible,
842 e.g. file loaded depends on open file which is not yet saved. *)
843 (* case !currently_open_file of
844 SOME f => raise PGIP ("<loadfile> when a file is open!\nCurrently open file: " ^
845 PgipTypes.string_of_pgipurl url)
847 use_thy_or_ml_file (File.platform_path url)
851 case !currently_open_file of
852 SOME f => (isarcmd "init_toplevel";
853 priority ("Aborted working in file: " ^
854 PgipTypes.string_of_pgipurl f);
855 currently_open_file := NONE)
856 | NONE => raise PGIP ("<abortfile> when no file is open!")
858 fun retractfile (Retractfile vs) =
862 case !currently_open_file of
863 SOME f => raise PGIP ("<retractfile> when a file is open!")
864 | NONE => (priority ("Retracting file: " ^ PgipTypes.string_of_pgipurl url);
865 (* TODO: next should be in thy loader, here just for testing *)
867 val name = thy_name url
868 in List.app (tell_file_retracted false) (ThyInfo.loaded_files name) end;
869 inform_file_retracted url)
875 fun systemcmd (Systemcmd vs) =
883 fun quitpgip _ = raise PGIP_QUIT
885 fun process_input inp = case inp
886 of Pgip.Askpgip _ => askpgip inp
887 | Pgip.Askpgml _ => askpgml inp
888 | Pgip.Askprefs _ => askprefs inp
889 | Pgip.Askconfig _ => askconfig inp
890 | Pgip.Getpref _ => getpref inp
891 | Pgip.Setpref _ => setpref inp
892 | Pgip.Proverinit _ => proverinit inp
893 | Pgip.Proverexit _ => proverexit inp
894 | Pgip.Setproverflag _ => setproverflag inp
895 | Pgip.Dostep _ => dostep inp
896 | Pgip.Undostep _ => undostep inp
897 | Pgip.Redostep _ => redostep inp
898 | Pgip.Forget _ => error "<forget> not implemented by Isabelle"
899 | Pgip.Restoregoal _ => error "<restoregoal> not implemented by Isabelle"
900 | Pgip.Abortgoal _ => abortgoal inp
901 | Pgip.Askids _ => askids inp
902 | Pgip.Askrefs _ => askrefs inp
903 | Pgip.Showid _ => showid inp
904 | Pgip.Askguise _ => askguise inp
905 | Pgip.Parsescript _ => parsescript inp
906 | Pgip.Showproofstate _ => showproofstate inp
907 | Pgip.Showctxt _ => showctxt inp
908 | Pgip.Searchtheorems _ => searchtheorems inp
909 | Pgip.Setlinewidth _ => setlinewidth inp
910 | Pgip.Viewdoc _ => viewdoc inp
911 | Pgip.Doitem _ => doitem inp
912 | Pgip.Undoitem _ => undoitem inp
913 | Pgip.Redoitem _ => redoitem inp
914 | Pgip.Aborttheory _ => aborttheory inp
915 | Pgip.Retracttheory _ => retracttheory inp
916 | Pgip.Loadfile _ => loadfile inp
917 | Pgip.Openfile _ => openfile inp
918 | Pgip.Closefile _ => closefile inp
919 | Pgip.Abortfile _ => abortfile inp
920 | Pgip.Retractfile _ => retractfile inp
921 | Pgip.Changecwd _ => changecwd inp
922 | Pgip.Systemcmd _ => systemcmd inp
923 | Pgip.Quitpgip _ => quitpgip inp
926 fun process_pgip_element pgipxml =
928 xml as (XML.Elem elem) =>
929 (case Pgip.input elem of
930 NONE => warning ("Unrecognized PGIP command, ignored: \n" ^
932 | SOME inp => (process_input inp)) (* errors later; packet discarded *)
933 | XML.Text t => ignored_text_warning t
934 and ignored_text_warning t =
935 if size (Symbol.strip_blanks t) > 0 then
936 warning ("Ignored text in PGIP packet: \n" ^ t)
939 fun process_pgip_tree xml =
943 XML.Elem ("pgip", attrs, pgips) =>
945 val class = PgipTypes.get_attr "class" attrs
946 val dest = PgipTypes.get_attr_opt "destid" attrs
947 val seq = PgipTypes.read_pgipnat (PgipTypes.get_attr "seq" attrs)
948 (* Respond to prover broadcasts, or messages for us. Ignore rest *)
952 | SOME id => matching_pgip_id id
954 (pgip_refid := PgipTypes.get_attr_opt "id" attrs;
955 pgip_refseq := SOME seq;
956 List.app process_pgip_element pgips;
957 (* return true to indicate <ready/> *)
960 (* no response to ignored messages. *)
963 | _ => raise PGIP "Invalid PGIP packet received")
965 (Output.error_msg ((msg ^ "\nPGIP error occured in XML text below:\n") ^
966 (XML.string_of xml));
971 val process_pgip_plain = K () o process_pgip_tree o XML.parse
973 (* PGIP loop: process PGIP input only *)
981 val _ = if ready then issue_pgip (Ready ()) else ()
983 (case try Source.get_single src of
985 | NONE => raise XML_PARSE)
989 | SOME (pgip,src') =>
991 val ready' = (process_pgip_tree pgip)
992 handle PGIP_QUIT => raise PGIP_QUIT
993 | e => (handler (e,SOME src'); true)
997 end handle e => handler (e,SOME src) (* error in XML parse or Ready issue *)
999 and handler (e,srco) =
1001 (XML_PARSE,SOME src) =>
1002 panic "Invalid XML input, aborting" (* TODO: attempt recovery *)
1003 | (Interrupt,SOME src) =>
1004 (Output.error_msg "Interrupt during PGIP processing"; loop true src)
1005 | (Toplevel.UNDEF,SOME src) =>
1006 (Output.error_msg "No working context defined"; loop true src)
1008 (Output.error_msg (Toplevel.exn_message e); loop true src)
1009 | (PGIP_QUIT,_) => ()
1012 (* TODO: add socket interface *)
1014 val xmlP = XML.parse_comments |-- XML.parse_element >> single
1016 val tty_src = Source.set_prompt "" (Source.source Symbol.stopper xmlP NONE Source.tty)
1018 fun pgip_toplevel x = loop true x
1022 (* Extra command for embedding prover-control inside document (obscure/debug usage). *)
1024 fun init_outer_syntax () =
1025 OuterSyntax.improper_command "ProofGeneral.process_pgip" "(internal)" OuterKeyword.control
1026 (OuterParse.text >> (Toplevel.no_timing oo
1027 (fn txt => Toplevel.imperative (fn () => process_pgip_plain txt))));
1032 val initialized = ref false;
1034 fun init_pgip false = panic "No Proof General interface support for Isabelle/classic mode."
1036 (! initialized orelse
1037 (setup_preferences_tweak ();
1038 Output.add_mode proof_generalN Output.default_output Output.default_escape;
1039 Markup.add_mode proof_generalN YXML.output_markup;
1041 Output.no_warnings init_outer_syntax ();
1042 setup_thy_loader ();
1043 setup_present_hook ();
1044 init_pgip_session_id ();
1048 change print_mode (update (op =) proof_generalN);
1049 pgip_toplevel tty_src);
1053 (** Out-of-loop PGIP commands (for Emacs hybrid mode) **)
1056 val pgip_output_channel = ref Output.writeln_default
1059 (* Set recipient for PGIP results *)
1060 fun init_pgip_channel writefn =
1061 (init_pgip_session_id();
1062 pgip_output_channel := writefn)
1064 (* Process a PGIP command.
1065 This works for preferences but not generally guaranteed
1066 because we haven't done full setup here (e.g., no pgml mode) *)
1067 fun process_pgip str =
1068 setmp output_xml_fn (!pgip_output_channel) process_pgip_plain str