renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
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}]
120 | pgml_terms (XML.Text text) = map (Pgml.Raw o Pgml.atom_to_xml) (pgml_syms text);
127 fun pgml area content =
128 Pgml.Pgml {version = NONE, systemid = NONE, area = SOME area, content = content};
130 fun message_content default_area s =
132 val body = YXML.parse_body s;
135 [XML.Elem (name, _, _)] =>
136 if name = Markup.stateN then PgipTypes.Display else default_area
137 | _ => default_area);
138 in Pgml.pgml_to_xml (pgml area (maps pgml_terms body)) end;
141 fun normalmsg area s = issue_pgip
142 (Normalresponse {content = [message_content area s]});
144 fun errormsg area fatality s = issue_pgip
145 (Errorresponse {fatality = fatality, location = NONE, content = [message_content area s]});
147 (*error responses with useful locations*)
148 fun error_with_pos area fatality pos s = issue_pgip
151 location = SOME (PgipIsabelle.location_of_position pos),
152 content = [message_content area s]});
154 fun panic s = (errormsg Message Panic ("## SYSTEM EXIT ##\n" ^ s); exit 1);
155 fun nonfatal_error s = errormsg Message Nonfatal s;
156 fun log_msg s = errormsg Message Log s;
158 (* NB: all of standard functions print strings terminated with new lines, but we don't
159 add new lines explicitly in PGIP: they are left implicit. It means that PGIP messages
160 can't be written without newlines. *)
161 fun setup_messages () =
162 (Output.writeln_fn := (fn s => normalmsg Message s);
163 Output.status_fn := (fn _ => ());
164 Output.priority_fn := (fn s => normalmsg Status s);
165 Output.tracing_fn := (fn s => normalmsg Tracing s);
166 Output.warning_fn := (fn s => errormsg Message Warning s);
167 Output.error_fn := (fn s => errormsg Message Fatal s);
168 Output.debug_fn := (fn s => errormsg Message Debug s));
171 (* immediate messages *)
173 fun tell_clear_goals () =
174 issue_pgip (Normalresponse { content = [Pgml.pgml_to_xml (pgml Display [])] })
175 fun tell_clear_response () =
176 issue_pgip (Normalresponse { content = [Pgml.pgml_to_xml (pgml Message [])] })
178 fun tell_file_loaded completed path =
179 issue_pgip (Informfileloaded {url=PgipTypes.pgipurl_of_path path,
180 completed=completed})
181 fun tell_file_outdated completed path =
182 issue_pgip (Informfileoutdated {url=PgipTypes.pgipurl_of_path path,
183 completed=completed})
184 fun tell_file_retracted completed path =
185 issue_pgip (Informfileretracted {url=PgipTypes.pgipurl_of_path path,
186 completed=completed})
189 (* theory loader actions *)
192 (* da: TODO: PGIP has a completed flag so the prover can indicate to the
193 interface which files are busy performing a particular action.
194 To make use of this we need to adjust the hook in thy_info.ML
195 (may actually be difficult to tell the interface *which* action is in
196 progress, but we could add a generic "Lock" action which uses
197 informfileloaded: the broker/UI should not infer too much from incomplete
200 fun trace_action action name =
201 if action = ThyInfo.Update then
202 List.app (tell_file_loaded true) (ThyInfo.loaded_files name)
203 else if action = ThyInfo.Outdate then
204 List.app (tell_file_outdated true) (ThyInfo.loaded_files name)
205 else if action = ThyInfo.Remove then
206 List.app (tell_file_retracted true) (ThyInfo.loaded_files name)
211 fun setup_thy_loader () = ThyInfo.add_hook trace_action;
212 fun sync_thy_loader () = List.app (trace_action ThyInfo.Update) (ThyInfo.get_names ());
216 (* get informed about files *)
218 val thy_name = Path.implode o #1 o Path.split_ext o Path.base;
220 val inform_file_retracted = ThyInfo.if_known_thy ThyInfo.remove_thy o thy_name;
221 val inform_file_processed = ThyInfo.if_known_thy ThyInfo.touch_child_thys o thy_name;
223 fun proper_inform_file_processed path state =
224 let val name = thy_name path in
225 if Toplevel.is_toplevel state andalso ThyInfo.known_thy name then
226 (ThyInfo.touch_child_thys name;
227 ThyInfo.register_thy name handle ERROR msg =>
228 (warning (cat_lines [msg, "Failed to register theory: " ^ quote name]);
229 tell_file_retracted true (Path.base path)))
230 else raise Toplevel.UNDEF
234 (* restart top-level loop (keeps most state information) *)
236 val welcome = priority o Session.welcome;
241 tell_clear_response ();
246 (* theorem dependencies *)
250 fun add_proof_body (PBody {thms, ...}) =
251 thms |> fold (fn (_, (name, _, _)) => name <> "" ? Symtab.update (name, ()));
254 (case Thm.proof_body_of th of
255 PBody {proof = PThm (_, ((name, _, _), body)), ...} =>
256 if Thm.has_name_hint th andalso Thm.get_name_hint th = name
257 then add_proof_body (Future.join body)
259 | body => add_proof_body body);
265 (* FIXME proper derivation names!? *)
266 val names = map Thm.get_name_hint (filter Thm.has_name_hint ths);
267 val deps = Symtab.keys (fold add_thm ths Symtab.empty);
268 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 = Unsynchronized.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' =>
300 if ! show_theorem_dependencies andalso
301 can Toplevel.theory_of state andalso Toplevel.is_theory state'
303 let val (names, deps) = new_thms_deps (Toplevel.theory_of state) (Toplevel.theory_of state') in
304 if null names orelse null deps then ()
305 else thm_deps_message (spaces_quote names, spaces_quote deps)
312 (** lexicalstructure element with keywords (PGIP version of elisp keywords file) **)
314 fun lexicalstructure_keywords () =
315 let val keywords = Keyword.dest_keywords ()
316 val commands = Keyword.dest_commands ()
317 fun keyword_elt kind keyword =
318 XML.Elem("keyword", [("word", keyword), ("category", kind)], [])
320 (* Also, note we don't call init_outer_syntax here to add interface commands,
321 but they should never appear in scripts anyway so it shouldn't matter *)
323 {content = map (keyword_elt "minor") keywords @ map (keyword_elt "major") commands}
326 (* TODO: we can issue a lexicalstructure/keyword when the syntax gets extended dynamically;
327 hooks needed in outer_syntax.ML to do that. *)
330 (* Configuration: GUI config, proverinfo messages *)
333 val isabellewww = "http://isabelle.in.tum.de/"
334 val staticconfig = "~~/lib/ProofGeneral/pgip_isar.xml"
335 fun orenv v d = case getenv v of "" => d | s => s
336 fun config_file() = orenv "ISABELLE_PGIPCONFIG" staticconfig
337 fun isabelle_www() = orenv "ISABELLE_HOMEPAGE" isabellewww
339 fun send_pgip_config () =
341 val path = Path.explode (config_file())
342 val ex = File.exists path
345 (Url.explode (isabelle_www()))
347 (panic ("Error in URL in environment variable ISABELLE_HOMEPAGE.");
348 Url.explode isabellewww)
351 Proverinfo { name = "Isabelle",
352 version = Distribution.version,
353 instance = Session.name(),
354 descr = "The Isabelle/Isar theorem prover",
356 filenameextns = ".thy;" }
359 (issue_pgip proverinfo;
360 issue_pgip_rawtext (File.read path);
361 issue_pgip (lexicalstructure_keywords()))
362 else panic ("PGIP configuration file \"" ^ config_file() ^ "\" not found")
367 (* Preferences: tweak for PGIP interfaces *)
369 val preferences = Unsynchronized.ref Preferences.pure_preferences;
371 fun add_preference cat pref =
372 CRITICAL (fn () => Unsynchronized.change preferences (Preferences.add cat pref));
374 fun setup_preferences_tweak () =
375 CRITICAL (fn () => Unsynchronized.change preferences
376 (Preferences.set_default ("show-question-marks", "false") #>
377 Preferences.remove "show-question-marks" #> (* we use markup, not ?s *)
378 Preferences.remove "theorem-dependencies" #> (* set internally *)
379 Preferences.remove "full-proofs")); (* set internally *)
383 (* Sending commands to Isar *)
385 fun isarcmd s = Isar.>>> (Outer_Syntax.parse Position.none s);
388 - apply a command given a transition function;
389 - fix position from path of currently open file [line numbers risk garbling though].
392 (* load an arbitrary file (must be .thy or .ML) *)
394 fun use_thy_or_ml_file file =
396 val (path,extn) = Path.split_ext (Path.explode file)
399 "" => isarcmd ("use_thy " ^ quote (Path.implode path))
400 | "thy" => isarcmd ("use_thy " ^ quote (Path.implode path))
401 | "ML" => isarcmd ("use " ^ quote file)
402 | other => error ("Don't know how to read a file with extension " ^ quote other)
406 (******* PGIP actions *******)
409 (* Responses to each of the PGIP input commands.
410 These are programmed uniformly for extensibility. *)
412 fun askpgip (Askpgip _) =
414 (Usespgip { version = PgipIsabelle.isabelle_pgip_version_supported,
415 pgipelems = PgipIsabelle.accepted_inputs });
418 fun askpgml (Askpgml _) =
420 (Usespgml { version = PgipIsabelle.isabelle_pgml_version_supported })
422 fun askprefs (Askprefs _) =
424 fun preference_of {name, descr, default, pgiptype, get, set } =
425 { name = name, descr = SOME descr, default = SOME default,
426 pgiptype = pgiptype }
428 List.app (fn (prefcat, prefs) =>
429 issue_pgip (Hasprefs {prefcategory=SOME prefcat,
430 prefs=map preference_of prefs}))
434 fun askconfig (Askconfig _) = () (* TODO: add config response *)
437 fun lookuppref pref =
438 case AList.lookup (op =)
439 (map (fn p => (#name p,p))
440 (maps snd (!preferences))) pref of
441 NONE => error ("Unknown prover preference: " ^ quote pref)
444 fun setpref (Setpref vs) =
447 val value = #value vs
448 val set = #set (lookuppref name)
453 fun getpref (Getpref vs) =
456 val get = #get (lookuppref name)
458 issue_pgip (Prefval {name=name, value=get ()})
462 fun proverinit _ = restart ()
464 fun proverexit _ = isarcmd "quit"
466 fun set_proverflag_quiet b =
467 isarcmd (if b then "disable_pr" else "enable_pr")
469 fun set_proverflag_pgmlsymbols b =
470 (pgmlsymbols_flag := b;
471 NAMED_CRITICAL "print_mode" (fn () =>
472 Unsynchronized.change print_mode
474 remove (op =) Symbol.xsymbolsN mode @ (if b then [Symbol.xsymbolsN] else []))))
476 fun set_proverflag_thmdeps b =
477 (show_theorem_dependencies := b;
478 Proofterm.proofs := (if b then 1 else 2))
480 fun setproverflag (Setproverflag vs) =
482 val flagname = #flagname vs
483 val value = #value vs
486 "quiet" => set_proverflag_quiet value
487 | "pgmlsymbols" => set_proverflag_pgmlsymbols value
488 | "metainfo:thmdeps" => set_proverflag_thmdeps value
489 | _ => log_msg ("Unrecognised prover control flag: " ^
490 (quote flagname) ^ " ignored."))
494 fun dostep (Dostep vs) =
501 fun undostep (Undostep vs) =
503 val times = #times vs
505 isarcmd ("undos_proof " ^ Int.toString times)
508 fun redostep _ = sys_error "redo unavailable"
510 fun abortgoal _ = isarcmd "kill" (* was: ProofGeneral.kill_proof *)
513 (*** PGIP identifier tables ***)
515 (* TODO: these ones should be triggered by hooks after a
516 declaration addition/removal, to be sent automatically. *)
518 fun addids t = issue_pgip (Addids {idtables = [t]})
519 fun delids t = issue_pgip (Delids {idtables = [t]})
524 fun theory_facts name =
525 let val thy = ThyInfo.get_theory name
526 in (map PureThy.facts_of (Theory.parents_of thy), PureThy.facts_of thy) end;
528 fun thms_of_thy name = map fst (theory_facts name |-> Facts.extern_static);
529 fun qualified_thms_of_thy name = map fst (theory_facts name |-> Facts.dest_static);
533 fun askids (Askids vs) =
535 val url = #url vs (* ask for identifiers within a file *)
536 val thyname = #thyname vs (* ask for identifiers within a theory *)
537 val objtype = #objtype vs (* ask for identifiers of a particular type *)
539 fun idtable ty ctx ids = {objtype=ty,context=ctx,ids=ids}
541 fun setids t = issue_pgip (Setids {idtables = [t]})
543 (* fake one-level nested "subtheories" by picking apart names. *)
544 val immed_thms_of_thy = filter_out Long_Name.is_qualified o thms_of_thy
545 fun thy_prefix s = case Long_Name.explode s of
546 x::_::_ => SOME x (* String.find? *)
548 fun subthys_of_thy s =
549 List.foldl (fn (NONE,xs) => xs | (SOME x,xs) => insert op= x xs) []
550 (map thy_prefix (thms_of_thy s))
551 fun subthms_of_thy thy =
552 (case thy_prefix thy of
553 NONE => immed_thms_of_thy thy
554 | SOME prf => filter (String.isPrefix (unprefix (prf ^ Long_Name.separator) thy))
557 case (thyname,objtype) of
559 setids (idtable ObjFile NONE (ThyInfo.get_names())) (*FIXME: uris*)
560 | (NONE, SOME ObjFile) =>
561 setids (idtable ObjFile NONE (ThyInfo.get_names())) (*FIXME: uris*)
562 | (SOME fi, SOME ObjFile) =>
563 setids (idtable ObjTheory (SOME fi) [fi]) (* TODO: check exists *)
564 | (NONE, SOME ObjTheory) =>
565 setids (idtable ObjTheory NONE (ThyInfo.get_names()))
566 | (SOME thy, SOME ObjTheory) =>
567 setids (idtable ObjTheory (SOME thy) (subthys_of_thy thy))
568 | (SOME thy, SOME ObjTheorem) =>
569 setids (idtable ObjTheorem (SOME thy) (subthms_of_thy thy))
570 | (NONE, SOME ObjTheorem) =>
571 (* A large query, but not unreasonable. ~5000 results for HOL.*)
572 (* Several setids should be allowed, but Eclipse code is currently broken:
573 List.app (fn thy => setids (idtable ObjTheorem (SOME thy) (subthms_of_thy thy)))
574 (ThyInfo.get_names()) *)
575 setids (idtable ObjTheorem NONE (* this one gives ~7000 for HOL *)
576 (maps qualified_thms_of_thy (ThyInfo.get_names())))
577 | _ => warning ("askids: ignored argument combination")
582 fun askrefs (Askrefs vs) =
584 val url = #url vs (* ask for references of a file (i.e. immediate pre-requisites) *)
585 val thyname = #thyname vs (* ask for references of a theory (other theories) *)
586 val objtype = #objtype vs (* ask for references of a particular type... *)
587 val name = #name vs (* ... with this name *)
589 fun idtable ty ctx ids = {objtype=ty,context=ctx,ids=ids}
591 val thy_name = Path.implode o #1 o Path.split_ext o Path.base
594 let val thy = thy_name f
595 val filerefs = #uses (ThyLoad.deps_thy (Path.dir f) thy)
597 issue_pgip (Setrefs {url=url, thyname=NONE, objtype=SOME PgipTypes.ObjFile,
598 name=NONE, idtables=[], fileurls=filerefs})
602 let val thyrefs = #imports (ThyLoad.deps_thy Path.current thy)
604 issue_pgip (Setrefs {url=url, thyname=thyname, objtype=SOME PgipTypes.ObjTheory,
605 name=NONE, idtables=[{context=NONE, objtype=PgipTypes.ObjTheory,
606 ids=thyrefs}], fileurls=[]})
609 fun thmrefs thmname =
611 (* TODO: interim: this is probably not right.
612 What we want is mapping onto simple PGIP name/context model. *)
613 val ctx = Toplevel.context_of (Isar.state ()) (* NB: raises UNDEF *)
614 val thy = ProofContext.theory_of ctx
615 val ths = [PureThy.get_thm thy thmname]
616 val deps = #2 (thms_deps ths);
619 else issue_pgip (Setrefs {url=url, thyname=thyname, name=name,
620 objtype=SOME PgipTypes.ObjTheorem,
621 idtables=[{context=NONE, objtype=PgipTypes.ObjTheorem,
622 ids=deps}], fileurls=[]})
625 case (url,thyname,objtype,name) of
626 (SOME file, NONE, _, _) => filerefs file
627 | (_,SOME thy,_,_) => thyrefs thy
628 | (_,_,SOME PgipTypes.ObjTheorem,SOME thmname) => thmrefs thmname
629 | _ => error ("Unimplemented/invalid case of <askrefs>")
634 fun showid (Showid vs) =
636 val thyname = #thyname vs
637 val objtype = #objtype vs
640 val topthy = Toplevel.theory_of o Isar.state
643 let val comps = Long_Name.explode id
645 (thy::(rest as _::_)) => (ThyInfo.get_theory thy, space_implode "." rest)
646 | [plainid] => (topthy(),plainid)
647 | _ => raise Toplevel.UNDEF (* assert false *)
651 fun idvalue strings =
652 issue_pgip (Idvalue { thyname=thyname, objtype=objtype, name=name,
653 text=[XML.Elem("pgml",[],
654 maps YXML.parse_body strings)] })
656 fun strings_of_thm (thy, name) =
657 map (Display.string_of_thm_global thy) (PureThy.get_thms thy name)
659 val string_of_thy = Pretty.string_of o Proof_Display.pretty_full_theory false
661 case (thyname, objtype) of
662 (_, ObjTheory) => idvalue [string_of_thy (ThyInfo.get_theory name)]
663 | (SOME thy, ObjTheorem) => idvalue (strings_of_thm (ThyInfo.get_theory thy, name))
664 | (NONE, ObjTheorem) => idvalue (strings_of_thm (splitthy name))
665 | (_, ot) => error ("Cannot show objects of type "^(PgipTypes.name_of_objtype ot))
668 (*** Inspecting state ***)
670 (* The file which is currently being processed interactively.
671 In the pre-PGIP code, this was informed to Isabelle and the theory loader
672 on completion, but that allows for circularity in case we read
673 ourselves. So PGIP opens the filename at the start of a script.
674 We ought to prevent problems by modifying the theory loader to know
675 about this special status, but for now we just keep a local reference.
678 val currently_open_file = Unsynchronized.ref (NONE : pgipurl option)
680 fun get_currently_open_file () = ! currently_open_file;
683 (* The "guise" is the PGIP abstraction of the prover's state.
684 The <informguise> message is merely used for consistency checking. *)
686 val openfile = !currently_open_file
688 val topthy = Toplevel.theory_of o Isar.state
689 val topthy_name = Context.theory_name o topthy
691 val opentheory = SOME (topthy_name()) handle Toplevel.UNDEF => NONE
693 fun topproofpos () = try Toplevel.proof_position_of (Isar.state ());
694 val openproofpos = topproofpos()
696 issue_pgip (Informguise { file = openfile,
698 (* would be nice to get thm name... *)
700 proofpos = openproofpos })
703 fun parsescript (Parsescript vs) =
706 val systemdata = #systemdata vs
707 val location = #location vs (* TODO: extract position *)
709 val doc = PgipParser.pgip_parser Position.none text
711 val sysattrs = PgipTypes.opt_attr "systemdata" systemdata
712 val locattrs = PgipTypes.attrs_of_location location
714 issue_pgip (Parseresult { attrs= sysattrs@locattrs,
719 fun showproofstate _ = isarcmd "pr"
721 fun showctxt _ = isarcmd "print_context"
723 fun searchtheorems (Searchtheorems vs) =
727 isarcmd ("find_theorems " ^ arg)
730 fun setlinewidth (Setlinewidth vs) =
732 val width = #width vs
734 isarcmd ("pretty_setmargin " ^ Int.toString width) (* FIXME: conversion back/forth! *)
737 fun viewdoc (Viewdoc vs) =
741 isarcmd ("print_" ^ arg) (* FIXME: isabelle doc?. Return URLs, maybe? *)
746 fun doitem (Doitem vs) =
760 isarcmd "kill" (* was: "init_toplevel" *)
762 fun retracttheory (Retracttheory vs) =
764 val thyname = #thyname vs
766 isarcmd ("kill_thy " ^ quote thyname)
772 (* Path management: we allow theory files to have dependencies in
773 their own directory, but when we change directory for a new file we
774 remove the path. Leaving it there can cause confusion with
775 difference in batch mode.
776 NB: PGIP does not assume that the prover has a load path.
780 val current_working_dir = Unsynchronized.ref (NONE : string option)
782 fun changecwd_dir newdirpath =
784 val newdir = File.platform_path newdirpath
786 (case (!current_working_dir) of
788 | SOME dir => ThyLoad.del_path dir;
789 ThyLoad.add_path newdir;
790 current_working_dir := SOME newdir)
794 fun changecwd (Changecwd vs) =
797 val newdir = PgipTypes.path_of_pgipurl url
802 fun openfile (Openfile vs) =
805 val filepath = PgipTypes.path_of_pgipurl url
806 val filedir = Path.dir filepath
807 val thy_name = Path.implode o #1 o Path.split_ext o Path.base
808 val openfile_retract = Output.no_warnings_CRITICAL
809 (ThyInfo.if_known_thy ThyInfo.remove_thy) o thy_name;
811 case !currently_open_file of
812 SOME f => raise PGIP ("<openfile> when a file is already open!\nCurrently open file: " ^
813 PgipTypes.string_of_pgipurl url)
814 | NONE => (openfile_retract filepath;
815 changecwd_dir filedir;
816 priority ("Working in file: " ^ PgipTypes.string_of_pgipurl url);
817 currently_open_file := SOME url)
821 case !currently_open_file of
822 SOME f => (proper_inform_file_processed f (Isar.state());
823 priority ("Finished working in file: " ^ PgipTypes.string_of_pgipurl f);
824 currently_open_file := NONE)
825 | NONE => raise PGIP ("<closefile> when no file is open!")
827 fun loadfile (Loadfile vs) =
831 (* da: this doesn't seem to cause a problem, batch loading uses
832 a different state context. Of course confusion is still possible,
833 e.g. file loaded depends on open file which is not yet saved. *)
834 (* case !currently_open_file of
835 SOME f => raise PGIP ("<loadfile> when a file is open!\nCurrently open file: " ^
836 PgipTypes.string_of_pgipurl url)
838 use_thy_or_ml_file (File.platform_path url)
842 case !currently_open_file of
843 SOME f => (isarcmd "init_toplevel";
844 priority ("Aborted working in file: " ^
845 PgipTypes.string_of_pgipurl f);
846 currently_open_file := NONE)
847 | NONE => raise PGIP ("<abortfile> when no file is open!")
849 fun retractfile (Retractfile vs) =
853 case !currently_open_file of
854 SOME f => raise PGIP ("<retractfile> when a file is open!")
855 | NONE => (priority ("Retracting file: " ^ PgipTypes.string_of_pgipurl url);
856 (* TODO: next should be in thy loader, here just for testing *)
858 val name = thy_name url
859 in List.app (tell_file_retracted false) (ThyInfo.loaded_files name) end;
860 inform_file_retracted url)
866 fun systemcmd (Systemcmd vs) =
874 fun quitpgip _ = raise PGIP_QUIT
876 fun process_input inp = case inp
877 of Pgip.Askpgip _ => askpgip inp
878 | Pgip.Askpgml _ => askpgml inp
879 | Pgip.Askprefs _ => askprefs inp
880 | Pgip.Askconfig _ => askconfig inp
881 | Pgip.Getpref _ => getpref inp
882 | Pgip.Setpref _ => setpref inp
883 | Pgip.Proverinit _ => proverinit inp
884 | Pgip.Proverexit _ => proverexit inp
885 | Pgip.Setproverflag _ => setproverflag inp
886 | Pgip.Dostep _ => dostep inp
887 | Pgip.Undostep _ => undostep inp
888 | Pgip.Redostep _ => redostep inp
889 | Pgip.Forget _ => error "<forget> not implemented by Isabelle"
890 | Pgip.Restoregoal _ => error "<restoregoal> not implemented by Isabelle"
891 | Pgip.Abortgoal _ => abortgoal inp
892 | Pgip.Askids _ => askids inp
893 | Pgip.Askrefs _ => askrefs inp
894 | Pgip.Showid _ => showid inp
895 | Pgip.Askguise _ => askguise inp
896 | Pgip.Parsescript _ => parsescript inp
897 | Pgip.Showproofstate _ => showproofstate inp
898 | Pgip.Showctxt _ => showctxt inp
899 | Pgip.Searchtheorems _ => searchtheorems inp
900 | Pgip.Setlinewidth _ => setlinewidth inp
901 | Pgip.Viewdoc _ => viewdoc inp
902 | Pgip.Doitem _ => doitem inp
903 | Pgip.Undoitem _ => undoitem inp
904 | Pgip.Redoitem _ => redoitem inp
905 | Pgip.Aborttheory _ => aborttheory inp
906 | Pgip.Retracttheory _ => retracttheory inp
907 | Pgip.Loadfile _ => loadfile inp
908 | Pgip.Openfile _ => openfile inp
909 | Pgip.Closefile _ => closefile inp
910 | Pgip.Abortfile _ => abortfile inp
911 | Pgip.Retractfile _ => retractfile inp
912 | Pgip.Changecwd _ => changecwd inp
913 | Pgip.Systemcmd _ => systemcmd inp
914 | Pgip.Quitpgip _ => quitpgip inp
917 fun process_pgip_element pgipxml =
919 xml as (XML.Elem elem) =>
920 (case Pgip.input elem of
921 NONE => warning ("Unrecognized PGIP command, ignored: \n" ^
923 | SOME inp => (process_input inp)) (* errors later; packet discarded *)
924 | XML.Text t => ignored_text_warning t
925 and ignored_text_warning t =
926 if size (Symbol.strip_blanks t) > 0 then
927 warning ("Ignored text in PGIP packet: \n" ^ t)
930 fun process_pgip_tree xml =
934 XML.Elem ("pgip", attrs, pgips) =>
936 val class = PgipTypes.get_attr "class" attrs
937 val dest = PgipTypes.get_attr_opt "destid" attrs
938 val seq = PgipTypes.read_pgipnat (PgipTypes.get_attr "seq" attrs)
939 (* Respond to prover broadcasts, or messages for us. Ignore rest *)
943 | SOME id => matching_pgip_id id
945 (pgip_refid := PgipTypes.get_attr_opt "id" attrs;
946 pgip_refseq := SOME seq;
947 List.app process_pgip_element pgips;
948 (* return true to indicate <ready/> *)
951 (* no response to ignored messages. *)
954 | _ => raise PGIP "Invalid PGIP packet received")
956 (Output.error_msg ((msg ^ "\nPGIP error occurred in XML text below:\n") ^
957 (XML.string_of xml));
962 val process_pgip_plain = K () o process_pgip_tree o XML.parse
964 (* PGIP loop: process PGIP input only *)
972 val _ = if ready then issue_pgip (Ready ()) else ()
974 (case try Source.get_single src of
976 | NONE => raise XML_PARSE)
980 | SOME (pgip,src') =>
982 val ready' = (process_pgip_tree pgip)
983 handle PGIP_QUIT => raise PGIP_QUIT
984 | e => (handler (e,SOME src'); true)
988 end handle e => handler (e,SOME src) (* error in XML parse or Ready issue *)
990 and handler (e,srco) =
992 (XML_PARSE,SOME src) =>
993 panic "Invalid XML input, aborting" (* TODO: attempt recovery *)
994 | (Exn.Interrupt,SOME src) =>
995 (Output.error_msg "Interrupt during PGIP processing"; loop true src)
996 | (Toplevel.UNDEF,SOME src) =>
997 (Output.error_msg "No working context defined"; loop true src)
999 (Output.error_msg (ML_Compiler.exn_message e); loop true src)
1000 | (PGIP_QUIT,_) => ()
1003 (* TODO: add socket interface *)
1005 val xmlP = XML.parse_comments |-- XML.parse_element >> single
1007 val tty_src = Source.set_prompt "" (Source.source Symbol.stopper xmlP NONE Source.tty)
1009 fun pgip_toplevel x = loop true x
1013 (* Extra command for embedding prover-control inside document (obscure/debug usage). *)
1015 fun init_outer_syntax () =
1016 Outer_Syntax.improper_command "ProofGeneral.process_pgip" "(internal)" Keyword.control
1017 (Parse.text >> (Toplevel.no_timing oo
1018 (fn txt => Toplevel.imperative (fn () => process_pgip_plain txt))));
1023 val initialized = Unsynchronized.ref false;
1025 fun init_pgip false = panic "No Proof General interface support for Isabelle/classic mode."
1027 (! initialized orelse
1028 (setup_preferences_tweak ();
1029 Output.add_mode proof_generalN Output.default_output Output.default_escape;
1030 Markup.add_mode proof_generalN YXML.output_markup;
1032 Output.no_warnings_CRITICAL init_outer_syntax ();
1033 setup_thy_loader ();
1034 setup_present_hook ();
1035 init_pgip_session_id ();
1037 Unsynchronized.set initialized);
1039 Unsynchronized.change print_mode (update (op =) proof_generalN);
1040 pgip_toplevel tty_src);
1044 (** Out-of-loop PGIP commands (for Emacs hybrid mode) **)
1047 val pgip_output_channel = Unsynchronized.ref Output.writeln_default
1050 (* Set recipient for PGIP results *)
1051 fun init_pgip_channel writefn =
1052 (init_pgip_session_id();
1053 pgip_output_channel := writefn)
1055 (* Process a PGIP command.
1056 This works for preferences but not generally guaranteed
1057 because we haven't done full setup here (e.g., no pgml mode) *)
1058 fun process_pgip str =
1059 setmp_CRITICAL output_xml_fn (!pgip_output_channel) process_pgip_plain str