removed obsolete PGIP material;
authorwenzelm
Mon, 13 May 2013 20:30:49 +0200
changeset 51965 4af6884329cb
parent 51964 f1c1d8637216
child 51966 0e18eee8c2c2
removed obsolete PGIP material;
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 <askrefs>")
-    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 <informguise> 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 ("<openfile> 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 ("<closefile> 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 ("<loadfile> 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 ("<abortfile> when no file is open!")
-
-fun retractfile (Retractfile vs) =
-    let
-        val url = #url vs
-    in
-        case !currently_open_file of
-            SOME f => raise PGIP ("<retractfile> 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 "<forget> not implemented by Isabelle"
-  | PgipInput.Restoregoal _      => error "<restoregoal> 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 <ready/> *)
-                   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;