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