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