1 (* Title: Pure/ProofGeneral/proof_general_pgip.ML
2 Author: David Aspinall and Markus Wenzel
4 Isabelle configuration for Proof General using PGIP protocol.
5 See http://proofgeneral.inf.ed.ac.uk/kit
8 signature PROOF_GENERAL_PGIP =
10 val new_thms_deps: theory -> theory -> string list * string list
11 val init_pgip: bool -> unit (* main PGIP loop with true; fail with false *)
13 (* These two are just to support the semi-PGIP Emacs mode *)
14 val init_pgip_channel: (string -> unit) -> unit
15 val process_pgip: string -> unit
17 (* More message functions... *)
18 val nonfatal_error : string -> unit (* recoverable (batch) error: carry on scripting *)
19 val log_msg : string -> unit (* for internal log messages *)
20 val error_with_pos : PgipTypes.displayarea -> PgipTypes.fatality -> Position.T -> string -> unit
22 val get_currently_open_file : unit -> Path.T option (* interface focus *)
23 val add_preference: string -> Preferences.preference -> unit
26 structure ProofGeneralPgip : PROOF_GENERAL_PGIP =
34 val proof_generalN = "ProofGeneral";
35 val pgmlsymbols_flag = Unsynchronized.ref true;
38 (* assembling and issuing PGIP packets *)
40 val pgip_refid = Unsynchronized.ref NONE: string option Unsynchronized.ref;
41 val pgip_refseq = Unsynchronized.ref NONE: int option Unsynchronized.ref;
45 val pgip_tag = "Isabelle/Isar"
46 val pgip_id = Unsynchronized.ref ""
47 val pgip_seq = Unsynchronized.ref 0
48 fun pgip_serial () = Unsynchronized.inc pgip_seq
50 fun assemble_pgips pgips =
51 Pgip { tag = SOME pgip_tag,
55 destid = ! pgip_refid,
56 (* destid=refid since Isabelle only communicates back to sender *)
58 refseq = ! pgip_refseq,
62 fun init_pgip_session_id () =
63 pgip_id := getenv "HOSTNAME" ^ "/" ^ getenv "USER" ^ "/" ^
64 getenv "ISABELLE_PID" ^ "/" ^ Time.toString (Time.now ())
66 fun matching_pgip_id id = (id = ! pgip_id)
68 val output_xml_fn = Unsynchronized.ref Output.writeln_default
69 fun output_xml s = ! output_xml_fn (XML.string_of s);
71 val output_pgips = XML.string_of o PgipOutput.output o assemble_pgips o map PgipOutput.output;
73 val output_pgmlterm = XML.string_of o Pgml.pgmlterm_to_xml;
74 val output_pgmltext = XML.string_of o Pgml.pgml_to_xml;
77 fun issue_pgip_rawtext str =
78 output_xml (PgipOutput.output (assemble_pgips (YXML.parse_body str)));
80 fun issue_pgip pgipop =
81 output_xml (PgipOutput.output (assemble_pgips [PgipOutput.output pgipop]));
87 (** messages and notification **)
94 if ! pgmlsymbols_flag then
95 (case Symbol.decode s of
96 Symbol.Sym name => Pgml.Sym {name = name, content = s}
100 val pgml_syms = map pgml_sym o Symbol.explode;
103 [Markup.tclassN, Markup.tfreeN, Markup.tvarN, Markup.freeN,
104 Markup.boundN, Markup.varN, Markup.skolemN];
108 fun pgml_terms (XML.Elem (name, atts, body)) =
109 if member (op =) token_markups name then
110 let val content = pgml_syms (Buffer.content (fold XML.add_content body Buffer.empty))
111 in [Pgml.Atoms {kind = SOME name, content = content}] end
113 let val content = maps pgml_terms body in
114 if name = Markup.blockN then
115 [Pgml.Box {orient = NONE, indent = Properties.get_int atts Markup.indentN, content = content}]
116 else if name = Markup.breakN then
117 [Pgml.Break {mandatory = NONE, indent = Properties.get_int atts Markup.widthN}]
118 else if name = Markup.fbreakN then
119 [Pgml.Break {mandatory = SOME true, indent = NONE}]
122 | pgml_terms (XML.Text text) = map (Pgml.Raw o Pgml.atom_to_xml) (pgml_syms text);
129 fun pgml area content =
130 Pgml.Pgml {version = NONE, systemid = NONE, area = SOME area, content = content};
132 fun message_content default_area s =
134 val body = YXML.parse_body s;
137 [XML.Elem (name, _, _)] =>
138 if name = Markup.stateN then PgipTypes.Display else default_area
139 | _ => default_area);
140 in Pgml.pgml_to_xml (pgml area (maps pgml_terms body)) end;
143 fun normalmsg area s = issue_pgip
144 (Normalresponse {content = [message_content area s]});
146 fun errormsg area fatality s = issue_pgip
147 (Errorresponse {fatality = fatality, location = NONE, content = [message_content area s]});
149 (*error responses with useful locations*)
150 fun error_with_pos area fatality pos s = issue_pgip
153 location = SOME (PgipIsabelle.location_of_position pos),
154 content = [message_content area s]});
156 fun panic s = (errormsg Message Panic ("## SYSTEM EXIT ##\n" ^ s); exit 1);
157 fun nonfatal_error s = errormsg Message Nonfatal s;
158 fun log_msg s = errormsg Message Log s;
160 (* NB: all of standard functions print strings terminated with new lines, but we don't
161 add new lines explicitly in PGIP: they are left implicit. It means that PGIP messages
162 can't be written without newlines. *)
163 fun setup_messages () =
164 (Output.writeln_fn := (fn s => normalmsg Message s);
165 Output.status_fn := (fn _ => ());
166 Output.priority_fn := (fn s => normalmsg Status s);
167 Output.tracing_fn := (fn s => normalmsg Tracing s);
168 Output.warning_fn := (fn s => errormsg Message Warning s);
169 Output.error_fn := (fn s => errormsg Message Fatal s);
170 Output.debug_fn := (fn s => errormsg Message Debug s));
173 (* immediate messages *)
175 fun tell_clear_goals () =
176 issue_pgip (Normalresponse { content = [Pgml.pgml_to_xml (pgml Display [])] })
177 fun tell_clear_response () =
178 issue_pgip (Normalresponse { content = [Pgml.pgml_to_xml (pgml Message [])] })
180 fun tell_file_loaded completed path =
181 issue_pgip (Informfileloaded {url=PgipTypes.pgipurl_of_path path,
182 completed=completed})
183 fun tell_file_outdated completed path =
184 issue_pgip (Informfileoutdated {url=PgipTypes.pgipurl_of_path path,
185 completed=completed})
186 fun tell_file_retracted completed path =
187 issue_pgip (Informfileretracted {url=PgipTypes.pgipurl_of_path path,
188 completed=completed})
191 (* theory loader actions *)
194 (* da: TODO: PGIP has a completed flag so the prover can indicate to the
195 interface which files are busy performing a particular action.
196 To make use of this we need to adjust the hook in thy_info.ML
197 (may actually be difficult to tell the interface *which* action is in
198 progress, but we could add a generic "Lock" action which uses
199 informfileloaded: the broker/UI should not infer too much from incomplete
202 fun trace_action action name =
203 if action = ThyInfo.Update then
204 List.app (tell_file_loaded true) (ThyInfo.loaded_files name)
205 else if action = ThyInfo.Outdate then
206 List.app (tell_file_outdated true) (ThyInfo.loaded_files name)
207 else if action = ThyInfo.Remove then
208 List.app (tell_file_retracted true) (ThyInfo.loaded_files name)
213 fun setup_thy_loader () = ThyInfo.add_hook trace_action;
214 fun sync_thy_loader () = List.app (trace_action ThyInfo.Update) (ThyInfo.get_names ());
218 (* get informed about files *)
220 val thy_name = Path.implode o #1 o Path.split_ext o Path.base;
222 val inform_file_retracted = ThyInfo.if_known_thy ThyInfo.remove_thy o thy_name;
223 val inform_file_processed = ThyInfo.if_known_thy ThyInfo.touch_child_thys o thy_name;
225 fun proper_inform_file_processed path state =
226 let val name = thy_name path in
227 if Toplevel.is_toplevel state andalso ThyInfo.known_thy name then
228 (ThyInfo.touch_child_thys name;
229 ThyInfo.register_thy name handle ERROR msg =>
230 (warning (cat_lines [msg, "Failed to register theory: " ^ quote name]);
231 tell_file_retracted true (Path.base path)))
232 else raise Toplevel.UNDEF
236 (* restart top-level loop (keeps most state information) *)
238 val welcome = priority o Session.welcome;
243 tell_clear_response ();
248 (* theorem dependencies *)
252 fun add_proof_body (PBody {thms, ...}) =
253 thms |> fold (fn (_, (name, _, _)) => name <> "" ? Symtab.update (name, ()));
256 (case Thm.proof_body_of th of
257 PBody {proof = PThm (_, ((name, _, _), body)), ...} =>
258 if Thm.has_name_hint th andalso Thm.get_name_hint th = name
259 then add_proof_body (Future.join body)
261 | body => add_proof_body body);
267 (* FIXME proper derivation names!? *)
268 val names = map Thm.get_name_hint (filter Thm.has_name_hint ths);
269 val deps = Symtab.keys (fold add_thm ths Symtab.empty);
270 in (names, deps) end;
272 fun new_thms_deps thy thy' =
274 val prev_facts = PureThy.facts_of thy;
275 val facts = PureThy.facts_of thy';
276 in thms_deps (maps #2 (Facts.dest_static [prev_facts] facts)) end;
281 (* theorem dependeny output *)
283 val show_theorem_dependencies = Unsynchronized.ref false;
287 val spaces_quote = space_implode " " o map quote;
289 fun thm_deps_message (thms, deps) =
291 val valuethms = XML.Elem ("value", [("name", "thms")], [XML.Text thms]);
292 val valuedeps = XML.Elem ("value", [("name", "deps")], [XML.Text deps]);
294 issue_pgip (Metainforesponse
295 {attrs = [("infotype", "isabelle_theorem_dependencies")],
296 content = [valuethms, valuedeps]})
301 fun setup_present_hook () = Toplevel.add_hook (fn _ => fn state => fn state' =>
302 if ! show_theorem_dependencies andalso
303 can Toplevel.theory_of state andalso Toplevel.is_theory state'
305 let val (names, deps) = new_thms_deps (Toplevel.theory_of state) (Toplevel.theory_of state') in
306 if null names orelse null deps then ()
307 else thm_deps_message (spaces_quote names, spaces_quote deps)
314 (** lexicalstructure element with keywords (PGIP version of elisp keywords file) **)
316 fun lexicalstructure_keywords () =
317 let val keywords = OuterKeyword.dest_keywords ()
318 val commands = OuterKeyword.dest_commands ()
319 fun keyword_elt kind keyword =
320 XML.Elem("keyword", [("word", keyword), ("category", kind)], [])
322 (* Also, note we don't call init_outer_syntax here to add interface commands,
323 but they should never appear in scripts anyway so it shouldn't matter *)
325 {content = map (keyword_elt "minor") keywords @ map (keyword_elt "major") commands}
328 (* TODO: we can issue a lexicalstructure/keyword when the syntax gets extended dynamically;
329 hooks needed in outer_syntax.ML to do that. *)
332 (* Configuration: GUI config, proverinfo messages *)
335 val isabellewww = "http://isabelle.in.tum.de/"
336 val staticconfig = "~~/lib/ProofGeneral/pgip_isar.xml"
337 fun orenv v d = case getenv v of "" => d | s => s
338 fun config_file() = orenv "ISABELLE_PGIPCONFIG" staticconfig
339 fun isabelle_www() = orenv "ISABELLE_HOMEPAGE" isabellewww
341 fun send_pgip_config () =
343 val path = Path.explode (config_file())
344 val ex = File.exists path
347 (Url.explode (isabelle_www()))
349 (panic ("Error in URL in environment variable ISABELLE_HOMEPAGE.");
350 Url.explode isabellewww)
353 Proverinfo { name = "Isabelle",
354 version = Distribution.version,
355 instance = Session.name(),
356 descr = "The Isabelle/Isar theorem prover",
358 filenameextns = ".thy;" }
361 (issue_pgip proverinfo;
362 issue_pgip_rawtext (File.read path);
363 issue_pgip (lexicalstructure_keywords()))
364 else panic ("PGIP configuration file \"" ^ config_file() ^ "\" not found")
369 (* Preferences: tweak for PGIP interfaces *)
371 val preferences = Unsynchronized.ref Preferences.pure_preferences;
373 fun add_preference cat pref =
374 CRITICAL (fn () => Unsynchronized.change preferences (Preferences.add cat pref));
376 fun setup_preferences_tweak () =
377 CRITICAL (fn () => Unsynchronized.change preferences
378 (Preferences.set_default ("show-question-marks", "false") #>
379 Preferences.remove "show-question-marks" #> (* we use markup, not ?s *)
380 Preferences.remove "theorem-dependencies" #> (* set internally *)
381 Preferences.remove "full-proofs")); (* set internally *)
385 (* Sending commands to Isar *)
387 fun isarcmd s = Isar.>>> (OuterSyntax.parse Position.none s);
390 - apply a command given a transition function;
391 - fix position from path of currently open file [line numbers risk garbling though].
394 (* load an arbitrary file (must be .thy or .ML) *)
396 fun use_thy_or_ml_file file =
398 val (path,extn) = Path.split_ext (Path.explode file)
401 "" => isarcmd ("use_thy " ^ quote (Path.implode path))
402 | "thy" => isarcmd ("use_thy " ^ quote (Path.implode path))
403 | "ML" => isarcmd ("use " ^ quote file)
404 | other => error ("Don't know how to read a file with extension " ^ quote other)
408 (******* PGIP actions *******)
411 (* Responses to each of the PGIP input commands.
412 These are programmed uniformly for extensibility. *)
414 fun askpgip (Askpgip _) =
416 (Usespgip { version = PgipIsabelle.isabelle_pgip_version_supported,
417 pgipelems = PgipIsabelle.accepted_inputs });
420 fun askpgml (Askpgml _) =
422 (Usespgml { version = PgipIsabelle.isabelle_pgml_version_supported })
424 fun askprefs (Askprefs _) =
426 fun preference_of {name, descr, default, pgiptype, get, set } =
427 { name = name, descr = SOME descr, default = SOME default,
428 pgiptype = pgiptype }
430 List.app (fn (prefcat, prefs) =>
431 issue_pgip (Hasprefs {prefcategory=SOME prefcat,
432 prefs=map preference_of prefs}))
436 fun askconfig (Askconfig _) = () (* TODO: add config response *)
439 fun lookuppref pref =
440 case AList.lookup (op =)
441 (map (fn p => (#name p,p))
442 (maps snd (!preferences))) pref of
443 NONE => error ("Unknown prover preference: " ^ quote pref)
446 fun setpref (Setpref vs) =
449 val value = #value vs
450 val set = #set (lookuppref name)
455 fun getpref (Getpref vs) =
458 val get = #get (lookuppref name)
460 issue_pgip (Prefval {name=name, value=get ()})
464 fun proverinit _ = restart ()
466 fun proverexit _ = isarcmd "quit"
468 fun set_proverflag_quiet b =
469 isarcmd (if b then "disable_pr" else "enable_pr")
471 fun set_proverflag_pgmlsymbols b =
472 (pgmlsymbols_flag := b;
473 NAMED_CRITICAL "print_mode" (fn () =>
474 Unsynchronized.change print_mode
476 remove (op =) Symbol.xsymbolsN mode @ (if b then [Symbol.xsymbolsN] else []))))
478 fun set_proverflag_thmdeps b =
479 (show_theorem_dependencies := b;
480 Proofterm.proofs := (if b then 1 else 2))
482 fun setproverflag (Setproverflag vs) =
484 val flagname = #flagname vs
485 val value = #value vs
488 "quiet" => set_proverflag_quiet value
489 | "pgmlsymbols" => set_proverflag_pgmlsymbols value
490 | "metainfo:thmdeps" => set_proverflag_thmdeps value
491 | _ => log_msg ("Unrecognised prover control flag: " ^
492 (quote flagname) ^ " ignored."))
496 fun dostep (Dostep vs) =
503 fun undostep (Undostep vs) =
505 val times = #times vs
507 isarcmd ("undos_proof " ^ Int.toString times)
510 fun redostep _ = sys_error "redo unavailable"
512 fun abortgoal _ = isarcmd "kill" (* was: ProofGeneral.kill_proof *)
515 (*** PGIP identifier tables ***)
517 (* TODO: these ones should be triggered by hooks after a
518 declaration addition/removal, to be sent automatically. *)
520 fun addids t = issue_pgip (Addids {idtables = [t]})
521 fun delids t = issue_pgip (Delids {idtables = [t]})
526 fun theory_facts name =
527 let val thy = ThyInfo.get_theory name
528 in (map PureThy.facts_of (Theory.parents_of thy), PureThy.facts_of thy) end;
530 fun thms_of_thy name = map fst (theory_facts name |-> Facts.extern_static);
531 fun qualified_thms_of_thy name = map fst (theory_facts name |-> Facts.dest_static);
535 fun askids (Askids vs) =
537 val url = #url vs (* ask for identifiers within a file *)
538 val thyname = #thyname vs (* ask for identifiers within a theory *)
539 val objtype = #objtype vs (* ask for identifiers of a particular type *)
541 fun idtable ty ctx ids = {objtype=ty,context=ctx,ids=ids}
543 fun setids t = issue_pgip (Setids {idtables = [t]})
545 (* fake one-level nested "subtheories" by picking apart names. *)
546 val immed_thms_of_thy = filter_out Long_Name.is_qualified o thms_of_thy
547 fun thy_prefix s = case Long_Name.explode s of
548 x::_::_ => SOME x (* String.find? *)
550 fun subthys_of_thy s =
551 List.foldl (fn (NONE,xs) => xs | (SOME x,xs) => insert op= x xs) []
552 (map thy_prefix (thms_of_thy s))
553 fun subthms_of_thy thy =
554 (case thy_prefix thy of
555 NONE => immed_thms_of_thy thy
556 | SOME prf => filter (String.isPrefix (unprefix (prf ^ Long_Name.separator) thy))
559 case (thyname,objtype) of
561 setids (idtable ObjFile NONE (ThyInfo.get_names())) (*FIXME: uris*)
562 | (NONE, SOME ObjFile) =>
563 setids (idtable ObjFile NONE (ThyInfo.get_names())) (*FIXME: uris*)
564 | (SOME fi, SOME ObjFile) =>
565 setids (idtable ObjTheory (SOME fi) [fi]) (* TODO: check exists *)
566 | (NONE, SOME ObjTheory) =>
567 setids (idtable ObjTheory NONE (ThyInfo.get_names()))
568 | (SOME thy, SOME ObjTheory) =>
569 setids (idtable ObjTheory (SOME thy) (subthys_of_thy thy))
570 | (SOME thy, SOME ObjTheorem) =>
571 setids (idtable ObjTheorem (SOME thy) (subthms_of_thy thy))
572 | (NONE, SOME ObjTheorem) =>
573 (* A large query, but not unreasonable. ~5000 results for HOL.*)
574 (* Several setids should be allowed, but Eclipse code is currently broken:
575 List.app (fn thy => setids (idtable ObjTheorem (SOME thy) (subthms_of_thy thy)))
576 (ThyInfo.get_names()) *)
577 setids (idtable ObjTheorem NONE (* this one gives ~7000 for HOL *)
578 (maps qualified_thms_of_thy (ThyInfo.get_names())))
579 | _ => warning ("askids: ignored argument combination")
584 fun askrefs (Askrefs vs) =
586 val url = #url vs (* ask for references of a file (i.e. immediate pre-requisites) *)
587 val thyname = #thyname vs (* ask for references of a theory (other theories) *)
588 val objtype = #objtype vs (* ask for references of a particular type... *)
589 val name = #name vs (* ... with this name *)
591 fun idtable ty ctx ids = {objtype=ty,context=ctx,ids=ids}
593 val thy_name = Path.implode o #1 o Path.split_ext o Path.base
596 let val thy = thy_name f
597 val filerefs = #uses (ThyLoad.deps_thy (Path.dir f) thy)
599 issue_pgip (Setrefs {url=url, thyname=NONE, objtype=SOME PgipTypes.ObjFile,
600 name=NONE, idtables=[], fileurls=filerefs})
604 let val thyrefs = #imports (ThyLoad.deps_thy Path.current thy)
606 issue_pgip (Setrefs {url=url, thyname=thyname, objtype=SOME PgipTypes.ObjTheory,
607 name=NONE, idtables=[{context=NONE, objtype=PgipTypes.ObjTheory,
608 ids=thyrefs}], fileurls=[]})
611 fun thmrefs thmname =
613 (* TODO: interim: this is probably not right.
614 What we want is mapping onto simple PGIP name/context model. *)
615 val ctx = Toplevel.context_of (Isar.state ()) (* NB: raises UNDEF *)
616 val thy = ProofContext.theory_of ctx
617 val ths = [PureThy.get_thm thy thmname]
618 val deps = #2 (thms_deps ths);
621 else issue_pgip (Setrefs {url=url, thyname=thyname, name=name,
622 objtype=SOME PgipTypes.ObjTheorem,
623 idtables=[{context=NONE, objtype=PgipTypes.ObjTheorem,
624 ids=deps}], fileurls=[]})
627 case (url,thyname,objtype,name) of
628 (SOME file, NONE, _, _) => filerefs file
629 | (_,SOME thy,_,_) => thyrefs thy
630 | (_,_,SOME PgipTypes.ObjTheorem,SOME thmname) => thmrefs thmname
631 | _ => error ("Unimplemented/invalid case of <askrefs>")
636 fun showid (Showid vs) =
638 val thyname = #thyname vs
639 val objtype = #objtype vs
642 val topthy = Toplevel.theory_of o Isar.state
645 let val comps = Long_Name.explode id
647 (thy::(rest as _::_)) => (ThyInfo.get_theory thy, space_implode "." rest)
648 | [plainid] => (topthy(),plainid)
649 | _ => raise Toplevel.UNDEF (* assert false *)
653 fun idvalue strings =
654 issue_pgip (Idvalue { thyname=thyname, objtype=objtype, name=name,
655 text=[XML.Elem("pgml",[],
656 maps YXML.parse_body strings)] })
658 fun strings_of_thm (thy, name) =
659 map (Display.string_of_thm_global thy) (PureThy.get_thms thy name)
661 val string_of_thy = Pretty.string_of o Proof_Display.pretty_full_theory false
663 case (thyname, objtype) of
664 (_, ObjTheory) => idvalue [string_of_thy (ThyInfo.get_theory name)]
665 | (SOME thy, ObjTheorem) => idvalue (strings_of_thm (ThyInfo.get_theory thy, name))
666 | (NONE, ObjTheorem) => idvalue (strings_of_thm (splitthy name))
667 | (_, ot) => error ("Cannot show objects of type "^(PgipTypes.name_of_objtype ot))
670 (*** Inspecting state ***)
672 (* The file which is currently being processed interactively.
673 In the pre-PGIP code, this was informed to Isabelle and the theory loader
674 on completion, but that allows for circularity in case we read
675 ourselves. So PGIP opens the filename at the start of a script.
676 We ought to prevent problems by modifying the theory loader to know
677 about this special status, but for now we just keep a local reference.
680 val currently_open_file = Unsynchronized.ref (NONE : pgipurl option)
682 fun get_currently_open_file () = ! currently_open_file;
685 (* The "guise" is the PGIP abstraction of the prover's state.
686 The <informguise> message is merely used for consistency checking. *)
688 val openfile = !currently_open_file
690 val topthy = Toplevel.theory_of o Isar.state
691 val topthy_name = Context.theory_name o topthy
693 val opentheory = SOME (topthy_name()) handle Toplevel.UNDEF => NONE
695 fun topproofpos () = try Toplevel.proof_position_of (Isar.state ());
696 val openproofpos = topproofpos()
698 issue_pgip (Informguise { file = openfile,
700 (* would be nice to get thm name... *)
702 proofpos = openproofpos })
705 fun parsescript (Parsescript vs) =
708 val systemdata = #systemdata vs
709 val location = #location vs (* TODO: extract position *)
711 val doc = PgipParser.pgip_parser Position.none text
713 val sysattrs = PgipTypes.opt_attr "systemdata" systemdata
714 val locattrs = PgipTypes.attrs_of_location location
716 issue_pgip (Parseresult { attrs= sysattrs@locattrs,
721 fun showproofstate _ = isarcmd "pr"
723 fun showctxt _ = isarcmd "print_context"
725 fun searchtheorems (Searchtheorems vs) =
729 isarcmd ("find_theorems " ^ arg)
732 fun setlinewidth (Setlinewidth vs) =
734 val width = #width vs
736 isarcmd ("pretty_setmargin " ^ Int.toString width) (* FIXME: conversion back/forth! *)
739 fun viewdoc (Viewdoc vs) =
743 isarcmd ("print_" ^ arg) (* FIXME: isabelle doc?. Return URLs, maybe? *)
748 fun doitem (Doitem vs) =
762 isarcmd "kill" (* was: "init_toplevel" *)
764 fun retracttheory (Retracttheory vs) =
766 val thyname = #thyname vs
768 isarcmd ("kill_thy " ^ quote thyname)
774 (* Path management: we allow theory files to have dependencies in
775 their own directory, but when we change directory for a new file we
776 remove the path. Leaving it there can cause confusion with
777 difference in batch mode.
778 NB: PGIP does not assume that the prover has a load path.
782 val current_working_dir = Unsynchronized.ref (NONE : string option)
784 fun changecwd_dir newdirpath =
786 val newdir = File.platform_path newdirpath
788 (case (!current_working_dir) of
790 | SOME dir => ThyLoad.del_path dir;
791 ThyLoad.add_path newdir;
792 current_working_dir := SOME newdir)
796 fun changecwd (Changecwd vs) =
799 val newdir = PgipTypes.path_of_pgipurl url
804 fun openfile (Openfile vs) =
807 val filepath = PgipTypes.path_of_pgipurl url
808 val filedir = Path.dir filepath
809 val thy_name = Path.implode o #1 o Path.split_ext o Path.base
810 val openfile_retract = Output.no_warnings_CRITICAL
811 (ThyInfo.if_known_thy ThyInfo.remove_thy) o thy_name;
813 case !currently_open_file of
814 SOME f => raise PGIP ("<openfile> when a file is already open!\nCurrently open file: " ^
815 PgipTypes.string_of_pgipurl url)
816 | NONE => (openfile_retract filepath;
817 changecwd_dir filedir;
818 priority ("Working in file: " ^ PgipTypes.string_of_pgipurl url);
819 currently_open_file := SOME url)
823 case !currently_open_file of
824 SOME f => (proper_inform_file_processed f (Isar.state());
825 priority ("Finished working in file: " ^ PgipTypes.string_of_pgipurl f);
826 currently_open_file := NONE)
827 | NONE => raise PGIP ("<closefile> when no file is open!")
829 fun loadfile (Loadfile vs) =
833 (* da: this doesn't seem to cause a problem, batch loading uses
834 a different state context. Of course confusion is still possible,
835 e.g. file loaded depends on open file which is not yet saved. *)
836 (* case !currently_open_file of
837 SOME f => raise PGIP ("<loadfile> when a file is open!\nCurrently open file: " ^
838 PgipTypes.string_of_pgipurl url)
840 use_thy_or_ml_file (File.platform_path url)
844 case !currently_open_file of
845 SOME f => (isarcmd "init_toplevel";
846 priority ("Aborted working in file: " ^
847 PgipTypes.string_of_pgipurl f);
848 currently_open_file := NONE)
849 | NONE => raise PGIP ("<abortfile> when no file is open!")
851 fun retractfile (Retractfile vs) =
855 case !currently_open_file of
856 SOME f => raise PGIP ("<retractfile> when a file is open!")
857 | NONE => (priority ("Retracting file: " ^ PgipTypes.string_of_pgipurl url);
858 (* TODO: next should be in thy loader, here just for testing *)
860 val name = thy_name url
861 in List.app (tell_file_retracted false) (ThyInfo.loaded_files name) end;
862 inform_file_retracted url)
868 fun systemcmd (Systemcmd vs) =
876 fun quitpgip _ = raise PGIP_QUIT
878 fun process_input inp = case inp
879 of Pgip.Askpgip _ => askpgip inp
880 | Pgip.Askpgml _ => askpgml inp
881 | Pgip.Askprefs _ => askprefs inp
882 | Pgip.Askconfig _ => askconfig inp
883 | Pgip.Getpref _ => getpref inp
884 | Pgip.Setpref _ => setpref inp
885 | Pgip.Proverinit _ => proverinit inp
886 | Pgip.Proverexit _ => proverexit inp
887 | Pgip.Setproverflag _ => setproverflag inp
888 | Pgip.Dostep _ => dostep inp
889 | Pgip.Undostep _ => undostep inp
890 | Pgip.Redostep _ => redostep inp
891 | Pgip.Forget _ => error "<forget> not implemented by Isabelle"
892 | Pgip.Restoregoal _ => error "<restoregoal> not implemented by Isabelle"
893 | Pgip.Abortgoal _ => abortgoal inp
894 | Pgip.Askids _ => askids inp
895 | Pgip.Askrefs _ => askrefs inp
896 | Pgip.Showid _ => showid inp
897 | Pgip.Askguise _ => askguise inp
898 | Pgip.Parsescript _ => parsescript inp
899 | Pgip.Showproofstate _ => showproofstate inp
900 | Pgip.Showctxt _ => showctxt inp
901 | Pgip.Searchtheorems _ => searchtheorems inp
902 | Pgip.Setlinewidth _ => setlinewidth inp
903 | Pgip.Viewdoc _ => viewdoc inp
904 | Pgip.Doitem _ => doitem inp
905 | Pgip.Undoitem _ => undoitem inp
906 | Pgip.Redoitem _ => redoitem inp
907 | Pgip.Aborttheory _ => aborttheory inp
908 | Pgip.Retracttheory _ => retracttheory inp
909 | Pgip.Loadfile _ => loadfile inp
910 | Pgip.Openfile _ => openfile inp
911 | Pgip.Closefile _ => closefile inp
912 | Pgip.Abortfile _ => abortfile inp
913 | Pgip.Retractfile _ => retractfile inp
914 | Pgip.Changecwd _ => changecwd inp
915 | Pgip.Systemcmd _ => systemcmd inp
916 | Pgip.Quitpgip _ => quitpgip inp
919 fun process_pgip_element pgipxml =
921 xml as (XML.Elem elem) =>
922 (case Pgip.input elem of
923 NONE => warning ("Unrecognized PGIP command, ignored: \n" ^
925 | SOME inp => (process_input inp)) (* errors later; packet discarded *)
926 | XML.Text t => ignored_text_warning t
927 and ignored_text_warning t =
928 if size (Symbol.strip_blanks t) > 0 then
929 warning ("Ignored text in PGIP packet: \n" ^ t)
932 fun process_pgip_tree xml =
936 XML.Elem ("pgip", attrs, pgips) =>
938 val class = PgipTypes.get_attr "class" attrs
939 val dest = PgipTypes.get_attr_opt "destid" attrs
940 val seq = PgipTypes.read_pgipnat (PgipTypes.get_attr "seq" attrs)
941 (* Respond to prover broadcasts, or messages for us. Ignore rest *)
945 | SOME id => matching_pgip_id id
947 (pgip_refid := PgipTypes.get_attr_opt "id" attrs;
948 pgip_refseq := SOME seq;
949 List.app process_pgip_element pgips;
950 (* return true to indicate <ready/> *)
953 (* no response to ignored messages. *)
956 | _ => raise PGIP "Invalid PGIP packet received")
958 (Output.error_msg ((msg ^ "\nPGIP error occured in XML text below:\n") ^
959 (XML.string_of xml));
964 val process_pgip_plain = K () o process_pgip_tree o XML.parse
966 (* PGIP loop: process PGIP input only *)
974 val _ = if ready then issue_pgip (Ready ()) else ()
976 (case try Source.get_single src of
978 | NONE => raise XML_PARSE)
982 | SOME (pgip,src') =>
984 val ready' = (process_pgip_tree pgip)
985 handle PGIP_QUIT => raise PGIP_QUIT
986 | e => (handler (e,SOME src'); true)
990 end handle e => handler (e,SOME src) (* error in XML parse or Ready issue *)
992 and handler (e,srco) =
994 (XML_PARSE,SOME src) =>
995 panic "Invalid XML input, aborting" (* TODO: attempt recovery *)
996 | (Exn.Interrupt,SOME src) =>
997 (Output.error_msg "Interrupt during PGIP processing"; loop true src)
998 | (Toplevel.UNDEF,SOME src) =>
999 (Output.error_msg "No working context defined"; loop true src)
1001 (Output.error_msg (ML_Compiler.exn_message e); loop true src)
1002 | (PGIP_QUIT,_) => ()
1005 (* TODO: add socket interface *)
1007 val xmlP = XML.parse_comments |-- XML.parse_element >> single
1009 val tty_src = Source.set_prompt "" (Source.source Symbol.stopper xmlP NONE Source.tty)
1011 fun pgip_toplevel x = loop true x
1015 (* Extra command for embedding prover-control inside document (obscure/debug usage). *)
1017 fun init_outer_syntax () =
1018 OuterSyntax.improper_command "ProofGeneral.process_pgip" "(internal)" OuterKeyword.control
1019 (OuterParse.text >> (Toplevel.no_timing oo
1020 (fn txt => Toplevel.imperative (fn () => process_pgip_plain txt))));
1025 val initialized = Unsynchronized.ref false;
1027 fun init_pgip false = panic "No Proof General interface support for Isabelle/classic mode."
1029 (! initialized orelse
1030 (setup_preferences_tweak ();
1031 Output.add_mode proof_generalN Output.default_output Output.default_escape;
1032 Markup.add_mode proof_generalN YXML.output_markup;
1034 Output.no_warnings_CRITICAL init_outer_syntax ();
1035 setup_thy_loader ();
1036 setup_present_hook ();
1037 init_pgip_session_id ();
1039 Unsynchronized.set initialized);
1041 Unsynchronized.change print_mode (update (op =) proof_generalN);
1042 pgip_toplevel tty_src);
1046 (** Out-of-loop PGIP commands (for Emacs hybrid mode) **)
1049 val pgip_output_channel = Unsynchronized.ref Output.writeln_default
1052 (* Set recipient for PGIP results *)
1053 fun init_pgip_channel writefn =
1054 (init_pgip_session_id();
1055 pgip_output_channel := writefn)
1057 (* Process a PGIP command.
1058 This works for preferences but not generally guaranteed
1059 because we haven't done full setup here (e.g., no pgml mode) *)
1060 fun process_pgip str =
1061 setmp_CRITICAL output_xml_fn (!pgip_output_channel) process_pgip_plain str