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 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 *)
25 structure ProofGeneralPgip : PROOF_GENERAL_PGIP =
33 val proof_generalN = "ProofGeneral";
34 val pgmlsymbols_flag = ref true;
41 fun xsym_output "\\" = "\\\\"
42 | xsym_output s = if Symbol.is_raw s then Symbol.decode_raw s else s;
45 (case Symbol.decode s of
46 Symbol.Char s => XML.text s
48 let val ascii = implode (map xsym_output (Symbol.explode s))
49 in if !pgmlsymbols_flag then XML.element "sym" [("name", sn)] [XML.text ascii]
51 | Symbol.Ctrl sn => XML.element "ctrl" [("name", sn)] [XML.text sn] (* FIXME: no such PGML *)
52 | Symbol.Raw raw => raw);
55 let val syms = Symbol.explode str
56 in (implode (map pgml_sym syms), Symbol.length syms) end;
60 fun setup_proofgeneral_output () =
61 Output.add_mode proof_generalN pgml_output Symbol.encode_raw;
66 (* token translations *)
70 val class_tag = "class"
71 val tfree_tag = "tfree"
74 val bound_tag = "bound"
76 val skolem_tag = "skolem"
78 fun xml_atom kind x = XML.element "atom" [("kind", kind)] [XML.text x];
81 (xml_atom kind x, Symbol.length (Symbol.explode x));
83 fun free_or_skolem x =
84 (case try Name.dest_skolem x of
85 NONE => tagit free_tag x
86 | SOME x' => tagit skolem_tag x');
89 (case Lexicon.read_variable s of
91 (case try Name.dest_skolem x of
92 NONE => tagit var_tag s
93 | SOME x' => tagit skolem_tag
94 (setmp show_question_marks true Term.string_of_vname (x', i)))
95 | NONE => tagit var_tag s);
97 val proof_general_trans =
98 Syntax.tokentrans_mode proof_generalN
99 [("class", tagit class_tag),
100 ("tfree", tagit tfree_tag),
101 ("tvar", tagit tvar_tag),
102 ("free", free_or_skolem),
103 ("bound", tagit bound_tag),
104 ("var", var_or_skolem)];
108 val _ = Context.add_setup (Sign.add_tokentrfuns proof_general_trans);
113 (* assembling and issuing PGIP packets *)
115 val pgip_refid = ref NONE: string option ref;
116 val pgip_refseq = ref NONE: int option ref;
119 val pgip_class = "pg"
120 val pgip_tag = "Isabelle/Isar"
123 fun pgip_serial () = inc pgip_seq
125 fun assemble_pgips pgips =
126 Pgip { tag = SOME pgip_tag,
130 destid = !pgip_refid,
131 (* destid=refid since Isabelle only communicates back to sender *)
133 refseq = !pgip_refseq,
137 fun init_pgip_session_id () =
138 pgip_id := getenv "HOSTNAME" ^ "/" ^ getenv "USER" ^ "/" ^
139 getenv "ISABELLE_PID" ^ "/" ^ Time.toString (Time.now ())
141 fun matching_pgip_id id = (id = !pgip_id)
143 val output_xml_fn = ref Output.writeln_default
144 fun output_xml s = (!output_xml_fn) (XML.string_of_tree s); (* TODO: string buffer *)
147 XML.string_of_tree o PgipOutput.output o assemble_pgips o map PgipOutput.output;
149 val output_pgmlterm =
150 XML.string_of_tree o Pgml.pgmlterm_to_xml;
152 val output_pgmltext =
153 XML.string_of_tree o Pgml.pgml_to_xml;
156 fun issue_pgip_rawtext str =
157 output_xml (PgipOutput.output (assemble_pgips [XML.Output str]))
159 fun issue_pgips pgipops =
160 output_xml (PgipOutput.output (assemble_pgips (map PgipOutput.output pgipops)));
162 fun issue_pgip pgipop =
163 output_xml (PgipOutput.output (assemble_pgips [PgipOutput.output pgipop]));
168 fun pgml area terms = Pgml.Pgml { version=NONE,systemid=NONE,
169 area=SOME area, content=terms }
171 (** messages and notification **)
174 val delay_msgs = ref false (*true: accumulate messages*)
175 val delayed_msgs = ref []
177 fun queue_or_issue pgip =
179 delayed_msgs := pgip :: ! delayed_msgs
182 fun wrap_pgml area s =
183 if String.isPrefix "<pgml" s then
184 XML.Output s (* already pgml outermost *)
186 Pgml.pgml_to_xml (pgml area [Pgml.Raw (XML.Output s)]) (* mixed *)
189 fun normalmsg area s =
191 val content = wrap_pgml area s
192 val pgip = Normalresponse { content=[content] }
197 fun errormsg area fatality s =
199 val content = wrap_pgml area s
200 val pgip = Errorresponse { fatality=fatality,
207 (* Error responses with useful locations *)
208 fun error_with_pos area fatality pos s =
210 val content = wrap_pgml area s
211 val pgip = Errorresponse { fatality=fatality,
212 location=SOME (PgipIsabelle.location_of_position pos),
218 fun start_delay_msgs () = (set delay_msgs; delayed_msgs := [])
219 fun end_delayed_msgs () = (reset delay_msgs; ! delayed_msgs)
222 (* NB: all of the standard error/message functions now expect already-escaped text.
223 FIXME: this may cause us problems now we're generating trees; on the other
224 hand the output functions were tuned some time ago, so it ought to be
225 enough to use XML.Output always above. *)
226 (* NB 2: all of standard functions print strings terminated with new lines, but we don't
227 add new lines explicitly in PGIP: they are left implicit. It means that PGIP messages
228 can't be written without newlines. *)
230 fun setup_messages () =
231 (Output.writeln_fn := (fn s => normalmsg Message s);
232 Output.priority_fn := (fn s => normalmsg Status s);
233 Output.tracing_fn := (fn s => normalmsg Tracing s);
234 Output.warning_fn := (fn s => errormsg Message Warning s);
235 Output.error_fn := (fn s => errormsg Message Fatal s);
236 Output.debug_fn := (fn s => errormsg Message Debug s));
238 fun panic s = (errormsg Message Panic ("## SYSTEM EXIT ##\n" ^ s); exit 1);
239 fun nonfatal_error s = errormsg Message Nonfatal s;
240 fun log_msg s = errormsg Message Log s;
243 (* immediate messages *)
245 fun tell_clear_goals () =
246 issue_pgip (Normalresponse { content = [Pgml.pgml_to_xml (pgml Display [])] })
247 fun tell_clear_response () =
248 issue_pgip (Normalresponse { content = [Pgml.pgml_to_xml (pgml Message [])] })
250 fun tell_file_loaded completed path =
251 issue_pgip (Informfileloaded {url=PgipTypes.pgipurl_of_path path,
252 completed=completed})
253 fun tell_file_outdated completed path =
254 issue_pgip (Informfileoutdated {url=PgipTypes.pgipurl_of_path path,
255 completed=completed})
256 fun tell_file_retracted completed path =
257 issue_pgip (Informfileretracted {url=PgipTypes.pgipurl_of_path path,
258 completed=completed})
267 val pgmlterms_no_text= [Pgml.Raw (XML.Output no_text)]
269 fun split_markup text =
270 (case space_explode no_text text of
272 | _ => (error ("Internal error: failed to split XML markup:\n" ^ text); ("", "")));
275 fun block_markup markup =
277 val pgml = Pgml.Box { orient = NONE,
278 indent = Markup.get_int markup Markup.indentN,
279 content = pgmlterms_no_text }
280 in split_markup (output_pgmlterm pgml) end;
282 fun break_markup markup =
284 val pgml = Pgml.Break { mandatory = NONE,
285 indent = Markup.get_int markup Markup.widthN }
286 in (output_pgmlterm pgml, "") end;
288 fun fbreak_markup markup =
290 val pgml = Pgml.Break { mandatory = SOME true, indent = NONE }
291 in (output_pgmlterm pgml, "") end;
294 split_markup (output_pgmltext (pgml PgipTypes.Display pgmlterms_no_text))
296 fun proof_general_markup (markup as (name, _)) =
297 if name = Markup.blockN then block_markup markup
298 else if name = Markup.breakN then break_markup markup
299 else if name = Markup.fbreakN then fbreak_markup markup
300 (* else if name = Markup.classN then class_markup markup
301 else if name = Markup.tyconN then tycon_markup markup
302 else if name = Markup.constN then const_markup markup
303 else if name = Markup.axiomN then axiom_markup markup
304 else if name = Markup.sortN then sort_markup markup
305 else if name = Markup.typN then typ_markup markup
306 else if name = Markup.termN then term_markup markup
307 else if name = Markup.keywordN then keyword_markup markup
308 else if name = Markup.commandN then command_markup markup
309 else if name = Markup.promptN then prompt_markup markup *)
310 else if name = Markup.stateN then state_markup
311 (* else if name = Markup.subgoalN then subgoal_markup () *)
316 val _ = Markup.add_mode proof_generalN proof_general_markup;
321 (* theory loader actions *)
324 (* da: TODO: PGIP has a completed flag so the prover can indicate to the
325 interface which files are busy performing a particular action.
326 To make use of this we need to adjust the hook in thy_info.ML
327 (may actually be difficult to tell the interface *which* action is in
328 progress, but we could add a generic "Lock" action which uses
329 informfileloaded: the broker/UI should not infer too much from incomplete
332 fun trace_action action name =
333 if action = ThyInfo.Update then
334 List.app (tell_file_loaded true) (ThyInfo.loaded_files name)
335 else if action = ThyInfo.Outdate then
336 List.app (tell_file_outdated true) (ThyInfo.loaded_files name)
337 else if action = ThyInfo.Remove then
338 List.app (tell_file_retracted true) (ThyInfo.loaded_files name)
343 fun setup_thy_loader () = ThyInfo.add_hook trace_action;
344 fun sync_thy_loader () = List.app (trace_action ThyInfo.Update) (ThyInfo.names ());
348 (* get informed about files *)
350 val thy_name = Path.implode o #1 o Path.split_ext o Path.base;
352 val inform_file_retracted = ThyInfo.if_known_thy ThyInfo.remove_thy o thy_name;
353 val inform_file_processed = ThyInfo.if_known_thy ThyInfo.touch_child_thys o thy_name;
355 fun proper_inform_file_processed path state =
356 let val name = thy_name path in
357 if Toplevel.is_toplevel state andalso ThyInfo.known_thy name then
358 (ThyInfo.touch_child_thys name;
359 ThyInfo.register_thy name handle ERROR msg =>
360 (warning (cat_lines [msg, "Failed to register theory: " ^ quote name]);
361 tell_file_retracted true (Path.base path)))
362 else raise Toplevel.UNDEF
366 (* restart top-level loop (keeps most state information) *)
368 val welcome = priority o Session.welcome;
373 tell_clear_response ();
375 raise Toplevel.RESTART)
378 (* theorem dependency output *)
380 val show_theorem_dependencies = ref false;
384 val spaces_quote = space_implode " " o map quote;
386 fun thm_deps_message (thms, deps) =
388 val valuethms = XML.Elem("value",[("name", "thms")],[XML.Text thms])
389 val valuedeps = XML.Elem("value",[("name", "deps")],[XML.Text deps])
391 issue_pgip (Metainforesponse {attrs=[("infotype", "isabelle_theorem_dependencies")],
392 content=[valuethms,valuedeps]})
395 fun tell_thm_deps ths =
396 if !show_theorem_dependencies then
398 val names = map PureThy.get_name_hint (filter PureThy.has_name_hint ths);
399 val deps = (Symtab.keys (fold Proofterm.thms_of_proof'
400 (map Thm.proof_of ths) Symtab.empty))
402 if null names orelse null deps then ()
403 else thm_deps_message (spaces_quote names, spaces_quote deps)
409 fun setup_present_hook () =
410 Present.add_hook (fn _ => fn res => tell_thm_deps (maps #2 res));
414 (** lexicalstructure element with keywords (PGIP version of elisp keywords file) **)
416 fun lexicalstructure_keywords () =
417 let val commands = OuterSyntax.dest_keywords ()
418 fun category_of k = if k mem commands then "major" else "minor"
419 (* NB: we might filter to only include words like elisp case (OuterSyntax.is_keyword). *)
420 fun keyword_elt (keyword,help,kind,_) =
421 XML.Elem("keyword", [("word", keyword), ("category", category_of kind)],
422 [XML.Elem("shorthelp", [], [XML.Text help])])
424 (* Also, note we don't call init_outer_syntax here to add interface commands,
425 but they should never appear in scripts anyway so it shouldn't matter *)
426 Lexicalstructure {content = map keyword_elt (OuterSyntax.dest_parsers()) }
429 (* TODO: we can issue a lexicalstructure/keyword when the syntax gets extended dynamically;
430 hooks needed in outer_syntax.ML to do that. *)
433 (* Configuration: GUI config, proverinfo messages *)
436 val isabellewww = "http://isabelle.in.tum.de/"
437 val staticconfig = "~~/lib/ProofGeneral/pgip_isar.xml"
438 fun orenv v d = case getenv v of "" => d | s => s
439 fun config_file() = orenv "ISABELLE_PGIPCONFIG" staticconfig
440 fun isabelle_www() = orenv "ISABELLE_HOMEPAGE" isabellewww
442 fun send_pgip_config () =
444 val path = Path.explode (config_file())
445 val ex = File.exists path
448 (Url.explode (isabelle_www()))
450 (panic ("Error in URL in environment variable ISABELLE_HOMEPAGE.");
451 Url.explode isabellewww)
454 Proverinfo { name = "Isabelle",
456 instance = Session.name(),
457 descr = "The Isabelle/Isar theorem prover",
459 filenameextns = ".thy;" }
462 (issue_pgip proverinfo;
463 issue_pgip_rawtext (File.read path);
464 issue_pgip (lexicalstructure_keywords()))
465 else panic ("PGIP configuration file \"" ^ config_file() ^ "\" not found")
470 (* Preferences: tweak for PGIP interfaces *)
472 val preferences = ref Preferences.preferences;
474 fun setup_preferences_tweak() =
476 (!preferences |> Preferences.set_default ("show-question-marks","false")
477 |> Preferences.remove "show-question-marks" (* we use markup, not ?s *)
478 |> Preferences.remove "theorem-dependencies" (* set internally *)
479 |> Preferences.remove "full-proofs") (* set internally *)
483 (* Sending commands to Isar *)
486 s |> OuterSyntax.scan |> OuterSyntax.read
487 (*|> map (Toplevel.position Position.none o #3)*)
492 - apply a command given a transition function, e.g. IsarCmd.undo.
493 - fix position from path of currently open file [line numbers risk garbling though].
496 (* load an arbitrary file (must be .thy or .ML) *)
498 fun use_thy_or_ml_file file =
500 val (path,extn) = Path.split_ext (Path.explode file)
503 "" => isarcmd ("use_thy " ^ quote (Path.implode path))
504 | "thy" => isarcmd ("use_thy " ^ quote (Path.implode path))
505 | "ML" => isarcmd ("use " ^ quote file)
506 | other => error ("Don't know how to read a file with extension " ^ quote other)
510 (******* PGIP actions *******)
513 (* Responses to each of the PGIP input commands.
514 These are programmed uniformly for extensibility. *)
516 fun askpgip (Askpgip _) =
518 (Usespgip { version = PgipIsabelle.isabelle_pgip_version_supported,
519 pgipelems = PgipIsabelle.accepted_inputs });
522 fun askpgml (Askpgml _) =
524 (Usespgml { version = PgipIsabelle.isabelle_pgml_version_supported })
526 fun askprefs (Askprefs _) =
528 fun preference_of {name, descr, default, pgiptype, get, set } =
529 { name = name, descr = SOME descr, default = SOME default,
530 pgiptype = pgiptype }
532 List.app (fn (prefcat, prefs) =>
533 issue_pgip (Hasprefs {prefcategory=SOME prefcat,
534 prefs=map preference_of prefs}))
538 fun askconfig (Askconfig _) = () (* TODO: add config response *)
541 fun lookuppref pref =
542 case AList.lookup (op =)
543 (map (fn p => (#name p,p))
544 (maps snd (!preferences))) pref of
545 NONE => error ("Unknown prover preference: " ^ quote pref)
548 fun setpref (Setpref vs) =
551 val value = #value vs
552 val set = #set (lookuppref name)
557 fun getpref (Getpref vs) =
560 val get = #get (lookuppref name)
562 issue_pgip (Prefval {name=name, value=get ()})
566 fun proverinit _ = restart ()
568 fun proverexit _ = isarcmd "quit"
570 fun set_proverflag_quiet b =
571 isarcmd (if b then "disable_pr" else "enable_pr")
573 fun set_proverflag_pgmlsymbols b =
574 (pgmlsymbols_flag := b;
575 NAMED_CRITICAL "print_mode" (fn () =>
578 remove (op =) Symbol.xsymbolsN mode @ (if b then [Symbol.xsymbolsN] else []))))
580 fun set_proverflag_thmdeps b =
581 (show_theorem_dependencies := b;
582 proofs := (if b then 1 else 2))
584 fun setproverflag (Setproverflag vs) =
586 val flagname = #flagname vs
587 val value = #value vs
590 "quiet" => set_proverflag_quiet value
591 | "pgmlsymbols" => set_proverflag_pgmlsymbols value
592 | "metainfo:thmdeps" => set_proverflag_thmdeps value
593 | _ => log_msg ("Unrecognised prover control flag: " ^
594 (quote flagname) ^ " ignored."))
598 fun dostep (Dostep vs) =
605 fun undostep (Undostep vs) =
607 val times = #times vs
609 isarcmd ("undos_proof " ^ Int.toString times)
612 fun redostep _ = isarcmd "redo"
614 fun abortgoal _ = isarcmd "kill" (* was: ProofGeneral.kill_proof *)
617 (*** PGIP identifier tables ***)
619 (* TODO: these ones should be triggered by hooks after a
620 declaration addition/removal, to be sent automatically. *)
622 fun addids t = issue_pgip (Addids {idtables = [t]})
623 fun delids t = issue_pgip (Delids {idtables = [t]})
625 fun askids (Askids vs) =
627 val url = #url vs (* ask for identifiers within a file *)
628 val thyname = #thyname vs (* ask for identifiers within a theory *)
629 val objtype = #objtype vs (* ask for identifiers of a particular type *)
631 fun idtable ty ctx ids = {objtype=ty,context=ctx,ids=ids}
633 fun setids t = issue_pgip (Setids {idtables = [t]})
635 (* fake one-level nested "subtheories" by picking apart names. *)
637 map fst o NameSpace.extern_table o PureThy.theorems_of o ThyInfo.get_theory
638 val immed_thms_of_thy = filter_out NameSpace.is_qualified o thms_of_thy
639 fun thy_prefix s = case space_explode NameSpace.separator s of
640 x::_::_ => SOME x (* String.find? *)
642 fun subthys_of_thy s =
643 List.foldl (fn (NONE,xs) => xs | (SOME x,xs) => insert op= x xs) []
644 (map thy_prefix (thms_of_thy s))
645 fun subthms_of_thy thy =
646 (case thy_prefix thy of
647 NONE => immed_thms_of_thy thy
648 | SOME prf => filter (String.isPrefix (unprefix (prf ^ NameSpace.separator) thy))
650 val qualified_thms_of_thy = (* for global query with single response *)
651 (map fst) o NameSpace.dest_table o PureThy.theorems_of o ThyInfo.get_theory;
652 (* da: this version is equivalent to my previous, but splits up theorem sets with names
653 that I can't get to access later with get_thm. Anyway, would rather use sets.
654 Is above right way to get qualified names in that case? Filtering required again?
655 map PureThy.get_name_hint o filter PureThy.has_name_hint o
656 map snd o PureThy.thms_of o ThyInfo.get_theory; *)
658 case (thyname,objtype) of
660 setids (idtable ObjFile NONE (ThyInfo.names())) (*FIXME: uris*)
661 | (NONE, SOME ObjFile) =>
662 setids (idtable ObjFile NONE (ThyInfo.names())) (*FIXME: uris*)
663 | (SOME fi, SOME ObjFile) =>
664 setids (idtable ObjTheory (SOME fi) [fi]) (* TODO: check exists *)
665 | (NONE, SOME ObjTheory) =>
666 setids (idtable ObjTheory NONE (ThyInfo.names()))
667 | (SOME thy, SOME ObjTheory) =>
668 setids (idtable ObjTheory (SOME thy) (subthys_of_thy thy))
669 | (SOME thy, SOME ObjTheorem) =>
670 setids (idtable ObjTheorem (SOME thy) (subthms_of_thy thy))
671 | (NONE, SOME ObjTheorem) =>
672 (* A large query, but not unreasonable. ~5000 results for HOL.*)
673 (* Several setids should be allowed, but Eclipse code is currently broken:
674 List.app (fn thy => setids (idtable ObjTheorem (SOME thy) (subthms_of_thy thy)))
676 setids (idtable ObjTheorem NONE (* this one gives ~7000 for HOL *)
677 (maps qualified_thms_of_thy (ThyInfo.names())))
678 | _ => warning ("askids: ignored argument combination")
681 fun askrefs (Askrefs vs) =
683 val url = #url vs (* ask for references of a file (i.e. immediate pre-requisites) *)
684 val thyname = #thyname vs (* ask for references of a theory (other theories) *)
685 val objtype = #objtype vs (* ask for references of a particular type... *)
686 val name = #name vs (* ... with this name *)
688 fun idtable ty ctx ids = {objtype=ty,context=ctx,ids=ids}
690 val thms_of_thy = map fst o PureThy.thms_of o ThyInfo.get_theory
692 val thy_name = Path.implode o #1 o Path.split_ext o Path.base
695 let val thy = thy_name f
696 val filerefs = #uses (ThyLoad.deps_thy (Path.dir f) thy)
698 issue_pgip (Setrefs {url=url, thyname=NONE, objtype=SOME PgipTypes.ObjFile,
699 name=NONE, idtables=[], fileurls=filerefs})
703 let val thyrefs = #imports (ThyLoad.deps_thy Path.current thy)
705 issue_pgip (Setrefs {url=url, thyname=thyname, objtype=SOME PgipTypes.ObjTheory,
706 name=NONE, idtables=[{context=NONE, objtype=PgipTypes.ObjTheory,
707 ids=thyrefs}], fileurls=[]})
710 fun thmrefs thmname =
712 (* TODO: interim: this is probably not right.
713 What we want is mapping onto simple PGIP name/context model. *)
714 val ctx = Toplevel.context_of (Toplevel.get_state()) (* NB: raises UNDEF *)
715 val thy = Context.theory_of_proof ctx
716 val ths = [PureThy.get_thm thy (PureThy.Name thmname)]
717 val deps = filter_out (equal "")
718 (Symtab.keys (fold Proofterm.thms_of_proof
719 (map Thm.proof_of ths) Symtab.empty))
722 else issue_pgip (Setrefs {url=url, thyname=thyname, name=name,
723 objtype=SOME PgipTypes.ObjTheorem,
724 idtables=[{context=NONE, objtype=PgipTypes.ObjTheorem,
725 ids=deps}], fileurls=[]})
728 case (url,thyname,objtype,name) of
729 (SOME file, NONE, _, _) => filerefs file
730 | (_,SOME thy,_,_) => thyrefs thy
731 | (_,_,SOME PgipTypes.ObjTheorem,SOME thmname) => thmrefs thmname
732 | _ => error ("Unimplemented/invalid case of <askrefs>")
737 fun showid (Showid vs) =
739 val thyname = #thyname vs
740 val objtype = #objtype vs
743 val topthy = Toplevel.theory_of o Toplevel.get_state
746 let val comps = NameSpace.explode id
748 (thy::(rest as _::_)) => (ThyInfo.get_theory thy, space_implode "." rest)
749 | [plainid] => (topthy(),plainid)
750 | _ => raise Toplevel.UNDEF (* assert false *)
754 fun idvalue strings =
755 issue_pgip (Idvalue { thyname=thyname, objtype=objtype, name=name,
756 text=[XML.Elem("pgml",[],
757 map XML.Output strings)] })
759 fun string_of_thm th = Output.output
761 (Display.pretty_thm_aux
762 (Sign.pp (Thm.theory_of_thm th))
764 false (* show hyps *)
768 fun strings_of_thm (thy, name) = map string_of_thm (get_thms thy (Name name))
770 val string_of_thy = Output.output o
771 Pretty.string_of o (ProofDisplay.pretty_full_theory false)
773 case (thyname, objtype) of
774 (_,ObjTheory) => idvalue [string_of_thy (ThyInfo.get_theory name)]
775 | (SOME thy, ObjTheorem) => idvalue (strings_of_thm (ThyInfo.get_theory thy, name))
776 | (NONE, ObjTheorem) => idvalue (strings_of_thm (splitthy name))
777 | (_, ot) => error ("Cannot show objects of type "^(PgipTypes.name_of_objtype ot))
780 (*** Inspecting state ***)
782 (* The file which is currently being processed interactively.
783 In the pre-PGIP code, this was informed to Isabelle and the theory loader
784 on completion, but that allows for circularity in case we read
785 ourselves. So PGIP opens the filename at the start of a script.
786 We ought to prevent problems by modifying the theory loader to know
787 about this special status, but for now we just keep a local reference.
790 val currently_open_file = ref (NONE : pgipurl option)
792 fun get_currently_open_file () = ! currently_open_file;
795 (* The "guise" is the PGIP abstraction of the prover's state.
796 The <informguise> message is merely used for consistency checking. *)
798 val openfile = !currently_open_file
800 val topthy = Toplevel.theory_of o Toplevel.get_state
801 val topthy_name = Context.theory_name o topthy
803 val opentheory = SOME (topthy_name()) handle Toplevel.UNDEF => NONE
805 fun topproofpos () = try Toplevel.proof_position_of (Isar.state ());
806 val openproofpos = topproofpos()
808 issue_pgip (Informguise { file = openfile,
810 (* would be nice to get thm name... *)
812 proofpos = openproofpos })
815 fun parsescript (Parsescript vs) =
818 val systemdata = #systemdata vs
819 val location = #location vs (* TODO: extract position *)
821 val _ = start_delay_msgs () (* gather parsing errs/warns *)
822 val doc = OldPgipParser.pgip_parser text
823 (* not yet working: PgipParser.pgip_parser Position.none text *)
824 val errs = end_delayed_msgs ()
826 val sysattrs = PgipTypes.opt_attr "systemdata" systemdata
827 val locattrs = PgipTypes.attrs_of_location location
829 issue_pgip (Parseresult { attrs= sysattrs@locattrs,
831 errs = map PgipOutput.output errs })
834 fun showproofstate _ = isarcmd "pr"
836 fun showctxt _ = isarcmd "print_context"
838 fun searchtheorems (Searchtheorems vs) =
842 isarcmd ("find_theorems " ^ arg)
845 fun setlinewidth (Setlinewidth vs) =
847 val width = #width vs
849 isarcmd ("pretty_setmargin " ^ Int.toString width) (* FIXME: conversion back/forth! *)
852 fun viewdoc (Viewdoc vs) =
856 isarcmd ("print_" ^ arg) (* FIXME: isatool doc?. Return URLs, maybe? *)
861 fun doitem (Doitem vs) =
875 isarcmd "kill" (* was: "init_toplevel" *)
877 fun retracttheory (Retracttheory vs) =
879 val thyname = #thyname vs
881 isarcmd ("kill_thy " ^ quote thyname)
887 (* Path management: we allow theory files to have dependencies in
888 their own directory, but when we change directory for a new file we
889 remove the path. Leaving it there can cause confusion with
890 difference in batch mode.
891 NB: PGIP does not assume that the prover has a load path.
895 val current_working_dir = ref (NONE : string option)
897 fun changecwd_dir newdirpath =
899 val newdir = File.platform_path newdirpath
901 (case (!current_working_dir) of
903 | SOME dir => ThyLoad.del_path dir;
904 ThyLoad.add_path newdir;
905 current_working_dir := SOME newdir)
909 fun changecwd (Changecwd vs) =
912 val newdir = PgipTypes.path_of_pgipurl url
917 fun openfile (Openfile vs) =
920 val filepath = PgipTypes.path_of_pgipurl url
921 val filedir = Path.dir filepath
922 val thy_name = Path.implode o #1 o Path.split_ext o Path.base
923 val openfile_retract = Output.no_warnings (ThyInfo.if_known_thy ThyInfo.remove_thy) o thy_name;
925 case !currently_open_file of
926 SOME f => raise PGIP ("<openfile> when a file is already open!\nCurrently open file: " ^
927 PgipTypes.string_of_pgipurl url)
928 | NONE => (openfile_retract filepath;
929 changecwd_dir filedir;
930 priority ("Working in file: " ^ PgipTypes.string_of_pgipurl url);
931 currently_open_file := SOME url)
935 case !currently_open_file of
936 SOME f => (proper_inform_file_processed f (Isar.state());
937 priority ("Finished working in file: " ^ PgipTypes.string_of_pgipurl f);
938 currently_open_file := NONE)
939 | NONE => raise PGIP ("<closefile> when no file is open!")
941 fun loadfile (Loadfile vs) =
945 (* da: this doesn't seem to cause a problem, batch loading uses
946 a different state context. Of course confusion is still possible,
947 e.g. file loaded depends on open file which is not yet saved. *)
948 (* case !currently_open_file of
949 SOME f => raise PGIP ("<loadfile> when a file is open!\nCurrently open file: " ^
950 PgipTypes.string_of_pgipurl url)
952 use_thy_or_ml_file (File.platform_path url)
956 case !currently_open_file of
957 SOME f => (isarcmd "init_toplevel";
958 priority ("Aborted working in file: " ^
959 PgipTypes.string_of_pgipurl f);
960 currently_open_file := NONE)
961 | NONE => raise PGIP ("<abortfile> when no file is open!")
963 fun retractfile (Retractfile vs) =
967 case !currently_open_file of
968 SOME f => raise PGIP ("<retractfile> when a file is open!")
969 | NONE => (priority ("Retracting file: " ^ PgipTypes.string_of_pgipurl url);
970 (* TODO: next should be in thy loader, here just for testing *)
972 val name = thy_name url
973 in List.app (tell_file_retracted false) (ThyInfo.loaded_files name) end;
974 inform_file_retracted url)
980 fun systemcmd (Systemcmd vs) =
988 fun quitpgip _ = raise PGIP_QUIT
990 fun process_input inp = case inp
991 of Pgip.Askpgip _ => askpgip inp
992 | Pgip.Askpgml _ => askpgml inp
993 | Pgip.Askprefs _ => askprefs inp
994 | Pgip.Askconfig _ => askconfig inp
995 | Pgip.Getpref _ => getpref inp
996 | Pgip.Setpref _ => setpref inp
997 | Pgip.Proverinit _ => proverinit inp
998 | Pgip.Proverexit _ => proverexit inp
999 | Pgip.Setproverflag _ => setproverflag inp
1000 | Pgip.Dostep _ => dostep inp
1001 | Pgip.Undostep _ => undostep inp
1002 | Pgip.Redostep _ => redostep inp
1003 | Pgip.Forget _ => error "<forget> not implemented by Isabelle"
1004 | Pgip.Restoregoal _ => error "<restoregoal> not implemented by Isabelle"
1005 | Pgip.Abortgoal _ => abortgoal inp
1006 | Pgip.Askids _ => askids inp
1007 | Pgip.Askrefs _ => askrefs inp
1008 | Pgip.Showid _ => showid inp
1009 | Pgip.Askguise _ => askguise inp
1010 | Pgip.Parsescript _ => parsescript inp
1011 | Pgip.Showproofstate _ => showproofstate inp
1012 | Pgip.Showctxt _ => showctxt inp
1013 | Pgip.Searchtheorems _ => searchtheorems inp
1014 | Pgip.Setlinewidth _ => setlinewidth inp
1015 | Pgip.Viewdoc _ => viewdoc inp
1016 | Pgip.Doitem _ => doitem inp
1017 | Pgip.Undoitem _ => undoitem inp
1018 | Pgip.Redoitem _ => redoitem inp
1019 | Pgip.Aborttheory _ => aborttheory inp
1020 | Pgip.Retracttheory _ => retracttheory inp
1021 | Pgip.Loadfile _ => loadfile inp
1022 | Pgip.Openfile _ => openfile inp
1023 | Pgip.Closefile _ => closefile inp
1024 | Pgip.Abortfile _ => abortfile inp
1025 | Pgip.Retractfile _ => retractfile inp
1026 | Pgip.Changecwd _ => changecwd inp
1027 | Pgip.Systemcmd _ => systemcmd inp
1028 | Pgip.Quitpgip _ => quitpgip inp
1031 fun process_pgip_element pgipxml =
1033 xml as (XML.Elem elem) =>
1034 (case Pgip.input elem of
1035 NONE => warning ("Unrecognized PGIP command, ignored: \n" ^
1036 (XML.string_of_tree xml))
1037 | SOME inp => (process_input inp)) (* errors later; packet discarded *)
1038 | XML.Text t => ignored_text_warning t
1039 | XML.Output t => ignored_text_warning t
1040 and ignored_text_warning t =
1041 if size (Symbol.strip_blanks t) > 0 then
1042 warning ("Ignored text in PGIP packet: \n" ^ t)
1045 fun process_pgip_tree xml =
1046 (pgip_refid := NONE;
1047 pgip_refseq := NONE;
1049 XML.Elem ("pgip", attrs, pgips) =>
1051 val class = PgipTypes.get_attr "class" attrs
1052 val dest = PgipTypes.get_attr_opt "destid" attrs
1053 val seq = PgipTypes.read_pgipnat (PgipTypes.get_attr "seq" attrs)
1054 (* Respond to prover broadcasts, or messages for us. Ignore rest *)
1057 NONE => class = "pa"
1058 | SOME id => matching_pgip_id id
1059 in if processit then
1060 (pgip_refid := PgipTypes.get_attr_opt "id" attrs;
1061 pgip_refseq := SOME seq;
1062 List.app process_pgip_element pgips;
1063 (* return true to indicate <ready/> *)
1066 (* no response to ignored messages. *)
1069 | _ => raise PGIP "Invalid PGIP packet received")
1071 (Output.error_msg ((msg ^ "\nPGIP error occured in XML text below:\n") ^
1072 (XML.string_of_tree xml));
1075 (* External input *)
1077 val process_pgip_plain = K () o process_pgip_tree o XML.tree_of_string
1079 (* PGIP loop: process PGIP input only *)
1085 fun loop ready src =
1087 val _ = if ready then issue_pgip (Ready ()) else ()
1089 (case try Source.get_single src of
1091 | NONE => raise XML_PARSE)
1095 | SOME (pgip,src') =>
1097 val ready' = (process_pgip_tree pgip)
1098 handle PGIP_QUIT => raise PGIP_QUIT
1099 | e => (handler (e,SOME src'); true)
1103 end handle e => handler (e,SOME src) (* error in XML parse or Ready issue *)
1105 and handler (e,srco) =
1107 (XML_PARSE,SOME src) =>
1108 panic "Invalid XML input, aborting" (* TODO: attempt recovery *)
1109 | (Interrupt,SOME src) =>
1110 (Output.error_msg "Interrupt during PGIP processing"; loop true src)
1111 | (Toplevel.UNDEF,SOME src) =>
1112 (Output.error_msg "No working context defined"; loop true src)
1114 (Output.error_msg (Toplevel.exn_message e); loop true src)
1115 | (PGIP_QUIT,_) => ()
1118 (* TODO: add socket interface *)
1120 val xmlP = XML.scan_comment_whspc |-- XML.parse_elem >> single
1122 val tty_src = Source.set_prompt "" (Source.source Symbol.stopper xmlP NONE Source.tty)
1124 fun pgip_toplevel x = loop true x
1129 (* Extra command for embedding prover-control inside document (obscure/debug usage). *)
1132 OuterSyntax.improper_command "ProofGeneral.process_pgip" "(internal)" OuterKeyword.control
1133 (OuterParse.text >> (Toplevel.no_timing oo
1134 (fn txt => Toplevel.imperative (fn () => process_pgip_plain txt))));
1138 fun init_outer_syntax () = OuterSyntax.add_parsers [process_pgipP];
1146 val initialized = ref false;
1148 fun init_pgip false = panic "No Proof General interface support for Isabelle/classic mode."
1150 (! initialized orelse
1151 (Output.no_warnings init_outer_syntax ();
1152 OldPgipParser.init ();
1153 setup_preferences_tweak ();
1154 setup_proofgeneral_output ();
1156 setup_thy_loader ();
1157 setup_present_hook ();
1158 init_pgip_session_id ();
1162 change print_mode (cons proof_generalN o remove (op =) proof_generalN);
1163 pgip_toplevel tty_src);
1167 (** Out-of-loop PGIP commands (for Emacs hybrid mode) **)
1170 val pgip_output_channel = ref Output.writeln_default
1173 (* Set recipient for PGIP results *)
1174 fun init_pgip_channel writefn =
1175 (init_pgip_session_id();
1176 pgip_output_channel := writefn)
1178 (* Process a PGIP command.
1179 This works for preferences but not generally guaranteed
1180 because we haven't done full setup here (e.g., no pgml mode) *)
1181 fun process_pgip str =
1182 setmp output_xml_fn (!pgip_output_channel) process_pgip_plain str