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