# HG changeset patch # User wenzelm # Date 1368469849 -7200 # Node ID 4af6884329cb7117b2612d303bf9fccc75dc2c33 # Parent f1c1d8637216da73bf94f5a560819d952f4c1960 removed obsolete PGIP material; diff -r f1c1d8637216 -r 4af6884329cb src/Pure/ProofGeneral/proof_general_pgip.ML --- a/src/Pure/ProofGeneral/proof_general_pgip.ML Mon May 13 20:26:34 2013 +0200 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML Mon May 13 20:30:49 2013 +0200 @@ -11,12 +11,6 @@ val new_thms_deps: theory -> theory -> string list * string list - (* More message functions... *) - val nonfatal_error : string -> unit (* recoverable (batch) error: carry on scripting *) - val log_msg : string -> unit (* for internal log messages *) - val error_with_pos : PgipTypes.displayarea -> PgipTypes.fatality -> Position.T -> string -> unit - - val get_currently_open_file : unit -> Path.T option (* interface focus *) val add_preference: string -> Preferences.preference -> unit end @@ -32,8 +26,6 @@ (** print mode **) val proof_general_emacsN = "ProofGeneralEmacs"; -val proof_generalN = "ProofGeneral"; -val pgmlsymbols_flag = Unsynchronized.ref true; (* assembling and issuing PGIP packets *) @@ -62,182 +54,11 @@ fun matching_pgip_id id = (id = pgip_id) -val output_xml_fn = Unsynchronized.ref Output.physical_writeln -fun output_xml s = ! output_xml_fn (XML.string_of s); - val output_pgips = XML.string_of o PgipOutput.output o assemble_pgips o map PgipOutput.output; -val output_pgmlterm = XML.string_of o Pgml.pgmlterm_to_xml; -val output_pgmltext = XML.string_of o Pgml.pgml_to_xml; - - -fun issue_pgip_rawtext str = - output_xml (PgipOutput.output (assemble_pgips (YXML.parse_body str))); - -fun issue_pgip pgipop = - output_xml (PgipOutput.output (assemble_pgips [PgipOutput.output pgipop])); - -end; - - - -(** messages and notification **) - -(* PGML terms *) - -local - -fun pgml_sym s = - if ! pgmlsymbols_flag then - (case Symbol.decode s of - Symbol.Sym name => Pgml.Sym {name = name, content = s} - | _ => Pgml.Str s) - else Pgml.Str s; - -val pgml_syms = map pgml_sym o Symbol.explode; - -val token_markups = - [Markup.tfreeN, Markup.tvarN, Markup.freeN, Markup.boundN, Markup.varN, Markup.skolemN]; - -fun get_int props name = - (case Properties.get props name of NONE => NONE | SOME s => Int.fromString s); - -in - -fun pgml_terms (XML.Elem ((name, atts), body)) = - if member (op =) token_markups name then - let val content = pgml_syms (XML.content_of body) - in [Pgml.Atoms {kind = SOME name, content = content}] end - else - let val content = maps pgml_terms body in - if name = Markup.blockN then - [Pgml.Box {orient = NONE, indent = get_int atts Markup.indentN, content = content}] - else if name = Markup.breakN then - [Pgml.Break {mandatory = NONE, indent = get_int atts Markup.widthN}] - else content - end - | pgml_terms (XML.Text text) = map (Pgml.Raw o Pgml.atom_to_xml) (pgml_syms text); - end; -(* messages *) - -fun pgml area content = - Pgml.Pgml {version = NONE, systemid = NONE, area = SOME area, content = content}; - -fun message_content default_area s = - let - val body = YXML.parse_body s; - val area = - (case body of - [XML.Elem ((name, _), _)] => - if name = Markup.stateN then PgipTypes.Display else default_area - | _ => default_area); - in Pgml.pgml_to_xml (pgml area (maps pgml_terms body)) end; - - -fun normalmsg area s = issue_pgip - (Normalresponse {content = [message_content area s]}); - -fun errormsg area fatality s = issue_pgip - (Errorresponse {fatality = fatality, location = NONE, content = [message_content area s]}); - -(*error responses with useful locations*) -fun error_with_pos area fatality pos s = issue_pgip - (Errorresponse { - fatality = fatality, - location = SOME (PgipIsabelle.location_of_position pos), - content = [message_content area s]}); - -fun panic s = (errormsg Message Panic ("## SYSTEM EXIT ##\n" ^ s); exit 1); -fun nonfatal_error s = errormsg Message Nonfatal s; -fun log_msg s = errormsg Message Log s; - -(* NB: all of standard functions print strings terminated with new lines, but we don't - add new lines explicitly in PGIP: they are left implicit. It means that PGIP messages - can't be written without newlines. *) -fun setup_messages () = - (Output.Private_Hooks.writeln_fn := (fn s => normalmsg Message s); - Output.Private_Hooks.status_fn := (fn _ => ()); - Output.Private_Hooks.report_fn := (fn _ => ()); - Output.Private_Hooks.urgent_message_fn := (fn s => normalmsg Status s); - Output.Private_Hooks.tracing_fn := (fn s => normalmsg Tracing s); - Output.Private_Hooks.warning_fn := (fn s => errormsg Message Warning s); - Output.Private_Hooks.error_fn := (fn (_, s) => errormsg Message Fatal s)); - - -(* immediate messages *) - -fun tell_clear_goals () = - issue_pgip (Normalresponse { content = [Pgml.pgml_to_xml (pgml Display [])] }) -fun tell_clear_response () = - issue_pgip (Normalresponse { content = [Pgml.pgml_to_xml (pgml Message [])] }) - -fun tell_file_loaded completed path = - issue_pgip (Informfileloaded {url=PgipTypes.pgipurl_of_path path, - completed=completed}) -fun tell_file_outdated completed path = - issue_pgip (Informfileoutdated {url=PgipTypes.pgipurl_of_path path, - completed=completed}) -fun tell_file_retracted completed path = - issue_pgip (Informfileretracted {url=PgipTypes.pgipurl_of_path path, - completed=completed}) - - -(* theory loader actions *) - -local - (* da: TODO: PGIP has a completed flag so the prover can indicate to the - interface which files are busy performing a particular action. - To make use of this we need to adjust the hook in thy_info.ML - (may actually be difficult to tell the interface *which* action is in - progress, but we could add a generic "Lock" action which uses - informfileloaded: the broker/UI should not infer too much from incomplete - operations). - *) -fun trace_action action name = - if action = Thy_Info.Update then - List.app (tell_file_loaded true) (Thy_Info.loaded_files name) - else if action = Thy_Info.Remove then - List.app (tell_file_retracted true) (Thy_Info.loaded_files name) - else () - - -in - fun setup_thy_loader () = Thy_Info.add_hook trace_action; - fun sync_thy_loader () = List.app (trace_action Thy_Info.Update) (Thy_Info.get_names ()); -end; - - -(* get informed about files *) - -val thy_name = Path.implode o #1 o Path.split_ext o Path.base; - -val inform_file_retracted = Thy_Info.kill_thy o thy_name; - -fun inform_file_processed path state = - let val name = thy_name path in - if Toplevel.is_toplevel state then - Thy_Info.register_thy (Toplevel.end_theory Position.none state) - handle ERROR msg => - (warning (cat_lines [msg, "Failed to register theory: " ^ quote name]); - tell_file_retracted true (Path.base path)) - else raise Toplevel.UNDEF - end; - - -(* restart top-level loop (keeps most state information) *) - -val welcome = Output.urgent_message o Session.welcome; - -fun restart () = - (sync_thy_loader (); - tell_clear_goals (); - tell_clear_response (); - Isar.init (); - welcome ()); - (* theorem dependencies *) @@ -272,91 +93,6 @@ end; -(* theorem dependeny output *) - -val show_theorem_dependencies = Unsynchronized.ref false; - -local - -val spaces_quote = space_implode " " o map quote; - -fun thm_deps_message (thms, deps) = - let - val valuethms = XML.Elem (("value", [("name", "thms")]), [XML.Text thms]); - val valuedeps = XML.Elem (("value", [("name", "deps")]), [XML.Text deps]); - in - issue_pgip (Metainforesponse - {attrs = [("infotype", "isabelle_theorem_dependencies")], - content = [valuethms, valuedeps]}) - end; - -in - -fun setup_present_hook () = Toplevel.add_hook (fn _ => fn state => fn state' => - if ! show_theorem_dependencies andalso - can Toplevel.theory_of state andalso Toplevel.is_theory state' - then - let val (names, deps) = new_thms_deps (Toplevel.theory_of state) (Toplevel.theory_of state') in - if null names orelse null deps then () - else thm_deps_message (spaces_quote names, spaces_quote deps) - end - else ()); - -end; - - -(** lexicalstructure element with keywords (PGIP version of elisp keywords file) **) - -fun lexicalstructure_keywords () = - let val (keywords, commands) = Keyword.dest () - fun keyword_elt kind keyword = - XML.Elem (("keyword", [("word", keyword), ("category", kind)]), []) - in - Lexicalstructure - {content = map (keyword_elt "minor") keywords @ map (keyword_elt "major") commands} - end - -(* TODO: we can issue a lexicalstructure/keyword when the syntax gets extended dynamically; - hooks needed in outer_syntax.ML to do that. *) - - -(* Configuration: GUI config, proverinfo messages *) - -local - val isabellewww = "http://isabelle.in.tum.de/" - val staticconfig = "~~/lib/ProofGeneral/pgip_isar.xml" - fun orenv v d = case getenv v of "" => d | s => s - fun config_file() = orenv "ISABELLE_PGIPCONFIG" staticconfig - fun isabelle_www() = orenv "ISABELLE_HOMEPAGE" isabellewww -in -fun send_pgip_config () = - let - val path = Path.explode (config_file()) - val ex = File.exists path - - val wwwpage = - (Url.explode (isabelle_www())) - handle ERROR _ => - (panic ("Error in URL in environment variable ISABELLE_HOMEPAGE."); - Url.explode isabellewww) - - val proverinfo = - Proverinfo { name = "Isabelle", - version = Distribution.version, - instance = Session.name(), - descr = "The Isabelle/Isar theorem prover", - url = wwwpage, - filenameextns = ".thy;" } - in - if ex then - (issue_pgip proverinfo; - issue_pgip_rawtext (File.read path); - issue_pgip (lexicalstructure_keywords())) - else panic ("PGIP configuration file \"" ^ config_file() ^ "\" not found") - end; -end - - (* Preferences: tweak for PGIP interfaces *) val preferences = Unsynchronized.ref Preferences.pure_preferences; @@ -369,622 +105,8 @@ SOME {set, ...} => set value | NONE => error ("Unknown prover preference: " ^ quote pref)); -fun setup_preferences_tweak () = - CRITICAL (fn () => Unsynchronized.change preferences - (Preferences.set_default ("show-question-marks", "false") #> - Preferences.remove "show-question-marks" #> (* we use markup, not ?s *) - Preferences.remove "theorem-dependencies" #> (* set internally *) - Preferences.remove "full-proofs")); (* set internally *) - - -(* Sending commands to Isar *) - -fun isarcmd s = Isar.>>> (Outer_Syntax.parse Position.none s); - -(* TODO: - - apply a command given a transition function; - - fix position from path of currently open file [line numbers risk garbling though]. -*) - -(* load an arbitrary file (must be .thy or .ML) *) - -fun use_thy_or_ml_file file = - let - val (path,extn) = Path.split_ext (Path.explode file) - in - case extn of - "" => isarcmd ("use_thy " ^ quote (Path.implode path)) - | "thy" => isarcmd ("use_thy " ^ quote (Path.implode path)) - | "ML" => isarcmd ("use " ^ quote file) - | other => error ("Don't know how to read a file with extension " ^ quote other) - end - - -(******* PGIP actions *******) - - -(* Responses to each of the PGIP input commands. - These are programmed uniformly for extensibility. *) - -fun askpgip (Askpgip _) = - (issue_pgip - (Usespgip { version = PgipIsabelle.isabelle_pgip_version_supported, - pgipelems = PgipIsabelle.accepted_inputs }); - send_pgip_config()) - -fun askpgml (Askpgml _) = - issue_pgip - (Usespgml { version = PgipIsabelle.isabelle_pgml_version_supported }) - -fun askprefs (Askprefs _) = - let - fun preference_of {name, descr, default, pgiptype, get, set } = - { name = name, descr = SOME descr, default = SOME default, - pgiptype = pgiptype } - in - List.app (fn (prefcat, prefs) => - issue_pgip (Hasprefs {prefcategory=SOME prefcat, - prefs=map preference_of prefs})) - (!preferences) - end - -fun askconfig (Askconfig _) = () (* TODO: add config response *) - -local - fun lookuppref pref = - case AList.lookup (op =) - (map (fn p => (#name p,p)) - (maps snd (!preferences))) pref of - NONE => error ("Unknown prover preference: " ^ quote pref) - | SOME p => p -in -fun setpref (Setpref vs) = - let - val name = #name vs - val value = #value vs - val set = #set (lookuppref name) - in - set value - end - -fun getpref (Getpref vs) = - let - val name = #name vs - val get = #get (lookuppref name) - in - issue_pgip (Prefval {name=name, value=get ()}) - end -end - -fun proverinit _ = restart () - -fun proverexit _ = isarcmd "quit" - -fun set_proverflag_quiet b = - isarcmd (if b then "disable_pr" else "enable_pr") - -fun set_proverflag_pgmlsymbols b = - (pgmlsymbols_flag := b; - NAMED_CRITICAL "print_mode" (fn () => - Unsynchronized.change print_mode - (fn mode => - remove (op =) Symbol.xsymbolsN mode @ (if b then [Symbol.xsymbolsN] else [])))) - -fun set_proverflag_thmdeps b = - (show_theorem_dependencies := b; - Proofterm.proofs := (if b then 1 else 2)) - -fun setproverflag (Setproverflag vs) = - let - val flagname = #flagname vs - val value = #value vs - in - (case flagname of - "quiet" => set_proverflag_quiet value - | "pgmlsymbols" => set_proverflag_pgmlsymbols value - | "metainfo:thmdeps" => set_proverflag_thmdeps value - | _ => log_msg ("Unrecognised prover control flag: " ^ - (quote flagname) ^ " ignored.")) - end - - -fun dostep (Dostep vs) = - let - val text = #text vs - in - isarcmd text - end - -fun undostep (Undostep vs) = - let - val times = #times vs - in - isarcmd ("undos_proof " ^ string_of_int times) - end - -fun redostep _ = raise Fail "redo unavailable" - -fun abortgoal _ = isarcmd "kill" (* was: ProofGeneral.kill_proof *) - - -(*** PGIP identifier tables ***) - -(* TODO: these ones should be triggered by hooks after a - declaration addition/removal, to be sent automatically. *) - -fun addids t = issue_pgip (Addids {idtables = [t]}) -fun delids t = issue_pgip (Delids {idtables = [t]}) - - -local - -fun theory_facts thy = - (map Global_Theory.facts_of (Theory.parents_of thy), Global_Theory.facts_of thy); - -fun thms_of_thy name = - let val thy = Thy_Info.get_theory name - in map fst (theory_facts thy |-> Facts.extern_static (Proof_Context.init_global thy)) end; - -fun qualified_thms_of_thy name = - map fst (theory_facts (Thy_Info.get_theory name) |-> Facts.dest_static); - -in - -fun askids (Askids vs) = - let - val url = #url vs (* ask for identifiers within a file *) - val thyname = #thyname vs (* ask for identifiers within a theory *) - val objtype = #objtype vs (* ask for identifiers of a particular type *) - - fun idtable ty ctx ids = {objtype=ty,context=ctx,ids=ids} - - fun setids t = issue_pgip (Setids {idtables = [t]}) - - (* fake one-level nested "subtheories" by picking apart names. *) - val immed_thms_of_thy = filter_out Long_Name.is_qualified o thms_of_thy - fun thy_prefix s = case Long_Name.explode s of - x::_::_ => SOME x (* String.find? *) - | _ => NONE - fun subthys_of_thy s = - List.foldl (fn (NONE,xs) => xs | (SOME x,xs) => insert op= x xs) [] - (map thy_prefix (thms_of_thy s)) - fun subthms_of_thy thy = - (case thy_prefix thy of - NONE => immed_thms_of_thy thy - | SOME prf => filter (String.isPrefix (unprefix (prf ^ Long_Name.separator) thy)) - (thms_of_thy prf)) - in - case (thyname,objtype) of - (NONE, NONE) => - setids (idtable ObjFile NONE (Thy_Info.get_names())) (*FIXME: uris*) - | (NONE, SOME ObjFile) => - setids (idtable ObjFile NONE (Thy_Info.get_names())) (*FIXME: uris*) - | (SOME fi, SOME ObjFile) => - setids (idtable ObjTheory (SOME fi) [fi]) (* TODO: check exists *) - | (NONE, SOME ObjTheory) => - setids (idtable ObjTheory NONE (Thy_Info.get_names())) - | (SOME thy, SOME ObjTheory) => - setids (idtable ObjTheory (SOME thy) (subthys_of_thy thy)) - | (SOME thy, SOME ObjTheorem) => - setids (idtable ObjTheorem (SOME thy) (subthms_of_thy thy)) - | (NONE, SOME ObjTheorem) => - (* A large query, but not unreasonable. ~5000 results for HOL.*) - (* Several setids should be allowed, but Eclipse code is currently broken: - List.app (fn thy => setids (idtable ObjTheorem (SOME thy) (subthms_of_thy thy))) - (Thy_Info.get_names()) *) - setids (idtable ObjTheorem NONE (* this one gives ~7000 for HOL *) - (maps qualified_thms_of_thy (Thy_Info.get_names()))) - | _ => warning ("askids: ignored argument combination") - end - -end; - -fun askrefs (Askrefs vs) = - let - val url = #url vs (* ask for references of a file (i.e. immediate pre-requisites) *) - val thyname = #thyname vs (* ask for references of a theory (other theories) *) - val objtype = #objtype vs (* ask for references of a particular type... *) - val name = #name vs (* ... with this name *) - - fun idtable ty ctx ids = {objtype=ty,context=ctx,ids=ids} - - val thy_name = Path.implode o #1 o Path.split_ext o Path.base - - fun filerefs f = - let val thy = thy_name f - in - issue_pgip (Setrefs {url=url, thyname=NONE, objtype=SOME PgipTypes.ObjFile, - name=NONE, idtables=[], fileurls=[]}) - end - - fun thyrefs thy = - let val thyrefs = map #1 (#imports (Thy_Load.check_thy Path.current thy)) - in - issue_pgip (Setrefs {url=url, thyname=thyname, objtype=SOME PgipTypes.ObjTheory, - name=NONE, idtables=[{context=NONE, objtype=PgipTypes.ObjTheory, - ids=thyrefs}], fileurls=[]}) - end - - fun thmrefs thmname = - let - (* TODO: interim: this is probably not right. - What we want is mapping onto simple PGIP name/context model. *) - val ctx = Toplevel.context_of (Isar.state ()) (* NB: raises UNDEF *) - val thy = Proof_Context.theory_of ctx - val ths = [Global_Theory.get_thm thy thmname] - val deps = #2 (thms_deps ths); - in - if null deps then () - else issue_pgip (Setrefs {url=url, thyname=thyname, name=name, - objtype=SOME PgipTypes.ObjTheorem, - idtables=[{context=NONE, objtype=PgipTypes.ObjTheorem, - ids=deps}], fileurls=[]}) - end - in - case (url,thyname,objtype,name) of - (SOME file, NONE, _, _) => filerefs file - | (_,SOME thy,_,_) => thyrefs thy - | (_,_,SOME PgipTypes.ObjTheorem,SOME thmname) => thmrefs thmname - | _ => error ("Unimplemented/invalid case of ") - end - - - -fun showid (Showid vs) = - let - val thyname = #thyname vs - val objtype = #objtype vs - val name = #name vs - - val topthy = Toplevel.theory_of o Isar.state - - fun splitthy id = - let val comps = Long_Name.explode id - in case comps of - (thy::(rest as _::_)) => (Thy_Info.get_theory thy, Long_Name.implode rest) - | [plainid] => (topthy(),plainid) - | _ => raise Toplevel.UNDEF (* assert false *) - end - - - fun idvalue strings = - issue_pgip (Idvalue { thyname=thyname, objtype=objtype, name=name, - text=[XML.Elem (("pgml", []), maps YXML.parse_body strings)] }) - - fun strings_of_thm (thy, name) = - map (Display.string_of_thm_global thy) (Global_Theory.get_thms thy name) - - val string_of_thy = Pretty.string_of o Proof_Display.pretty_full_theory false - in - case (thyname, objtype) of - (_, ObjTheory) => idvalue [string_of_thy (Thy_Info.get_theory name)] - | (SOME thy, ObjTheorem) => idvalue (strings_of_thm (Thy_Info.get_theory thy, name)) - | (NONE, ObjTheorem) => idvalue (strings_of_thm (splitthy name)) - | (_, ot) => error ("Cannot show objects of type "^(PgipTypes.name_of_objtype ot)) - end - -(*** Inspecting state ***) - -(* The file which is currently being processed interactively. - In the pre-PGIP code, this was informed to Isabelle and the theory loader - on completion, but that allows for circularity in case we read - ourselves. So PGIP opens the filename at the start of a script. - We ought to prevent problems by modifying the theory loader to know - about this special status, but for now we just keep a local reference. -*) - -val currently_open_file = Unsynchronized.ref (NONE : pgipurl option) - -fun get_currently_open_file () = ! currently_open_file; - -fun askguise _ = - (* The "guise" is the PGIP abstraction of the prover's state. - The message is merely used for consistency checking. *) - let - val openfile = !currently_open_file - - val topthy = Toplevel.theory_of o Isar.state - val topthy_name = Context.theory_name o topthy - - val opentheory = SOME (topthy_name()) handle Toplevel.UNDEF => NONE - - fun topproofpos () = try Toplevel.proof_position_of (Isar.state ()); - val openproofpos = topproofpos() - in - issue_pgip (Informguise { file = openfile, - theory = opentheory, - (* would be nice to get thm name... *) - theorem = NONE, - proofpos = openproofpos }) - end - -fun parsescript (Parsescript vs) = - let - val text = #text vs - val systemdata = #systemdata vs - val location = #location vs (* TODO: extract position *) - - val doc = PgipParser.pgip_parser Position.none text - - val sysattrs = PgipTypes.opt_attr "systemdata" systemdata - val locattrs = PgipTypes.attrs_of_location location - in - issue_pgip (Parseresult { attrs= sysattrs@locattrs, - doc = doc, - errs = [] }) - end - -fun showproofstate _ = isarcmd "pr" - -fun showctxt _ = isarcmd "print_context" - -fun searchtheorems (Searchtheorems vs) = - let - val arg = #arg vs - in - isarcmd ("find_theorems " ^ arg) - end - -fun setlinewidth (Setlinewidth vs) = - let - val width = #width vs - in - isarcmd ("pretty_setmargin " ^ string_of_int width) (* FIXME: conversion back/forth! *) - end - -fun viewdoc (Viewdoc vs) = - let - val arg = #arg vs - in - isarcmd ("print_" ^ arg) (* FIXME: isabelle doc?. Return URLs, maybe? *) - end - -(*** Theory ***) - -fun doitem (Doitem vs) = - let - val text = #text vs - in - isarcmd text - end - -fun undoitem _ = - isarcmd "undo" - -fun redoitem _ = - isarcmd "redo" - -fun aborttheory _ = - isarcmd "kill" (* was: "init_toplevel" *) - -fun retracttheory (Retracttheory vs) = - let - val thyname = #thyname vs - in - isarcmd ("kill_thy " ^ quote thyname) - end - - -(*** Files ***) - -fun changecwd (Changecwd {url, ...}) = - Thy_Load.set_master_path (PgipTypes.path_of_pgipurl url) - -fun openfile (Openfile vs) = - let - val url = #url vs - val filepath = PgipTypes.path_of_pgipurl url - val filedir = Path.dir filepath - val thy_name = Path.implode o #1 o Path.split_ext o Path.base - val openfile_retract = Thy_Info.kill_thy o thy_name; - in - case !currently_open_file of - SOME f => raise PGIP (" when a file is already open!\nCurrently open file: " ^ - PgipTypes.string_of_pgipurl url) - | NONE => (openfile_retract filepath; - Thy_Load.set_master_path filedir; - Output.urgent_message ("Working in file: " ^ PgipTypes.string_of_pgipurl url); - currently_open_file := SOME url) - end - -fun closefile _ = - case !currently_open_file of - SOME f => (inform_file_processed f (Isar.state ()); - Output.urgent_message - ("Finished working in file: " ^ PgipTypes.string_of_pgipurl f); - currently_open_file := NONE) - | NONE => raise PGIP (" when no file is open!") - -fun loadfile (Loadfile vs) = - let - val url = #url vs - in - (* da: this doesn't seem to cause a problem, batch loading uses - a different state context. Of course confusion is still possible, - e.g. file loaded depends on open file which is not yet saved. *) - (* case !currently_open_file of - SOME f => raise PGIP (" when a file is open!\nCurrently open file: " ^ - PgipTypes.string_of_pgipurl url) - | NONE => *) - use_thy_or_ml_file (File.platform_path url) - end - -fun abortfile _ = - case !currently_open_file of - SOME f => (isarcmd "init_toplevel"; - Output.urgent_message ("Aborted working in file: " ^ - PgipTypes.string_of_pgipurl f); - currently_open_file := NONE) - | NONE => raise PGIP (" when no file is open!") - -fun retractfile (Retractfile vs) = - let - val url = #url vs - in - case !currently_open_file of - SOME f => raise PGIP (" when a file is open!") - | NONE => (Output.urgent_message ("Retracting file: " ^ PgipTypes.string_of_pgipurl url); - (* TODO: next should be in thy loader, here just for testing *) - let - val name = thy_name url - in List.app (tell_file_retracted false) (Thy_Info.loaded_files name) end; - inform_file_retracted url) - end - - -(*** System ***) - -fun systemcmd (Systemcmd vs) = - let - val arg = #arg vs - in - isarcmd arg - end - -exception PGIP_QUIT; -fun quitpgip _ = raise PGIP_QUIT - -fun process_input inp = case inp - of PgipInput.Askpgip _ => askpgip inp - | PgipInput.Askpgml _ => askpgml inp - | PgipInput.Askprefs _ => askprefs inp - | PgipInput.Askconfig _ => askconfig inp - | PgipInput.Getpref _ => getpref inp - | PgipInput.Setpref _ => setpref inp - | PgipInput.Proverinit _ => proverinit inp - | PgipInput.Proverexit _ => proverexit inp - | PgipInput.Setproverflag _ => setproverflag inp - | PgipInput.Dostep _ => dostep inp - | PgipInput.Undostep _ => undostep inp - | PgipInput.Redostep _ => redostep inp - | PgipInput.Forget _ => error " not implemented by Isabelle" - | PgipInput.Restoregoal _ => error " not implemented by Isabelle" - | PgipInput.Abortgoal _ => abortgoal inp - | PgipInput.Askids _ => askids inp - | PgipInput.Askrefs _ => askrefs inp - | PgipInput.Showid _ => showid inp - | PgipInput.Askguise _ => askguise inp - | PgipInput.Parsescript _ => parsescript inp - | PgipInput.Showproofstate _ => showproofstate inp - | PgipInput.Showctxt _ => showctxt inp - | PgipInput.Searchtheorems _ => searchtheorems inp - | PgipInput.Setlinewidth _ => setlinewidth inp - | PgipInput.Viewdoc _ => viewdoc inp - | PgipInput.Doitem _ => doitem inp - | PgipInput.Undoitem _ => undoitem inp - | PgipInput.Redoitem _ => redoitem inp - | PgipInput.Aborttheory _ => aborttheory inp - | PgipInput.Retracttheory _ => retracttheory inp - | PgipInput.Loadfile _ => loadfile inp - | PgipInput.Openfile _ => openfile inp - | PgipInput.Closefile _ => closefile inp - | PgipInput.Abortfile _ => abortfile inp - | PgipInput.Retractfile _ => retractfile inp - | PgipInput.Changecwd _ => changecwd inp - | PgipInput.Systemcmd _ => systemcmd inp - | PgipInput.Quitpgip _ => quitpgip inp - - -fun process_pgip_element pgipxml = - case pgipxml of - xml as (XML.Elem elem) => - (case PgipInput.input elem of - NONE => warning ("Unrecognized PGIP command, ignored: \n" ^ - (XML.string_of xml)) - | SOME inp => (process_input inp)) (* errors later; packet discarded *) - | XML.Text t => ignored_text_warning t -and ignored_text_warning t = - if size (Symbol.strip_blanks t) > 0 then - warning ("Ignored text in PGIP packet: \n" ^ t) - else () - -fun process_pgip_tree xml = - (pgip_refid := NONE; - pgip_refseq := NONE; - (case xml of - XML.Elem (("pgip", attrs), pgips) => - (let - val class = PgipTypes.get_attr "class" attrs - val dest = PgipTypes.get_attr_opt "destid" attrs - val seq = PgipTypes.read_pgipnat (PgipTypes.get_attr "seq" attrs) - (* Respond to prover broadcasts, or messages for us. Ignore rest *) - val processit = - case dest of - NONE => class = "pa" - | SOME id => matching_pgip_id id - in if processit then - (pgip_refid := PgipTypes.get_attr_opt "id" attrs; - pgip_refseq := SOME seq; - List.app process_pgip_element pgips; - (* return true to indicate *) - true) - else - (* no response to ignored messages. *) - false - end) - | _ => raise PGIP "Invalid PGIP packet received") - handle PGIP msg => - (Output.error_msg ((msg ^ "\nPGIP error occurred in XML text below:\n") ^ - (XML.string_of xml)); - true)) - -(* External input *) - -val process_pgip_plain = K () o process_pgip_tree o XML.parse - -(* PGIP loop: process PGIP input only *) - -local - -exception XML_PARSE - -fun loop ready src = - let - val _ = if ready then issue_pgip (Ready ()) else () - val pgipo = - (case try Source.get_single src of - SOME pgipo => pgipo - | NONE => raise XML_PARSE) - in - case pgipo of - NONE => () - | SOME (pgip,src') => - let - val ready' = (process_pgip_tree pgip) - handle PGIP_QUIT => raise PGIP_QUIT - | e => (handler (e,SOME src'); true) - in - loop ready' src' - end - end handle e => handler (e,SOME src) (* error in XML parse or Ready issue *) - -and handler (e,srco) = - if Exn.is_interrupt e andalso is_some srco then - (Output.error_msg "Interrupt during PGIP processing"; loop true (the srco)) - else - case (e,srco) of - (XML_PARSE,SOME src) => - panic "Invalid XML input, aborting" (* TODO: attempt recovery *) - | (Toplevel.UNDEF,SOME src) => - (Output.error_msg "No working context defined"; loop true src) - | (e,SOME src) => - (Output.error_msg (ML_Compiler.exn_message e); loop true src) - | (PGIP_QUIT,_) => () - | (_,NONE) => () -in - (* TODO: add socket interface *) - - val xmlP = XML.parse_comments |-- XML.parse_element >> single - - val tty_src = - Source.set_prompt "" (Source.source Symbol.stopper xmlP NONE (Source.tty TextIO.stdIn)) - - fun pgip_toplevel x = loop true x -end - - -(** Out-of-loop PGIP commands (for Emacs hybrid mode) **) +(** PGIP/Emacs rudiments **) local @@ -994,7 +116,7 @@ fun process_element_emacs (XML.Elem (("askprefs", _), _)) = let - fun preference_of {name, descr, default, pgiptype, get, set} = + fun preference_of {name, descr, default, pgiptype, get = _, set = _} = {name = name, descr = SOME descr, default = SOME default, pgiptype = pgiptype}; in ! preferences |> List.app (fn (prefcat, prefs) => @@ -1040,11 +162,7 @@ val _ = Outer_Syntax.improper_command (("ProofGeneral.process_pgip", Keyword.control), Position.none) "(internal)" - (Parse.text >> - (fn str => Toplevel.imperative (fn () => - if print_mode_active proof_general_emacsN - then process_pgip_emacs str - else process_pgip_plain str))); + (Parse.text >> (fn str => Toplevel.imperative (fn () => process_pgip_emacs str))); end;