src/Pure/ProofGeneral/proof_general_pgip.ML
author wenzelm
Thu Sep 09 17:20:27 2010 +0200 (2010-09-09 ago)
changeset 39232 69c6d3e87660
parent 39139 8235606e2b23
child 39513 fce2202892c4
permissions -rw-r--r--
more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
     1 (*  Title:      Pure/ProofGeneral/proof_general_pgip.ML
     2     Author:     David Aspinall and Markus Wenzel
     3 
     4 Isabelle configuration for Proof General using PGIP protocol.
     5 See http://proofgeneral.inf.ed.ac.uk/kit
     6 *)
     7 
     8 signature PROOF_GENERAL_PGIP =
     9 sig
    10   val proof_general_emacsN: string
    11 
    12   val new_thms_deps: theory -> theory -> string list * string list
    13   val init_pgip: bool -> unit             (* main PGIP loop with true; fail with false *)
    14 
    15   val pgip_channel_emacs: (string -> unit) -> unit
    16 
    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
    21 
    22   val get_currently_open_file : unit -> Path.T option  (* interface focus *)
    23   val add_preference: string -> Preferences.preference -> unit
    24 end
    25 
    26 structure ProofGeneralPgip : PROOF_GENERAL_PGIP =
    27 struct
    28 
    29 open Pgip;
    30 
    31 
    32 (** print mode **)
    33 
    34 val proof_general_emacsN = "ProofGeneralEmacs";
    35 val proof_generalN = "ProofGeneral";
    36 val pgmlsymbols_flag = Unsynchronized.ref true;
    37 
    38 
    39 (* assembling and issuing PGIP packets *)
    40 
    41 val pgip_refid = Unsynchronized.ref NONE: string option Unsynchronized.ref;
    42 val pgip_refseq = Unsynchronized.ref NONE: int option Unsynchronized.ref;
    43 
    44 local
    45   val pgip_class  = "pg"
    46   val pgip_tag = "Isabelle/Isar"
    47   val pgip_id = Unsynchronized.ref ""
    48   val pgip_seq = Unsynchronized.ref 0
    49   fun pgip_serial () = Unsynchronized.inc pgip_seq
    50 
    51   fun assemble_pgips pgips =
    52     Pgip { tag = SOME pgip_tag,
    53            class = pgip_class,
    54            seq = pgip_serial (),
    55            id = ! pgip_id,
    56            destid = ! pgip_refid,
    57            (* destid=refid since Isabelle only communicates back to sender *)
    58            refid = ! pgip_refid,
    59            refseq = ! pgip_refseq,
    60            content = pgips }
    61 in
    62 
    63 fun init_pgip_session_id () =
    64     pgip_id := getenv "HOSTNAME" ^ "/" ^ getenv "USER" ^ "/" ^
    65                getenv "ISABELLE_PID" ^ "/" ^ Time.toString (Time.now ())
    66 
    67 fun matching_pgip_id id = (id = ! pgip_id)
    68 
    69 val output_xml_fn = Unsynchronized.ref Output.writeln_default
    70 fun output_xml s = ! output_xml_fn (XML.string_of s);
    71 
    72 val output_pgips = XML.string_of o PgipOutput.output o assemble_pgips o map PgipOutput.output;
    73 
    74 val output_pgmlterm = XML.string_of o Pgml.pgmlterm_to_xml;
    75 val output_pgmltext = XML.string_of o Pgml.pgml_to_xml;
    76 
    77 
    78 fun issue_pgip_rawtext str =
    79   output_xml (PgipOutput.output (assemble_pgips (YXML.parse_body str)));
    80 
    81 fun issue_pgip pgipop =
    82   output_xml (PgipOutput.output (assemble_pgips [PgipOutput.output pgipop]));
    83 
    84 end;
    85 
    86 
    87 
    88 (** messages and notification **)
    89 
    90 (* PGML terms *)
    91 
    92 local
    93 
    94 fun pgml_sym s =
    95   if ! pgmlsymbols_flag then
    96     (case Symbol.decode s of
    97       Symbol.Sym name => Pgml.Sym {name = name, content = s}
    98     | _ => Pgml.Str s)
    99   else Pgml.Str s;
   100 
   101 val pgml_syms = map pgml_sym o Symbol.explode;
   102 
   103 val token_markups =
   104  [Markup.tclassN, Markup.tfreeN, Markup.tvarN, Markup.freeN,
   105   Markup.boundN, Markup.varN, Markup.skolemN];
   106 
   107 in
   108 
   109 fun pgml_terms (XML.Elem ((name, atts), body)) =
   110       if member (op =) token_markups name then
   111         let val content = pgml_syms (Buffer.content (fold XML.add_content body Buffer.empty))
   112         in [Pgml.Atoms {kind = SOME name, content = content}] end
   113       else
   114         let val content = maps pgml_terms body in
   115           if name = Markup.blockN then
   116             [Pgml.Box {orient = NONE, indent = Properties.get_int atts Markup.indentN, content = content}]
   117           else if name = Markup.breakN then
   118             [Pgml.Break {mandatory = NONE, indent = Properties.get_int atts Markup.widthN}]
   119           else content
   120         end
   121   | pgml_terms (XML.Text text) = map (Pgml.Raw o Pgml.atom_to_xml) (pgml_syms text);
   122 
   123 end;
   124 
   125 
   126 (* messages *)
   127 
   128 fun pgml area content =
   129   Pgml.Pgml {version = NONE, systemid = NONE, area = SOME area, content = content};
   130 
   131 fun message_content default_area s =
   132   let
   133     val body = YXML.parse_body s;
   134     val area =
   135       (case body of
   136         [XML.Elem ((name, _), _)] =>
   137           if name = Markup.stateN then PgipTypes.Display else default_area
   138       | _ => default_area);
   139   in Pgml.pgml_to_xml (pgml area (maps pgml_terms body)) end;
   140 
   141 
   142 fun normalmsg area s = issue_pgip
   143   (Normalresponse {content = [message_content area s]});
   144 
   145 fun errormsg area fatality s = issue_pgip
   146   (Errorresponse {fatality = fatality, location = NONE, content = [message_content area s]});
   147 
   148 (*error responses with useful locations*)
   149 fun error_with_pos area fatality pos s = issue_pgip
   150   (Errorresponse {
   151     fatality = fatality,
   152     location = SOME (PgipIsabelle.location_of_position pos),
   153     content = [message_content area s]});
   154 
   155 fun panic s = (errormsg Message Panic ("## SYSTEM EXIT ##\n" ^ s); exit 1);
   156 fun nonfatal_error s = errormsg Message Nonfatal s;
   157 fun log_msg s = errormsg Message Log s;
   158 
   159 (* NB: all of standard functions print strings terminated with new lines, but we don't
   160    add new lines explicitly in PGIP: they are left implicit.  It means that PGIP messages
   161    can't be written without newlines. *)
   162 fun setup_messages () =
   163  (Output.writeln_fn := (fn s => normalmsg Message s);
   164   Output.status_fn := (fn _ => ());
   165   Output.report_fn := (fn _ => ());
   166   Output.priority_fn := (fn s => normalmsg Status s);
   167   Output.tracing_fn := (fn s => normalmsg Tracing s);
   168   Output.warning_fn := (fn s => errormsg Message Warning s);
   169   Output.error_fn := (fn s => errormsg Message Fatal s);
   170   Output.debug_fn := (fn s => errormsg Message Debug s));
   171 
   172 
   173 (* immediate messages *)
   174 
   175 fun tell_clear_goals () =
   176     issue_pgip (Normalresponse { content = [Pgml.pgml_to_xml (pgml Display [])] })
   177 fun tell_clear_response () =
   178     issue_pgip (Normalresponse { content = [Pgml.pgml_to_xml (pgml Message [])] })
   179 
   180 fun tell_file_loaded completed path   =
   181     issue_pgip (Informfileloaded {url=PgipTypes.pgipurl_of_path path,
   182                                   completed=completed})
   183 fun tell_file_outdated completed path   =
   184     issue_pgip (Informfileoutdated {url=PgipTypes.pgipurl_of_path path,
   185                                     completed=completed})
   186 fun tell_file_retracted completed path =
   187     issue_pgip (Informfileretracted {url=PgipTypes.pgipurl_of_path path,
   188                                      completed=completed})
   189 
   190 
   191 (* theory loader actions *)
   192 
   193 local
   194   (* da: TODO: PGIP has a completed flag so the prover can indicate to the
   195      interface which files are busy performing a particular action.
   196      To make use of this we need to adjust the hook in thy_info.ML
   197      (may actually be difficult to tell the interface *which* action is in
   198       progress, but we could add a generic "Lock" action which uses
   199       informfileloaded: the broker/UI should not infer too much from incomplete
   200       operations).
   201    *)
   202 fun trace_action action name =
   203   if action = Thy_Info.Update then
   204     List.app (tell_file_loaded true) (Thy_Info.loaded_files name)
   205   else if action = Thy_Info.Remove then
   206       List.app (tell_file_retracted true) (Thy_Info.loaded_files name)
   207   else ()
   208 
   209 
   210 in
   211   fun setup_thy_loader () = Thy_Info.add_hook trace_action;
   212   fun sync_thy_loader () = List.app (trace_action Thy_Info.Update) (Thy_Info.get_names ());
   213 end;
   214 
   215 
   216 (* get informed about files *)
   217 
   218 val thy_name = Path.implode o #1 o Path.split_ext o Path.base;
   219 
   220 val inform_file_retracted = Thy_Info.kill_thy o thy_name;
   221 
   222 fun inform_file_processed path state =
   223   let val name = thy_name path in
   224     if Toplevel.is_toplevel state then
   225       Thy_Info.register_thy (Toplevel.end_theory Position.none state)
   226         handle ERROR msg =>
   227           (warning (cat_lines [msg, "Failed to register theory: " ^ quote name]);
   228             tell_file_retracted true (Path.base path))
   229     else raise Toplevel.UNDEF
   230   end;
   231 
   232 
   233 (* restart top-level loop (keeps most state information) *)
   234 
   235 val welcome = priority o Session.welcome;
   236 
   237 fun restart () =
   238     (sync_thy_loader ();
   239      tell_clear_goals ();
   240      tell_clear_response ();
   241      Isar.init ();
   242      welcome ());
   243 
   244 
   245 (* theorem dependencies *)
   246 
   247 local
   248 
   249 fun add_proof_body (PBody {thms, ...}) =
   250   thms |> fold (fn (_, (name, _, _)) => name <> "" ? Symtab.update (name, ()));
   251 
   252 fun add_thm th =
   253   (case Thm.proof_body_of th of 
   254     PBody {proof = PThm (_, ((name, _, _), body)), ...} =>
   255       if Thm.has_name_hint th andalso Thm.get_name_hint th = name
   256       then add_proof_body (Future.join body)
   257       else I
   258   | body => add_proof_body body);
   259 
   260 in
   261 
   262 fun thms_deps ths =
   263   let
   264     (* FIXME proper derivation names!? *)
   265     val names = map Thm.get_name_hint (filter Thm.has_name_hint ths);
   266     val deps = Symtab.keys (fold add_thm ths Symtab.empty);
   267   in (names, deps) end;
   268 
   269 fun new_thms_deps thy thy' =
   270   let
   271     val prev_facts = PureThy.facts_of thy;
   272     val facts = PureThy.facts_of thy';
   273   in thms_deps (maps #2 (Facts.dest_static [prev_facts] facts)) end;
   274 
   275 end;
   276 
   277 
   278 (* theorem dependeny output *)
   279 
   280 val show_theorem_dependencies = Unsynchronized.ref false;
   281 
   282 local
   283 
   284 val spaces_quote = space_implode " " o map quote;
   285 
   286 fun thm_deps_message (thms, deps) =
   287   let
   288     val valuethms = XML.Elem (("value", [("name", "thms")]), [XML.Text thms]);
   289     val valuedeps = XML.Elem (("value", [("name", "deps")]), [XML.Text deps]);
   290   in
   291     issue_pgip (Metainforesponse
   292       {attrs = [("infotype", "isabelle_theorem_dependencies")],
   293        content = [valuethms, valuedeps]})
   294   end;
   295 
   296 in
   297 
   298 fun setup_present_hook () = Toplevel.add_hook (fn _ => fn state => fn state' =>
   299   if ! show_theorem_dependencies andalso
   300     can Toplevel.theory_of state andalso Toplevel.is_theory state'
   301   then
   302     let val (names, deps) = new_thms_deps (Toplevel.theory_of state) (Toplevel.theory_of state') in
   303       if null names orelse null deps then ()
   304       else thm_deps_message (spaces_quote names, spaces_quote deps)
   305     end
   306   else ());
   307 
   308 end;
   309 
   310 
   311 (** lexicalstructure element with keywords (PGIP version of elisp keywords file) **)
   312 
   313 fun lexicalstructure_keywords () =
   314     let val keywords = Keyword.dest_keywords ()
   315         val commands = Keyword.dest_commands ()
   316         fun keyword_elt kind keyword =
   317             XML.Elem (("keyword", [("word", keyword), ("category", kind)]), [])
   318         in
   319             Lexicalstructure
   320               {content = map (keyword_elt "minor") keywords @ map (keyword_elt "major") commands}
   321         end
   322 
   323 (* TODO: we can issue a lexicalstructure/keyword when the syntax gets extended dynamically;
   324    hooks needed in outer_syntax.ML to do that. *)
   325 
   326 
   327 (* Configuration: GUI config, proverinfo messages *)
   328 
   329 local
   330     val isabellewww = "http://isabelle.in.tum.de/"
   331     val staticconfig = "~~/lib/ProofGeneral/pgip_isar.xml"
   332     fun orenv v d = case getenv v of "" => d  | s => s
   333     fun config_file()  = orenv "ISABELLE_PGIPCONFIG" staticconfig
   334     fun isabelle_www() = orenv "ISABELLE_HOMEPAGE" isabellewww
   335 in
   336 fun send_pgip_config () =
   337     let
   338         val path = Path.explode (config_file())
   339         val ex = File.exists path
   340 
   341         val wwwpage =
   342             (Url.explode (isabelle_www()))
   343             handle ERROR _ =>
   344                    (panic ("Error in URL in environment variable ISABELLE_HOMEPAGE.");
   345                         Url.explode isabellewww)
   346 
   347         val proverinfo =
   348             Proverinfo { name = "Isabelle",
   349                          version = Distribution.version,
   350                          instance = Session.name(),
   351                          descr = "The Isabelle/Isar theorem prover",
   352                          url = wwwpage,
   353                          filenameextns = ".thy;" }
   354     in
   355         if ex then
   356             (issue_pgip proverinfo;
   357              issue_pgip_rawtext (File.read path);
   358              issue_pgip (lexicalstructure_keywords()))
   359         else panic ("PGIP configuration file \"" ^ config_file() ^ "\" not found")
   360     end;
   361 end
   362 
   363 
   364 (* Preferences: tweak for PGIP interfaces *)
   365 
   366 val preferences = Unsynchronized.ref Preferences.pure_preferences;
   367 
   368 fun add_preference cat pref =
   369   CRITICAL (fn () => Unsynchronized.change preferences (Preferences.add cat pref));
   370 
   371 fun setup_preferences_tweak () =
   372   CRITICAL (fn () => Unsynchronized.change preferences
   373    (Preferences.set_default ("show-question-marks", "false") #>
   374     Preferences.remove "show-question-marks" #>   (* we use markup, not ?s *)
   375     Preferences.remove "theorem-dependencies" #>  (* set internally *)
   376     Preferences.remove "full-proofs"));           (* set internally *)
   377 
   378 
   379 
   380 (* Sending commands to Isar *)
   381 
   382 fun isarcmd s = Isar.>>> (Outer_Syntax.parse Position.none s);
   383 
   384 (* TODO:
   385     - apply a command given a transition function;
   386     - fix position from path of currently open file [line numbers risk garbling though].
   387 *)
   388 
   389 (* load an arbitrary file (must be .thy or .ML) *)
   390 
   391 fun use_thy_or_ml_file file =
   392     let
   393         val (path,extn) = Path.split_ext (Path.explode file)
   394     in
   395         case extn of
   396             "" => isarcmd ("use_thy " ^ quote (Path.implode path))
   397           | "thy" => isarcmd ("use_thy " ^ quote (Path.implode path))
   398           | "ML" => isarcmd ("use " ^ quote file)
   399           | other => error ("Don't know how to read a file with extension " ^ quote other)
   400     end
   401 
   402 
   403 (******* PGIP actions *******)
   404 
   405 
   406 (* Responses to each of the PGIP input commands.
   407    These are programmed uniformly for extensibility. *)
   408 
   409 fun askpgip (Askpgip _) =
   410     (issue_pgip
   411          (Usespgip { version = PgipIsabelle.isabelle_pgip_version_supported,
   412                      pgipelems = PgipIsabelle.accepted_inputs });
   413      send_pgip_config())
   414 
   415 fun askpgml (Askpgml _) =
   416     issue_pgip
   417         (Usespgml { version = PgipIsabelle.isabelle_pgml_version_supported })
   418 
   419 fun askprefs (Askprefs _) =
   420     let
   421         fun preference_of {name, descr, default, pgiptype, get, set } =
   422             { name = name, descr = SOME descr, default = SOME default,
   423               pgiptype = pgiptype }
   424     in
   425         List.app (fn (prefcat, prefs) =>
   426                      issue_pgip (Hasprefs {prefcategory=SOME prefcat,
   427                                            prefs=map preference_of prefs}))
   428                  (!preferences)
   429     end
   430 
   431 fun askconfig (Askconfig _) = () (* TODO: add config response *)
   432 
   433 local
   434     fun lookuppref pref =
   435         case AList.lookup (op =)
   436                           (map (fn p => (#name p,p))
   437                                (maps snd (!preferences))) pref of
   438             NONE => error ("Unknown prover preference: " ^ quote pref)
   439           | SOME p => p
   440 in
   441 fun setpref (Setpref vs) =
   442     let
   443         val name = #name vs
   444         val value = #value vs
   445         val set = #set (lookuppref name)
   446     in
   447         set value
   448     end
   449 
   450 fun getpref (Getpref vs) =
   451     let
   452         val name = #name vs
   453         val get = #get (lookuppref name)
   454     in
   455         issue_pgip (Prefval {name=name, value=get ()})
   456     end
   457 end
   458 
   459 fun proverinit _ = restart ()
   460 
   461 fun proverexit _ = isarcmd "quit"
   462 
   463 fun set_proverflag_quiet b =
   464     isarcmd (if b then "disable_pr" else "enable_pr")
   465 
   466 fun set_proverflag_pgmlsymbols b =
   467     (pgmlsymbols_flag := b;
   468       NAMED_CRITICAL "print_mode" (fn () =>
   469         Unsynchronized.change print_mode
   470             (fn mode =>
   471                 remove (op =) Symbol.xsymbolsN mode @ (if b then [Symbol.xsymbolsN] else []))))
   472 
   473 fun set_proverflag_thmdeps b =
   474     (show_theorem_dependencies := b;
   475      Proofterm.proofs := (if b then 1 else 2))
   476 
   477 fun setproverflag (Setproverflag vs) =
   478     let
   479         val flagname = #flagname vs
   480         val value = #value vs
   481     in
   482         (case flagname of
   483              "quiet"            => set_proverflag_quiet value
   484            | "pgmlsymbols"      => set_proverflag_pgmlsymbols value
   485            | "metainfo:thmdeps" => set_proverflag_thmdeps value
   486            | _ => log_msg ("Unrecognised prover control flag: " ^
   487                            (quote flagname) ^ " ignored."))
   488     end
   489 
   490 
   491 fun dostep (Dostep vs) =
   492     let
   493         val text = #text vs
   494     in
   495         isarcmd text
   496     end
   497 
   498 fun undostep (Undostep vs) =
   499     let
   500         val times = #times vs
   501     in
   502         isarcmd ("undos_proof " ^ Int.toString times)
   503     end
   504 
   505 fun redostep _ = raise Fail "redo unavailable"
   506 
   507 fun abortgoal _ = isarcmd "kill" (* was: ProofGeneral.kill_proof *)
   508 
   509 
   510 (*** PGIP identifier tables ***)
   511 
   512 (* TODO: these ones should be triggered by hooks after a
   513    declaration addition/removal, to be sent automatically. *)
   514 
   515 fun addids t  = issue_pgip (Addids {idtables = [t]})
   516 fun delids t  = issue_pgip (Delids {idtables = [t]})
   517 
   518 
   519 local
   520 
   521 fun theory_facts name =
   522   let val thy = Thy_Info.get_theory name
   523   in (map PureThy.facts_of (Theory.parents_of thy), PureThy.facts_of thy) end;
   524 
   525 fun thms_of_thy name = map fst (theory_facts name |-> Facts.extern_static);
   526 fun qualified_thms_of_thy name = map fst (theory_facts name |-> Facts.dest_static);
   527 
   528 in
   529 
   530 fun askids (Askids vs) =
   531     let
   532         val url = #url vs            (* ask for identifiers within a file *)
   533         val thyname = #thyname vs    (* ask for identifiers within a theory *)
   534         val objtype = #objtype vs    (* ask for identifiers of a particular type *)
   535 
   536         fun idtable ty ctx ids = {objtype=ty,context=ctx,ids=ids}
   537 
   538         fun setids t = issue_pgip (Setids {idtables = [t]})
   539 
   540         (* fake one-level nested "subtheories" by picking apart names. *)
   541         val immed_thms_of_thy = filter_out Long_Name.is_qualified o thms_of_thy
   542         fun thy_prefix s = case Long_Name.explode s of
   543                                     x::_::_ => SOME x  (* String.find? *)
   544                                   | _ => NONE
   545         fun subthys_of_thy s =
   546             List.foldl  (fn (NONE,xs) => xs | (SOME x,xs) => insert op= x xs) []
   547                    (map thy_prefix (thms_of_thy s))
   548         fun subthms_of_thy thy =
   549             (case thy_prefix thy of
   550                  NONE => immed_thms_of_thy thy
   551                | SOME prf => filter (String.isPrefix (unprefix (prf ^ Long_Name.separator) thy))
   552                                     (thms_of_thy prf))
   553     in
   554         case (thyname,objtype) of
   555            (NONE, NONE) =>
   556            setids (idtable ObjFile NONE (Thy_Info.get_names())) (*FIXME: uris*)
   557          | (NONE, SOME ObjFile) =>
   558            setids (idtable ObjFile NONE (Thy_Info.get_names())) (*FIXME: uris*)
   559          | (SOME fi, SOME ObjFile) =>
   560            setids (idtable ObjTheory (SOME fi) [fi])       (* TODO: check exists *)
   561          | (NONE, SOME ObjTheory) =>
   562            setids (idtable ObjTheory NONE (Thy_Info.get_names()))
   563          | (SOME thy, SOME ObjTheory) =>
   564            setids (idtable ObjTheory (SOME thy) (subthys_of_thy thy))
   565          | (SOME thy, SOME ObjTheorem) =>
   566            setids (idtable ObjTheorem (SOME thy) (subthms_of_thy thy))
   567          | (NONE, SOME ObjTheorem) =>
   568            (* A large query, but not unreasonable. ~5000 results for HOL.*)
   569            (* Several setids should be allowed, but Eclipse code is currently broken:
   570               List.app (fn thy => setids (idtable ObjTheorem (SOME thy) (subthms_of_thy thy)))
   571                          (Thy_Info.get_names()) *)
   572            setids (idtable ObjTheorem NONE (* this one gives ~7000 for HOL *)
   573                            (maps qualified_thms_of_thy (Thy_Info.get_names())))
   574          | _ => warning ("askids: ignored argument combination")
   575     end
   576 
   577 end;
   578 
   579 fun askrefs (Askrefs vs) =
   580     let
   581         val url = #url vs            (* ask for references of a file (i.e. immediate pre-requisites) *)
   582         val thyname = #thyname vs    (* ask for references of a theory (other theories) *)
   583         val objtype = #objtype vs    (* ask for references of a particular type... *)
   584         val name = #name vs          (*   ... with this name *)
   585 
   586         fun idtable ty ctx ids = {objtype=ty,context=ctx,ids=ids}
   587 
   588         val thy_name = Path.implode o #1 o Path.split_ext o Path.base
   589 
   590         fun filerefs f =
   591             let val thy = thy_name f
   592                 val filerefs = #uses (Thy_Load.deps_thy (Path.dir f) thy)
   593             in
   594                 issue_pgip (Setrefs {url=url, thyname=NONE, objtype=SOME PgipTypes.ObjFile,
   595                                      name=NONE, idtables=[], fileurls=filerefs})
   596             end
   597 
   598         fun thyrefs thy =
   599             let val thyrefs = #imports (Thy_Load.deps_thy Path.current thy)
   600             in
   601                 issue_pgip (Setrefs {url=url, thyname=thyname, objtype=SOME PgipTypes.ObjTheory,
   602                                      name=NONE, idtables=[{context=NONE, objtype=PgipTypes.ObjTheory,
   603                                                            ids=thyrefs}], fileurls=[]})
   604             end
   605 
   606         fun thmrefs thmname =
   607             let
   608                 (* TODO: interim: this is probably not right.
   609                    What we want is mapping onto simple PGIP name/context model. *)
   610                 val ctx = Toplevel.context_of (Isar.state ()) (* NB: raises UNDEF *)
   611                 val thy = ProofContext.theory_of ctx
   612                 val ths = [PureThy.get_thm thy thmname]
   613                 val deps = #2 (thms_deps ths);
   614             in
   615                 if null deps then ()
   616                 else issue_pgip (Setrefs {url=url, thyname=thyname, name=name,
   617                                           objtype=SOME PgipTypes.ObjTheorem,
   618                                           idtables=[{context=NONE, objtype=PgipTypes.ObjTheorem,
   619                                                      ids=deps}], fileurls=[]})
   620             end
   621     in
   622         case (url,thyname,objtype,name) of
   623             (SOME file, NONE, _, _)  => filerefs file
   624           | (_,SOME thy,_,_)         => thyrefs thy
   625           | (_,_,SOME PgipTypes.ObjTheorem,SOME thmname) => thmrefs thmname
   626           | _  => error ("Unimplemented/invalid case of <askrefs>")
   627     end
   628 
   629 
   630 
   631 fun showid (Showid vs) =
   632     let
   633         val thyname = #thyname vs
   634         val objtype = #objtype vs
   635         val name = #name vs
   636 
   637         val topthy = Toplevel.theory_of o Isar.state
   638 
   639         fun splitthy id =
   640             let val comps = Long_Name.explode id
   641             in case comps of
   642                    (thy::(rest as _::_)) => (Thy_Info.get_theory thy, space_implode "." rest)
   643                  | [plainid] => (topthy(),plainid)
   644                  | _ => raise Toplevel.UNDEF (* assert false *)
   645             end
   646 
   647 
   648         fun idvalue strings =
   649             issue_pgip (Idvalue { thyname=thyname, objtype=objtype, name=name,
   650                                   text=[XML.Elem (("pgml", []), maps YXML.parse_body strings)] })
   651 
   652         fun strings_of_thm (thy, name) =
   653           map (Display.string_of_thm_global thy) (PureThy.get_thms thy name)
   654 
   655         val string_of_thy = Pretty.string_of o Proof_Display.pretty_full_theory false
   656     in
   657         case (thyname, objtype) of
   658             (_, ObjTheory) => idvalue [string_of_thy (Thy_Info.get_theory name)]
   659           | (SOME thy, ObjTheorem) => idvalue (strings_of_thm (Thy_Info.get_theory thy, name))
   660           | (NONE, ObjTheorem) => idvalue (strings_of_thm (splitthy name))
   661           | (_, ot) => error ("Cannot show objects of type "^(PgipTypes.name_of_objtype ot))
   662     end
   663 
   664 (*** Inspecting state ***)
   665 
   666 (* The file which is currently being processed interactively.
   667    In the pre-PGIP code, this was informed to Isabelle and the theory loader
   668    on completion, but that allows for circularity in case we read
   669    ourselves.  So PGIP opens the filename at the start of a script.
   670    We ought to prevent problems by modifying the theory loader to know
   671    about this special status, but for now we just keep a local reference.
   672 *)
   673 
   674 val currently_open_file = Unsynchronized.ref (NONE : pgipurl option)
   675 
   676 fun get_currently_open_file () = ! currently_open_file;
   677 
   678 fun askguise _ =
   679     (* The "guise" is the PGIP abstraction of the prover's state.
   680        The <informguise> message is merely used for consistency checking. *)
   681     let
   682         val openfile = !currently_open_file
   683 
   684         val topthy = Toplevel.theory_of o Isar.state
   685         val topthy_name = Context.theory_name o topthy
   686 
   687         val opentheory = SOME (topthy_name()) handle Toplevel.UNDEF => NONE
   688 
   689         fun topproofpos () = try Toplevel.proof_position_of (Isar.state ());
   690         val openproofpos = topproofpos()
   691     in
   692         issue_pgip (Informguise { file = openfile,
   693                                   theory = opentheory,
   694                                   (* would be nice to get thm name... *)
   695                                   theorem = NONE,
   696                                   proofpos = openproofpos })
   697     end
   698 
   699 fun parsescript (Parsescript vs) =
   700     let
   701         val text = #text vs
   702         val systemdata = #systemdata vs
   703         val location = #location vs   (* TODO: extract position *)
   704 
   705         val doc = PgipParser.pgip_parser Position.none text
   706 
   707         val sysattrs = PgipTypes.opt_attr "systemdata" systemdata
   708         val locattrs = PgipTypes.attrs_of_location location
   709      in
   710         issue_pgip (Parseresult { attrs= sysattrs@locattrs,
   711                                   doc = doc,
   712                                   errs = [] })
   713     end
   714 
   715 fun showproofstate _ = isarcmd "pr"
   716 
   717 fun showctxt _ = isarcmd "print_context"
   718 
   719 fun searchtheorems (Searchtheorems vs) =
   720     let
   721         val arg = #arg vs
   722     in
   723         isarcmd ("find_theorems " ^ arg)
   724     end
   725 
   726 fun setlinewidth (Setlinewidth vs) =
   727     let
   728         val width = #width vs
   729     in
   730         isarcmd ("pretty_setmargin " ^ Int.toString width) (* FIXME: conversion back/forth! *)
   731     end
   732 
   733 fun viewdoc (Viewdoc vs) =
   734     let
   735         val arg = #arg vs
   736     in
   737         isarcmd ("print_" ^ arg)   (* FIXME: isabelle doc?.  Return URLs, maybe? *)
   738     end
   739 
   740 (*** Theory ***)
   741 
   742 fun doitem (Doitem vs) =
   743     let
   744         val text = #text vs
   745     in
   746         isarcmd text
   747     end
   748 
   749 fun undoitem _ =
   750     isarcmd "undo"
   751 
   752 fun redoitem _ =
   753     isarcmd "redo"
   754 
   755 fun aborttheory _ =
   756     isarcmd "kill"  (* was: "init_toplevel" *)
   757 
   758 fun retracttheory (Retracttheory vs) =
   759     let
   760         val thyname = #thyname vs
   761     in
   762         isarcmd ("kill_thy " ^ quote thyname)
   763     end
   764 
   765 
   766 (*** Files ***)
   767 
   768 (* Path management: we allow theory files to have dependencies in
   769    their own directory, but when we change directory for a new file we
   770    remove the path.  Leaving it there can cause confusion with
   771    difference in batch mode.
   772    NB: PGIP does not assume that the prover has a load path.
   773 *)
   774 
   775 local
   776     val current_working_dir = Unsynchronized.ref (NONE : string option)
   777 in
   778 fun changecwd_dir newdirpath =
   779    let
   780        val newdir = File.platform_path newdirpath
   781    in
   782        (case (!current_working_dir) of
   783             NONE => ()
   784           | SOME dir => Thy_Load.del_path dir;
   785         Thy_Load.add_path newdir;
   786         current_working_dir := SOME newdir)
   787    end
   788 end
   789 
   790 fun changecwd (Changecwd vs) =
   791     let
   792         val url = #url vs
   793         val newdir = PgipTypes.path_of_pgipurl url
   794     in
   795         changecwd_dir url
   796     end
   797 
   798 fun openfile (Openfile vs) =
   799   let
   800       val url = #url vs
   801       val filepath = PgipTypes.path_of_pgipurl url
   802       val filedir = Path.dir filepath
   803       val thy_name = Path.implode o #1 o Path.split_ext o Path.base
   804       val openfile_retract = Thy_Info.kill_thy o thy_name;
   805   in
   806       case !currently_open_file of
   807           SOME f => raise PGIP ("<openfile> when a file is already open!\nCurrently open file: " ^
   808                                 PgipTypes.string_of_pgipurl url)
   809         | NONE => (openfile_retract filepath;
   810                    changecwd_dir filedir;
   811                    priority ("Working in file: " ^ PgipTypes.string_of_pgipurl url);
   812                    currently_open_file := SOME url)
   813   end
   814 
   815 fun closefile _ =
   816     case !currently_open_file of
   817         SOME f => (inform_file_processed f (Isar.state ());
   818                    priority ("Finished working in file: " ^ PgipTypes.string_of_pgipurl f);
   819                    currently_open_file := NONE)
   820       | NONE => raise PGIP ("<closefile> when no file is open!")
   821 
   822 fun loadfile (Loadfile vs) =
   823     let
   824         val url = #url vs
   825     in
   826         (* da: this doesn't seem to cause a problem, batch loading uses
   827            a different state context.  Of course confusion is still possible,
   828            e.g. file loaded depends on open file which is not yet saved. *)
   829         (* case !currently_open_file of
   830             SOME f => raise PGIP ("<loadfile> when a file is open!\nCurrently open file: " ^
   831                                   PgipTypes.string_of_pgipurl url)
   832           | NONE => *)
   833         use_thy_or_ml_file (File.platform_path url)
   834     end
   835 
   836 fun abortfile _ =
   837     case !currently_open_file of
   838         SOME f => (isarcmd "init_toplevel";
   839                    priority ("Aborted working in file: " ^
   840                              PgipTypes.string_of_pgipurl f);
   841                    currently_open_file := NONE)
   842       | NONE => raise PGIP ("<abortfile> when no file is open!")
   843 
   844 fun retractfile (Retractfile vs) =
   845     let
   846         val url = #url vs
   847     in
   848         case !currently_open_file of
   849             SOME f => raise PGIP ("<retractfile> when a file is open!")
   850           | NONE => (priority ("Retracting file: " ^ PgipTypes.string_of_pgipurl url);
   851                      (* TODO: next should be in thy loader, here just for testing *)
   852                      let
   853                          val name = thy_name url
   854                      in List.app (tell_file_retracted false) (Thy_Info.loaded_files name) end;
   855                      inform_file_retracted url)
   856     end
   857 
   858 
   859 (*** System ***)
   860 
   861 fun systemcmd (Systemcmd vs) =
   862   let
   863       val arg = #arg vs
   864   in
   865       isarcmd arg
   866   end
   867 
   868 exception PGIP_QUIT;
   869 fun quitpgip _ = raise PGIP_QUIT
   870 
   871 fun process_input inp = case inp
   872  of Pgip.Askpgip _          => askpgip inp
   873   | Pgip.Askpgml _          => askpgml inp
   874   | Pgip.Askprefs _         => askprefs inp
   875   | Pgip.Askconfig _        => askconfig inp
   876   | Pgip.Getpref _          => getpref inp
   877   | Pgip.Setpref _          => setpref inp
   878   | Pgip.Proverinit _       => proverinit inp
   879   | Pgip.Proverexit _       => proverexit inp
   880   | Pgip.Setproverflag _    => setproverflag inp
   881   | Pgip.Dostep _           => dostep inp
   882   | Pgip.Undostep _         => undostep inp
   883   | Pgip.Redostep _         => redostep inp
   884   | Pgip.Forget _           => error "<forget> not implemented by Isabelle"
   885   | Pgip.Restoregoal _      => error "<restoregoal> not implemented by Isabelle"
   886   | Pgip.Abortgoal _        => abortgoal inp
   887   | Pgip.Askids _           => askids inp
   888   | Pgip.Askrefs _          => askrefs inp
   889   | Pgip.Showid _           => showid inp
   890   | Pgip.Askguise _         => askguise inp
   891   | Pgip.Parsescript _      => parsescript inp
   892   | Pgip.Showproofstate _   => showproofstate inp
   893   | Pgip.Showctxt _         => showctxt inp
   894   | Pgip.Searchtheorems _   => searchtheorems inp
   895   | Pgip.Setlinewidth _     => setlinewidth inp
   896   | Pgip.Viewdoc _          => viewdoc inp
   897   | Pgip.Doitem _           => doitem inp
   898   | Pgip.Undoitem _         => undoitem inp
   899   | Pgip.Redoitem _         => redoitem inp
   900   | Pgip.Aborttheory _      => aborttheory inp
   901   | Pgip.Retracttheory _    => retracttheory inp
   902   | Pgip.Loadfile _         => loadfile inp
   903   | Pgip.Openfile _         => openfile inp
   904   | Pgip.Closefile _        => closefile inp
   905   | Pgip.Abortfile _        => abortfile inp
   906   | Pgip.Retractfile _      => retractfile inp
   907   | Pgip.Changecwd _        => changecwd inp
   908   | Pgip.Systemcmd _        => systemcmd inp
   909   | Pgip.Quitpgip _         => quitpgip inp
   910 
   911 
   912 fun process_pgip_element pgipxml =
   913     case pgipxml of
   914         xml as (XML.Elem elem) =>
   915         (case Pgip.input elem of
   916              NONE => warning ("Unrecognized PGIP command, ignored: \n" ^
   917                               (XML.string_of xml))
   918            | SOME inp => (process_input inp)) (* errors later; packet discarded *)
   919       | XML.Text t => ignored_text_warning t
   920 and ignored_text_warning t =
   921     if size (Symbol.strip_blanks t) > 0 then
   922            warning ("Ignored text in PGIP packet: \n" ^ t)
   923     else ()
   924 
   925 fun process_pgip_tree xml =
   926     (pgip_refid := NONE;
   927      pgip_refseq := NONE;
   928      (case xml of
   929           XML.Elem (("pgip", attrs), pgips) =>
   930           (let
   931                val class = PgipTypes.get_attr "class" attrs
   932                val dest  = PgipTypes.get_attr_opt "destid" attrs
   933                val seq = PgipTypes.read_pgipnat (PgipTypes.get_attr "seq" attrs)
   934                (* Respond to prover broadcasts, or messages for us. Ignore rest *)
   935                val processit =
   936                    case dest of
   937                        NONE =>    class = "pa"
   938                      | SOME id => matching_pgip_id id
   939            in if processit then
   940                   (pgip_refid :=  PgipTypes.get_attr_opt "id" attrs;
   941                    pgip_refseq := SOME seq;
   942                    List.app process_pgip_element pgips;
   943                    (* return true to indicate <ready/> *)
   944                    true)
   945               else
   946                   (* no response to ignored messages. *)
   947                   false
   948            end)
   949         | _ => raise PGIP "Invalid PGIP packet received")
   950      handle PGIP msg =>
   951             (Output.error_msg ((msg ^ "\nPGIP error occurred in XML text below:\n") ^
   952                                (XML.string_of xml));
   953              true))
   954 
   955 (* External input *)
   956 
   957 val process_pgip_plain = K () o process_pgip_tree o XML.parse
   958 
   959 (* PGIP loop: process PGIP input only *)
   960 
   961 local
   962 
   963 exception XML_PARSE
   964 
   965 fun loop ready src =
   966     let
   967         val _ = if ready then issue_pgip (Ready ()) else ()
   968         val pgipo =
   969           (case try Source.get_single src of
   970             SOME pgipo => pgipo
   971           | NONE => raise XML_PARSE)
   972     in
   973         case pgipo of
   974              NONE  => ()
   975            | SOME (pgip,src') =>
   976              let
   977                  val ready' = (process_pgip_tree pgip)
   978                                 handle PGIP_QUIT => raise PGIP_QUIT
   979                                      | e => (handler (e,SOME src'); true)
   980              in
   981                  loop ready' src'
   982              end
   983     end handle e => handler (e,SOME src)  (* error in XML parse or Ready issue *)
   984 
   985 and handler (e,srco) =
   986     if Exn.is_interrupt e andalso is_some srco then
   987         (Output.error_msg "Interrupt during PGIP processing"; loop true (the srco))
   988     else
   989         case (e,srco) of
   990             (XML_PARSE,SOME src) =>
   991             panic "Invalid XML input, aborting" (* TODO: attempt recovery  *)
   992           | (Toplevel.UNDEF,SOME src) =>
   993             (Output.error_msg "No working context defined"; loop true src)
   994           | (e,SOME src) =>
   995             (Output.error_msg (ML_Compiler.exn_message e); loop true src)
   996           | (PGIP_QUIT,_) => ()
   997           | (_,NONE) => ()
   998 in
   999   (* TODO: add socket interface *)
  1000 
  1001   val xmlP = XML.parse_comments |-- XML.parse_element >> single
  1002 
  1003   val tty_src =
  1004     Source.set_prompt "" (Source.source Symbol.stopper xmlP NONE (Source.tty TextIO.stdIn))
  1005 
  1006   fun pgip_toplevel x = loop true x
  1007 end
  1008 
  1009 
  1010 (* init *)
  1011 
  1012 val initialized = Unsynchronized.ref false;
  1013 
  1014 fun init_pgip false = panic "No Proof General interface support for Isabelle/classic mode."
  1015   | init_pgip true =
  1016       (if ! initialized then ()
  1017        else
  1018         (setup_preferences_tweak ();
  1019          Output.add_mode proof_generalN Output.default_output Output.default_escape;
  1020          Markup.add_mode proof_generalN YXML.output_markup;
  1021          setup_messages ();
  1022          setup_thy_loader ();
  1023          setup_present_hook ();
  1024          init_pgip_session_id ();
  1025          welcome ();
  1026          initialized := true);
  1027        sync_thy_loader ();
  1028        Unsynchronized.change print_mode (update (op =) proof_generalN);
  1029        pgip_toplevel tty_src);
  1030 
  1031 
  1032 
  1033 (** Out-of-loop PGIP commands (for Emacs hybrid mode) **)
  1034 
  1035 local
  1036     val pgip_output_channel = Unsynchronized.ref Output.writeln_default
  1037 in
  1038 
  1039 (* Set recipient for PGIP results *)
  1040 fun pgip_channel_emacs writefn =
  1041     (init_pgip_session_id();
  1042      pgip_output_channel := writefn)
  1043 
  1044 (* Process a PGIP command.
  1045    This works for preferences but not generally guaranteed
  1046    because we haven't done full setup here (e.g., no pgml mode)  *)
  1047 fun process_pgip_emacs str =
  1048      setmp_noncritical output_xml_fn (!pgip_output_channel) process_pgip_plain str
  1049 
  1050 end
  1051 
  1052 
  1053 (* Extra command for embedding prover-control inside document (obscure/debug usage). *)
  1054 
  1055 val _ =
  1056   Outer_Syntax.improper_command "ProofGeneral.process_pgip" "(internal)" Keyword.control
  1057     (Parse.text >> (Toplevel.no_timing oo
  1058       (fn txt => Toplevel.imperative (fn () =>
  1059         if print_mode_active proof_general_emacsN
  1060         then process_pgip_emacs txt
  1061         else process_pgip_plain txt))));
  1062 
  1063 end;