src/Pure/ProofGeneral/proof_general_pgip.ML
author wenzelm
Sun Mar 08 17:26:14 2009 +0100 (2009-03-08)
changeset 30364 577edc39b501
parent 29635 31d14e9fa0da
child 30723 a3adc9a96a16
permissions -rw-r--r--
moved basic algebra of long names from structure NameSpace to Long_Name;
     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 = ref true;
    36 
    37 
    38 (* assembling and issuing PGIP packets *)
    39 
    40 val pgip_refid = ref NONE: string option ref;
    41 val pgip_refseq = ref NONE: int option ref;
    42 
    43 local
    44   val pgip_class  = "pg"
    45   val pgip_tag = "Isabelle/Isar"
    46   val pgip_id = ref ""
    47   val pgip_seq = ref 0
    48   fun pgip_serial () = 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 = 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 = 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 = ref Preferences.pure_preferences;
   372 
   373 fun add_preference cat pref =
   374   CRITICAL (fn () => change preferences (Preferences.add cat pref));
   375 
   376 fun setup_preferences_tweak () =
   377   CRITICAL (fn () => 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         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 string_of_thm th = Pretty.string_of
   659                                    (Display.pretty_thm_aux
   660                                         (Syntax.pp_global (Thm.theory_of_thm th))
   661                                         false (* quote *)
   662                                         false (* show hyps *)
   663                                         [] (* asms *)
   664                                         th)
   665 
   666         fun strings_of_thm (thy, name) = map string_of_thm (PureThy.get_thms thy name)
   667 
   668         val string_of_thy = Pretty.string_of o ProofDisplay.pretty_full_theory false
   669     in
   670         case (thyname, objtype) of
   671             (_, ObjTheory) => idvalue [string_of_thy (ThyInfo.get_theory name)]
   672           | (SOME thy, ObjTheorem) => idvalue (strings_of_thm (ThyInfo.get_theory thy, name))
   673           | (NONE, ObjTheorem) => idvalue (strings_of_thm (splitthy name))
   674           | (_, ot) => error ("Cannot show objects of type "^(PgipTypes.name_of_objtype ot))
   675     end
   676 
   677 (*** Inspecting state ***)
   678 
   679 (* The file which is currently being processed interactively.
   680    In the pre-PGIP code, this was informed to Isabelle and the theory loader
   681    on completion, but that allows for circularity in case we read
   682    ourselves.  So PGIP opens the filename at the start of a script.
   683    We ought to prevent problems by modifying the theory loader to know
   684    about this special status, but for now we just keep a local reference.
   685 *)
   686 
   687 val currently_open_file = ref (NONE : pgipurl option)
   688 
   689 fun get_currently_open_file () = ! currently_open_file;
   690 
   691 fun askguise _ =
   692     (* The "guise" is the PGIP abstraction of the prover's state.
   693        The <informguise> message is merely used for consistency checking. *)
   694     let
   695         val openfile = !currently_open_file
   696 
   697         val topthy = Toplevel.theory_of o Isar.state
   698         val topthy_name = Context.theory_name o topthy
   699 
   700         val opentheory = SOME (topthy_name()) handle Toplevel.UNDEF => NONE
   701 
   702         fun topproofpos () = try Toplevel.proof_position_of (Isar.state ());
   703         val openproofpos = topproofpos()
   704     in
   705         issue_pgip (Informguise { file = openfile,
   706                                   theory = opentheory,
   707                                   (* would be nice to get thm name... *)
   708                                   theorem = NONE,
   709                                   proofpos = openproofpos })
   710     end
   711 
   712 fun parsescript (Parsescript vs) =
   713     let
   714         val text = #text vs
   715         val systemdata = #systemdata vs
   716         val location = #location vs   (* TODO: extract position *)
   717 
   718         val doc = PgipParser.pgip_parser Position.none text
   719 
   720         val sysattrs = PgipTypes.opt_attr "systemdata" systemdata
   721         val locattrs = PgipTypes.attrs_of_location location
   722      in
   723         issue_pgip (Parseresult { attrs= sysattrs@locattrs,
   724                                   doc = doc,
   725                                   errs = [] })
   726     end
   727 
   728 fun showproofstate _ = isarcmd "pr"
   729 
   730 fun showctxt _ = isarcmd "print_context"
   731 
   732 fun searchtheorems (Searchtheorems vs) =
   733     let
   734         val arg = #arg vs
   735     in
   736         isarcmd ("find_theorems " ^ arg)
   737     end
   738 
   739 fun setlinewidth (Setlinewidth vs) =
   740     let
   741         val width = #width vs
   742     in
   743         isarcmd ("pretty_setmargin " ^ Int.toString width) (* FIXME: conversion back/forth! *)
   744     end
   745 
   746 fun viewdoc (Viewdoc vs) =
   747     let
   748         val arg = #arg vs
   749     in
   750         isarcmd ("print_" ^ arg)   (* FIXME: isabelle doc?.  Return URLs, maybe? *)
   751     end
   752 
   753 (*** Theory ***)
   754 
   755 fun doitem (Doitem vs) =
   756     let
   757         val text = #text vs
   758     in
   759         isarcmd text
   760     end
   761 
   762 fun undoitem _ =
   763     isarcmd "undo"
   764 
   765 fun redoitem _ =
   766     isarcmd "redo"
   767 
   768 fun aborttheory _ =
   769     isarcmd "kill"  (* was: "init_toplevel" *)
   770 
   771 fun retracttheory (Retracttheory vs) =
   772     let
   773         val thyname = #thyname vs
   774     in
   775         isarcmd ("kill_thy " ^ quote thyname)
   776     end
   777 
   778 
   779 (*** Files ***)
   780 
   781 (* Path management: we allow theory files to have dependencies in
   782    their own directory, but when we change directory for a new file we
   783    remove the path.  Leaving it there can cause confusion with
   784    difference in batch mode.
   785    NB: PGIP does not assume that the prover has a load path.
   786 *)
   787 
   788 local
   789     val current_working_dir = ref (NONE : string option)
   790 in
   791 fun changecwd_dir newdirpath =
   792    let
   793        val newdir = File.platform_path newdirpath
   794    in
   795        (case (!current_working_dir) of
   796             NONE => ()
   797           | SOME dir => ThyLoad.del_path dir;
   798         ThyLoad.add_path newdir;
   799         current_working_dir := SOME newdir)
   800    end
   801 end
   802 
   803 fun changecwd (Changecwd vs) =
   804     let
   805         val url = #url vs
   806         val newdir = PgipTypes.path_of_pgipurl url
   807     in
   808         changecwd_dir url
   809     end
   810 
   811 fun openfile (Openfile vs) =
   812   let
   813       val url = #url vs
   814       val filepath = PgipTypes.path_of_pgipurl url
   815       val filedir = Path.dir filepath
   816       val thy_name = Path.implode o #1 o Path.split_ext o Path.base
   817       val openfile_retract = Output.no_warnings (ThyInfo.if_known_thy ThyInfo.remove_thy) o thy_name;
   818   in
   819       case !currently_open_file of
   820           SOME f => raise PGIP ("<openfile> when a file is already open!\nCurrently open file: " ^
   821                                 PgipTypes.string_of_pgipurl url)
   822         | NONE => (openfile_retract filepath;
   823                    changecwd_dir filedir;
   824                    priority ("Working in file: " ^ PgipTypes.string_of_pgipurl url);
   825                    currently_open_file := SOME url)
   826   end
   827 
   828 fun closefile _ =
   829     case !currently_open_file of
   830         SOME f => (proper_inform_file_processed f (Isar.state());
   831                    priority ("Finished working in file: " ^ PgipTypes.string_of_pgipurl f);
   832                    currently_open_file := NONE)
   833       | NONE => raise PGIP ("<closefile> when no file is open!")
   834 
   835 fun loadfile (Loadfile vs) =
   836     let
   837         val url = #url vs
   838     in
   839         (* da: this doesn't seem to cause a problem, batch loading uses
   840            a different state context.  Of course confusion is still possible,
   841            e.g. file loaded depends on open file which is not yet saved. *)
   842         (* case !currently_open_file of
   843             SOME f => raise PGIP ("<loadfile> when a file is open!\nCurrently open file: " ^
   844                                   PgipTypes.string_of_pgipurl url)
   845           | NONE => *)
   846         use_thy_or_ml_file (File.platform_path url)
   847     end
   848 
   849 fun abortfile _ =
   850     case !currently_open_file of
   851         SOME f => (isarcmd "init_toplevel";
   852                    priority ("Aborted working in file: " ^
   853                              PgipTypes.string_of_pgipurl f);
   854                    currently_open_file := NONE)
   855       | NONE => raise PGIP ("<abortfile> when no file is open!")
   856 
   857 fun retractfile (Retractfile vs) =
   858     let
   859         val url = #url vs
   860     in
   861         case !currently_open_file of
   862             SOME f => raise PGIP ("<retractfile> when a file is open!")
   863           | NONE => (priority ("Retracting file: " ^ PgipTypes.string_of_pgipurl url);
   864                      (* TODO: next should be in thy loader, here just for testing *)
   865                      let
   866                          val name = thy_name url
   867                      in List.app (tell_file_retracted false) (ThyInfo.loaded_files name) end;
   868                      inform_file_retracted url)
   869     end
   870 
   871 
   872 (*** System ***)
   873 
   874 fun systemcmd (Systemcmd vs) =
   875   let
   876       val arg = #arg vs
   877   in
   878       isarcmd arg
   879   end
   880 
   881 exception PGIP_QUIT;
   882 fun quitpgip _ = raise PGIP_QUIT
   883 
   884 fun process_input inp = case inp
   885  of Pgip.Askpgip _          => askpgip inp
   886   | Pgip.Askpgml _          => askpgml inp
   887   | Pgip.Askprefs _         => askprefs inp
   888   | Pgip.Askconfig _        => askconfig inp
   889   | Pgip.Getpref _          => getpref inp
   890   | Pgip.Setpref _          => setpref inp
   891   | Pgip.Proverinit _       => proverinit inp
   892   | Pgip.Proverexit _       => proverexit inp
   893   | Pgip.Setproverflag _    => setproverflag inp
   894   | Pgip.Dostep _           => dostep inp
   895   | Pgip.Undostep _         => undostep inp
   896   | Pgip.Redostep _         => redostep inp
   897   | Pgip.Forget _           => error "<forget> not implemented by Isabelle"
   898   | Pgip.Restoregoal _      => error "<restoregoal> not implemented by Isabelle"
   899   | Pgip.Abortgoal _        => abortgoal inp
   900   | Pgip.Askids _           => askids inp
   901   | Pgip.Askrefs _          => askrefs inp
   902   | Pgip.Showid _           => showid inp
   903   | Pgip.Askguise _         => askguise inp
   904   | Pgip.Parsescript _      => parsescript inp
   905   | Pgip.Showproofstate _   => showproofstate inp
   906   | Pgip.Showctxt _         => showctxt inp
   907   | Pgip.Searchtheorems _   => searchtheorems inp
   908   | Pgip.Setlinewidth _     => setlinewidth inp
   909   | Pgip.Viewdoc _          => viewdoc inp
   910   | Pgip.Doitem _           => doitem inp
   911   | Pgip.Undoitem _         => undoitem inp
   912   | Pgip.Redoitem _         => redoitem inp
   913   | Pgip.Aborttheory _      => aborttheory inp
   914   | Pgip.Retracttheory _    => retracttheory inp
   915   | Pgip.Loadfile _         => loadfile inp
   916   | Pgip.Openfile _         => openfile inp
   917   | Pgip.Closefile _        => closefile inp
   918   | Pgip.Abortfile _        => abortfile inp
   919   | Pgip.Retractfile _      => retractfile inp
   920   | Pgip.Changecwd _        => changecwd inp
   921   | Pgip.Systemcmd _        => systemcmd inp
   922   | Pgip.Quitpgip _         => quitpgip inp
   923 
   924 
   925 fun process_pgip_element pgipxml =
   926     case pgipxml of
   927         xml as (XML.Elem elem) =>
   928         (case Pgip.input elem of
   929              NONE => warning ("Unrecognized PGIP command, ignored: \n" ^
   930                               (XML.string_of xml))
   931            | SOME inp => (process_input inp)) (* errors later; packet discarded *)
   932       | XML.Text t => ignored_text_warning t
   933 and ignored_text_warning t =
   934     if size (Symbol.strip_blanks t) > 0 then
   935            warning ("Ignored text in PGIP packet: \n" ^ t)
   936     else ()
   937 
   938 fun process_pgip_tree xml =
   939     (pgip_refid := NONE;
   940      pgip_refseq := NONE;
   941      (case xml of
   942           XML.Elem ("pgip", attrs, pgips) =>
   943           (let
   944                val class = PgipTypes.get_attr "class" attrs
   945                val dest  = PgipTypes.get_attr_opt "destid" attrs
   946                val seq = PgipTypes.read_pgipnat (PgipTypes.get_attr "seq" attrs)
   947                (* Respond to prover broadcasts, or messages for us. Ignore rest *)
   948                val processit =
   949                    case dest of
   950                        NONE =>    class = "pa"
   951                      | SOME id => matching_pgip_id id
   952            in if processit then
   953                   (pgip_refid :=  PgipTypes.get_attr_opt "id" attrs;
   954                    pgip_refseq := SOME seq;
   955                    List.app process_pgip_element pgips;
   956                    (* return true to indicate <ready/> *)
   957                    true)
   958               else
   959                   (* no response to ignored messages. *)
   960                   false
   961            end)
   962         | _ => raise PGIP "Invalid PGIP packet received")
   963      handle PGIP msg =>
   964             (Output.error_msg ((msg ^ "\nPGIP error occured in XML text below:\n") ^
   965                                (XML.string_of xml));
   966              true))
   967 
   968 (* External input *)
   969 
   970 val process_pgip_plain = K () o process_pgip_tree o XML.parse
   971 
   972 (* PGIP loop: process PGIP input only *)
   973 
   974 local
   975 
   976 exception XML_PARSE
   977 
   978 fun loop ready src =
   979     let
   980         val _ = if ready then issue_pgip (Ready ()) else ()
   981         val pgipo =
   982           (case try Source.get_single src of
   983             SOME pgipo => pgipo
   984           | NONE => raise XML_PARSE)
   985     in
   986         case pgipo of
   987              NONE  => ()
   988            | SOME (pgip,src') =>
   989              let
   990                  val ready' = (process_pgip_tree pgip)
   991                                 handle PGIP_QUIT => raise PGIP_QUIT
   992                                      | e => (handler (e,SOME src'); true)
   993              in
   994                  loop ready' src'
   995              end
   996     end handle e => handler (e,SOME src)  (* error in XML parse or Ready issue *)
   997 
   998 and handler (e,srco) =
   999     case (e,srco) of
  1000         (XML_PARSE,SOME src) =>
  1001         panic "Invalid XML input, aborting" (* TODO: attempt recovery  *)
  1002       | (Exn.Interrupt,SOME src) =>
  1003         (Output.error_msg "Interrupt during PGIP processing"; loop true src)
  1004       | (Toplevel.UNDEF,SOME src) =>
  1005         (Output.error_msg "No working context defined"; loop true src)
  1006       | (e,SOME src) =>
  1007         (Output.error_msg (Toplevel.exn_message e); loop true src)
  1008       | (PGIP_QUIT,_) => ()
  1009       | (_,NONE) => ()
  1010 in
  1011   (* TODO: add socket interface *)
  1012 
  1013   val xmlP = XML.parse_comments |-- XML.parse_element >> single
  1014 
  1015   val tty_src = Source.set_prompt "" (Source.source Symbol.stopper xmlP NONE Source.tty)
  1016 
  1017   fun pgip_toplevel x = loop true x
  1018 end
  1019 
  1020 
  1021 (* Extra command for embedding prover-control inside document (obscure/debug usage). *)
  1022 
  1023 fun init_outer_syntax () =
  1024   OuterSyntax.improper_command "ProofGeneral.process_pgip" "(internal)" OuterKeyword.control
  1025     (OuterParse.text >> (Toplevel.no_timing oo
  1026       (fn txt => Toplevel.imperative (fn () => process_pgip_plain txt))));
  1027 
  1028 
  1029 (* init *)
  1030 
  1031 val initialized = ref false;
  1032 
  1033 fun init_pgip false = panic "No Proof General interface support for Isabelle/classic mode."
  1034   | init_pgip true =
  1035       (! initialized orelse
  1036         (setup_preferences_tweak ();
  1037          Output.add_mode proof_generalN Output.default_output Output.default_escape;
  1038          Markup.add_mode proof_generalN YXML.output_markup;
  1039          setup_messages ();
  1040          Output.no_warnings init_outer_syntax ();
  1041          setup_thy_loader ();
  1042          setup_present_hook ();
  1043          init_pgip_session_id ();
  1044          welcome ();
  1045          set initialized);
  1046         sync_thy_loader ();
  1047        change print_mode (update (op =) proof_generalN);
  1048        pgip_toplevel tty_src);
  1049 
  1050 
  1051 
  1052 (** Out-of-loop PGIP commands (for Emacs hybrid mode) **)
  1053 
  1054 local
  1055     val pgip_output_channel = ref Output.writeln_default
  1056 in
  1057 
  1058 (* Set recipient for PGIP results *)
  1059 fun init_pgip_channel writefn =
  1060     (init_pgip_session_id();
  1061      pgip_output_channel := writefn)
  1062 
  1063 (* Process a PGIP command.
  1064    This works for preferences but not generally guaranteed
  1065    because we haven't done full setup here (e.g., no pgml mode)  *)
  1066 fun process_pgip str =
  1067      setmp output_xml_fn (!pgip_output_channel) process_pgip_plain str
  1068 
  1069 end
  1070 
  1071 end;