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