src/Pure/ProofGeneral/proof_general_pgip.ML
author wenzelm
Sun May 18 15:04:09 2008 +0200 (2008-05-18)
changeset 26939 1035c89b4c02
parent 26723 3e4bb1ca9a74
child 27177 adefd3454174
permissions -rw-r--r--
moved global pretty/string_of functions from Sign to Syntax;
     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 commands = OuterSyntax.dest_keywords ()
   363         fun category_of k = if k mem commands then "major" else "minor"
   364          (* NB: we might filter to only include words like elisp case (OuterSyntax.is_keyword). *)
   365         fun keyword_elt (keyword,help,kind,_) =
   366             XML.Elem("keyword", [("word", keyword), ("category", category_of kind)],
   367                      [XML.Elem("shorthelp", [], [XML.Text help])])
   368         in
   369             (* Also, note we don't call init_outer_syntax here to add interface commands,
   370             but they should never appear in scripts anyway so it shouldn't matter *)
   371             Lexicalstructure {content = map keyword_elt (OuterSyntax.dest_parsers()) }
   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, e.g. IsarCmd.undo.
   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 _ = isarcmd "redo"
   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 fun askids (Askids vs) =
   567     let
   568         val url = #url vs            (* ask for identifiers within a file *)
   569         val thyname = #thyname vs    (* ask for identifiers within a theory *)
   570         val objtype = #objtype vs    (* ask for identifiers of a particular type *)
   571 
   572         fun idtable ty ctx ids = {objtype=ty,context=ctx,ids=ids}
   573 
   574         fun setids t = issue_pgip (Setids {idtables = [t]})
   575 
   576         (* fake one-level nested "subtheories" by picking apart names. *)
   577         val thms_of_thy =
   578             map fst o NameSpace.extern_table o PureThy.theorems_of o ThyInfo.get_theory
   579         val immed_thms_of_thy = filter_out NameSpace.is_qualified o thms_of_thy
   580         fun thy_prefix s = case space_explode NameSpace.separator s of
   581                                     x::_::_ => SOME x  (* String.find? *)
   582                                   | _ => NONE
   583         fun subthys_of_thy s =
   584             List.foldl  (fn (NONE,xs) => xs | (SOME x,xs) => insert op= x xs) []
   585                    (map thy_prefix (thms_of_thy s))
   586         fun subthms_of_thy thy =
   587             (case thy_prefix thy of
   588                  NONE => immed_thms_of_thy thy
   589                | SOME prf => filter (String.isPrefix (unprefix (prf ^ NameSpace.separator) thy))
   590                                     (thms_of_thy prf))
   591        val qualified_thms_of_thy = (* for global query with single response *)
   592             (map fst) o NameSpace.dest_table o PureThy.theorems_of o ThyInfo.get_theory;
   593 (* da: this version is equivalent to my previous, but splits up theorem sets with names
   594    that I can't get to access later with get_thm.  Anyway, would rather use sets.
   595    Is above right way to get qualified names in that case?  Filtering required again?
   596             map PureThy.get_name_hint o filter PureThy.has_name_hint o
   597               map snd o PureThy.thms_of o ThyInfo.get_theory; *)
   598     in
   599         case (thyname,objtype) of
   600            (NONE, NONE) =>
   601            setids (idtable ObjFile NONE (ThyInfo.get_names())) (*FIXME: uris*)
   602          | (NONE, SOME ObjFile) =>
   603            setids (idtable ObjFile NONE (ThyInfo.get_names())) (*FIXME: uris*)
   604          | (SOME fi, SOME ObjFile) =>
   605            setids (idtable ObjTheory (SOME fi) [fi])       (* TODO: check exists *)
   606          | (NONE, SOME ObjTheory) =>
   607            setids (idtable ObjTheory NONE (ThyInfo.get_names()))
   608          | (SOME thy, SOME ObjTheory) =>
   609            setids (idtable ObjTheory (SOME thy) (subthys_of_thy thy))
   610          | (SOME thy, SOME ObjTheorem) =>
   611            setids (idtable ObjTheorem (SOME thy) (subthms_of_thy thy))
   612          | (NONE, SOME ObjTheorem) =>
   613            (* A large query, but not unreasonable. ~5000 results for HOL.*)
   614            (* Several setids should be allowed, but Eclipse code is currently broken:
   615               List.app (fn thy => setids (idtable ObjTheorem (SOME thy) (subthms_of_thy thy)))
   616                          (ThyInfo.get_names()) *)
   617            setids (idtable ObjTheorem NONE (* this one gives ~7000 for HOL *)
   618                            (maps qualified_thms_of_thy (ThyInfo.get_names())))
   619          | _ => warning ("askids: ignored argument combination")
   620     end
   621 
   622 fun askrefs (Askrefs vs) =
   623     let
   624         val url = #url vs            (* ask for references of a file (i.e. immediate pre-requisites) *)
   625         val thyname = #thyname vs    (* ask for references of a theory (other theories) *)
   626         val objtype = #objtype vs    (* ask for references of a particular type... *)
   627         val name = #name vs          (*   ... with this name *)
   628 
   629         fun idtable ty ctx ids = {objtype=ty,context=ctx,ids=ids}
   630 
   631         val thy_name = Path.implode o #1 o Path.split_ext o Path.base
   632 
   633         fun filerefs f =
   634             let val thy = thy_name f
   635                 val filerefs = #uses (ThyLoad.deps_thy (Path.dir f) thy)
   636             in
   637                 issue_pgip (Setrefs {url=url, thyname=NONE, objtype=SOME PgipTypes.ObjFile,
   638                                      name=NONE, idtables=[], fileurls=filerefs})
   639             end
   640 
   641         fun thyrefs thy =
   642             let val thyrefs = #imports (ThyLoad.deps_thy Path.current thy)
   643             in
   644                 issue_pgip (Setrefs {url=url, thyname=thyname, objtype=SOME PgipTypes.ObjTheory,
   645                                      name=NONE, idtables=[{context=NONE, objtype=PgipTypes.ObjTheory,
   646                                                            ids=thyrefs}], fileurls=[]})
   647             end
   648 
   649         fun thmrefs thmname =
   650             let
   651                 (* TODO: interim: this is probably not right.
   652                    What we want is mapping onto simple PGIP name/context model. *)
   653                 val ctx = Toplevel.context_of (Isar.state ()) (* NB: raises UNDEF *)
   654                 val thy = Context.theory_of_proof ctx
   655                 val ths = [PureThy.get_thm thy thmname]
   656                 val deps = filter_out (equal "")
   657                                       (Symtab.keys (fold Proofterm.thms_of_proof
   658                                                          (map Thm.proof_of ths) Symtab.empty))
   659             in
   660                 if null deps then ()
   661                 else issue_pgip (Setrefs {url=url, thyname=thyname, name=name,
   662                                           objtype=SOME PgipTypes.ObjTheorem,
   663                                           idtables=[{context=NONE, objtype=PgipTypes.ObjTheorem,
   664                                                      ids=deps}], fileurls=[]})
   665             end
   666     in
   667         case (url,thyname,objtype,name) of
   668             (SOME file, NONE, _, _)  => filerefs file
   669           | (_,SOME thy,_,_)         => thyrefs thy
   670           | (_,_,SOME PgipTypes.ObjTheorem,SOME thmname) => thmrefs thmname
   671           | _  => error ("Unimplemented/invalid case of <askrefs>")
   672     end
   673 
   674 
   675 
   676 fun showid (Showid vs) =
   677     let
   678         val thyname = #thyname vs
   679         val objtype = #objtype vs
   680         val name = #name vs
   681 
   682         val topthy = Toplevel.theory_of o Isar.state
   683 
   684         fun splitthy id =
   685             let val comps = NameSpace.explode id
   686             in case comps of
   687                    (thy::(rest as _::_)) => (ThyInfo.get_theory thy, space_implode "." rest)
   688                  | [plainid] => (topthy(),plainid)
   689                  | _ => raise Toplevel.UNDEF (* assert false *)
   690             end
   691 
   692 
   693         fun idvalue strings =
   694             issue_pgip (Idvalue { thyname=thyname, objtype=objtype, name=name,
   695                                   text=[XML.Elem("pgml",[],
   696                                                  map XML.Output strings)] })
   697 
   698         fun string_of_thm th = Output.output
   699                                (Pretty.string_of
   700                                    (Display.pretty_thm_aux
   701                                         (Syntax.pp_global (Thm.theory_of_thm th))
   702                                         false (* quote *)
   703                                         false (* show hyps *)
   704                                         [] (* asms *)
   705                                         th))
   706 
   707         fun strings_of_thm (thy, name) = map string_of_thm (PureThy.get_thms thy name)
   708 
   709         val string_of_thy = Output.output o
   710                                 Pretty.string_of o (ProofDisplay.pretty_full_theory false)
   711     in
   712         case (thyname, objtype) of
   713             (_,ObjTheory) => idvalue [string_of_thy (ThyInfo.get_theory name)]
   714           | (SOME thy, ObjTheorem) => idvalue (strings_of_thm (ThyInfo.get_theory thy, name))
   715           | (NONE, ObjTheorem) => idvalue (strings_of_thm (splitthy name))
   716           | (_, ot) => error ("Cannot show objects of type "^(PgipTypes.name_of_objtype ot))
   717     end
   718 
   719 (*** Inspecting state ***)
   720 
   721 (* The file which is currently being processed interactively.
   722    In the pre-PGIP code, this was informed to Isabelle and the theory loader
   723    on completion, but that allows for circularity in case we read
   724    ourselves.  So PGIP opens the filename at the start of a script.
   725    We ought to prevent problems by modifying the theory loader to know
   726    about this special status, but for now we just keep a local reference.
   727 *)
   728 
   729 val currently_open_file = ref (NONE : pgipurl option)
   730 
   731 fun get_currently_open_file () = ! currently_open_file;
   732 
   733 fun askguise _ =
   734     (* The "guise" is the PGIP abstraction of the prover's state.
   735        The <informguise> message is merely used for consistency checking. *)
   736     let
   737         val openfile = !currently_open_file
   738 
   739         val topthy = Toplevel.theory_of o Isar.state
   740         val topthy_name = Context.theory_name o topthy
   741 
   742         val opentheory = SOME (topthy_name()) handle Toplevel.UNDEF => NONE
   743 
   744         fun topproofpos () = try Toplevel.proof_position_of (Isar.state ());
   745         val openproofpos = topproofpos()
   746     in
   747         issue_pgip (Informguise { file = openfile,
   748                                   theory = opentheory,
   749                                   (* would be nice to get thm name... *)
   750                                   theorem = NONE,
   751                                   proofpos = openproofpos })
   752     end
   753 
   754 fun parsescript (Parsescript vs) =
   755     let
   756         val text = #text vs
   757         val systemdata = #systemdata vs
   758         val location = #location vs   (* TODO: extract position *)
   759 
   760         val _ = start_delay_msgs ()   (* gather parsing errs/warns *)
   761 		    val doc = PgipParser.pgip_parser Position.none text
   762         val errs = end_delayed_msgs ()
   763 
   764         val sysattrs = PgipTypes.opt_attr "systemdata" systemdata
   765         val locattrs = PgipTypes.attrs_of_location location
   766      in
   767         issue_pgip (Parseresult { attrs= sysattrs@locattrs,
   768                                   doc = doc,
   769                                   errs = map PgipOutput.output errs })
   770     end
   771 
   772 fun showproofstate _ = isarcmd "pr"
   773 
   774 fun showctxt _ = isarcmd "print_context"
   775 
   776 fun searchtheorems (Searchtheorems vs) =
   777     let
   778         val arg = #arg vs
   779     in
   780         isarcmd ("find_theorems " ^ arg)
   781     end
   782 
   783 fun setlinewidth (Setlinewidth vs) =
   784     let
   785         val width = #width vs
   786     in
   787         isarcmd ("pretty_setmargin " ^ Int.toString width) (* FIXME: conversion back/forth! *)
   788     end
   789 
   790 fun viewdoc (Viewdoc vs) =
   791     let
   792         val arg = #arg vs
   793     in
   794         isarcmd ("print_" ^ arg)   (* FIXME: isatool doc?.  Return URLs, maybe? *)
   795     end
   796 
   797 (*** Theory ***)
   798 
   799 fun doitem (Doitem vs) =
   800     let
   801         val text = #text vs
   802     in
   803         isarcmd text
   804     end
   805 
   806 fun undoitem _ =
   807     isarcmd "undo"
   808 
   809 fun redoitem _ =
   810     isarcmd "redo"
   811 
   812 fun aborttheory _ =
   813     isarcmd "kill"  (* was: "init_toplevel" *)
   814 
   815 fun retracttheory (Retracttheory vs) =
   816     let
   817         val thyname = #thyname vs
   818     in
   819         isarcmd ("kill_thy " ^ quote thyname)
   820     end
   821 
   822 
   823 (*** Files ***)
   824 
   825 (* Path management: we allow theory files to have dependencies in
   826    their own directory, but when we change directory for a new file we
   827    remove the path.  Leaving it there can cause confusion with
   828    difference in batch mode.
   829    NB: PGIP does not assume that the prover has a load path.
   830 *)
   831 
   832 local
   833     val current_working_dir = ref (NONE : string option)
   834 in
   835 fun changecwd_dir newdirpath =
   836    let
   837        val newdir = File.platform_path newdirpath
   838    in
   839        (case (!current_working_dir) of
   840             NONE => ()
   841           | SOME dir => ThyLoad.del_path dir;
   842         ThyLoad.add_path newdir;
   843         current_working_dir := SOME newdir)
   844    end
   845 end
   846 
   847 fun changecwd (Changecwd vs) =
   848     let
   849         val url = #url vs
   850         val newdir = PgipTypes.path_of_pgipurl url
   851     in
   852         changecwd_dir url
   853     end
   854 
   855 fun openfile (Openfile vs) =
   856   let
   857       val url = #url vs
   858       val filepath = PgipTypes.path_of_pgipurl url
   859       val filedir = Path.dir filepath
   860       val thy_name = Path.implode o #1 o Path.split_ext o Path.base
   861       val openfile_retract = Output.no_warnings (ThyInfo.if_known_thy ThyInfo.remove_thy) o thy_name;
   862   in
   863       case !currently_open_file of
   864           SOME f => raise PGIP ("<openfile> when a file is already open!\nCurrently open file: " ^
   865                                 PgipTypes.string_of_pgipurl url)
   866         | NONE => (openfile_retract filepath;
   867                    changecwd_dir filedir;
   868                    priority ("Working in file: " ^ PgipTypes.string_of_pgipurl url);
   869                    currently_open_file := SOME url)
   870   end
   871 
   872 fun closefile _ =
   873     case !currently_open_file of
   874         SOME f => (proper_inform_file_processed f (Isar.state());
   875                    priority ("Finished working in file: " ^ PgipTypes.string_of_pgipurl f);
   876                    currently_open_file := NONE)
   877       | NONE => raise PGIP ("<closefile> when no file is open!")
   878 
   879 fun loadfile (Loadfile vs) =
   880     let
   881         val url = #url vs
   882     in
   883         (* da: this doesn't seem to cause a problem, batch loading uses
   884            a different state context.  Of course confusion is still possible,
   885            e.g. file loaded depends on open file which is not yet saved. *)
   886         (* case !currently_open_file of
   887             SOME f => raise PGIP ("<loadfile> when a file is open!\nCurrently open file: " ^
   888                                   PgipTypes.string_of_pgipurl url)
   889           | NONE => *)
   890         use_thy_or_ml_file (File.platform_path url)
   891     end
   892 
   893 fun abortfile _ =
   894     case !currently_open_file of
   895         SOME f => (isarcmd "init_toplevel";
   896                    priority ("Aborted working in file: " ^
   897                              PgipTypes.string_of_pgipurl f);
   898                    currently_open_file := NONE)
   899       | NONE => raise PGIP ("<abortfile> when no file is open!")
   900 
   901 fun retractfile (Retractfile vs) =
   902     let
   903         val url = #url vs
   904     in
   905         case !currently_open_file of
   906             SOME f => raise PGIP ("<retractfile> when a file is open!")
   907           | NONE => (priority ("Retracting file: " ^ PgipTypes.string_of_pgipurl url);
   908                      (* TODO: next should be in thy loader, here just for testing *)
   909                      let
   910                          val name = thy_name url
   911                      in List.app (tell_file_retracted false) (ThyInfo.loaded_files name) end;
   912                      inform_file_retracted url)
   913     end
   914 
   915 
   916 (*** System ***)
   917 
   918 fun systemcmd (Systemcmd vs) =
   919   let
   920       val arg = #arg vs
   921   in
   922       isarcmd arg
   923   end
   924 
   925 exception PGIP_QUIT;
   926 fun quitpgip _ = raise PGIP_QUIT
   927 
   928 fun process_input inp = case inp
   929  of Pgip.Askpgip _          => askpgip inp
   930   | Pgip.Askpgml _          => askpgml inp
   931   | Pgip.Askprefs _         => askprefs inp
   932   | Pgip.Askconfig _        => askconfig inp
   933   | Pgip.Getpref _          => getpref inp
   934   | Pgip.Setpref _          => setpref inp
   935   | Pgip.Proverinit _       => proverinit inp
   936   | Pgip.Proverexit _       => proverexit inp
   937   | Pgip.Setproverflag _    => setproverflag inp
   938   | Pgip.Dostep _           => dostep inp
   939   | Pgip.Undostep _         => undostep inp
   940   | Pgip.Redostep _         => redostep inp
   941   | Pgip.Forget _           => error "<forget> not implemented by Isabelle"
   942   | Pgip.Restoregoal _      => error "<restoregoal> not implemented by Isabelle"
   943   | Pgip.Abortgoal _        => abortgoal inp
   944   | Pgip.Askids _           => askids inp
   945   | Pgip.Askrefs _          => askrefs inp
   946   | Pgip.Showid _           => showid inp
   947   | Pgip.Askguise _         => askguise inp
   948   | Pgip.Parsescript _      => parsescript inp
   949   | Pgip.Showproofstate _   => showproofstate inp
   950   | Pgip.Showctxt _         => showctxt inp
   951   | Pgip.Searchtheorems _   => searchtheorems inp
   952   | Pgip.Setlinewidth _     => setlinewidth inp
   953   | Pgip.Viewdoc _          => viewdoc inp
   954   | Pgip.Doitem _           => doitem inp
   955   | Pgip.Undoitem _         => undoitem inp
   956   | Pgip.Redoitem _         => redoitem inp
   957   | Pgip.Aborttheory _      => aborttheory inp
   958   | Pgip.Retracttheory _    => retracttheory inp
   959   | Pgip.Loadfile _         => loadfile inp
   960   | Pgip.Openfile _         => openfile inp
   961   | Pgip.Closefile _        => closefile inp
   962   | Pgip.Abortfile _        => abortfile inp
   963   | Pgip.Retractfile _      => retractfile inp
   964   | Pgip.Changecwd _        => changecwd inp
   965   | Pgip.Systemcmd _        => systemcmd inp
   966   | Pgip.Quitpgip _         => quitpgip inp
   967 
   968 
   969 fun process_pgip_element pgipxml =
   970     case pgipxml of
   971         xml as (XML.Elem elem) =>
   972         (case Pgip.input elem of
   973              NONE => warning ("Unrecognized PGIP command, ignored: \n" ^
   974                               (XML.string_of xml))
   975            | SOME inp => (process_input inp)) (* errors later; packet discarded *)
   976       | XML.Text t => ignored_text_warning t
   977       | XML.Output t => ignored_text_warning t
   978 and ignored_text_warning t =
   979     if size (Symbol.strip_blanks t) > 0 then
   980            warning ("Ignored text in PGIP packet: \n" ^ t)
   981     else ()
   982 
   983 fun process_pgip_tree xml =
   984     (pgip_refid := NONE;
   985      pgip_refseq := NONE;
   986      (case xml of
   987           XML.Elem ("pgip", attrs, pgips) =>
   988           (let
   989                val class = PgipTypes.get_attr "class" attrs
   990                val dest  = PgipTypes.get_attr_opt "destid" attrs
   991                val seq = PgipTypes.read_pgipnat (PgipTypes.get_attr "seq" attrs)
   992                (* Respond to prover broadcasts, or messages for us. Ignore rest *)
   993                val processit =
   994                    case dest of
   995                        NONE =>    class = "pa"
   996                      | SOME id => matching_pgip_id id
   997            in if processit then
   998                   (pgip_refid :=  PgipTypes.get_attr_opt "id" attrs;
   999                    pgip_refseq := SOME seq;
  1000                    List.app process_pgip_element pgips;
  1001                    (* return true to indicate <ready/> *)
  1002                    true)
  1003               else
  1004                   (* no response to ignored messages. *)
  1005                   false
  1006            end)
  1007         | _ => raise PGIP "Invalid PGIP packet received")
  1008      handle PGIP msg =>
  1009             (Output.error_msg ((msg ^ "\nPGIP error occured in XML text below:\n") ^
  1010                                (XML.string_of xml));
  1011              true))
  1012 
  1013 (* External input *)
  1014 
  1015 val process_pgip_plain = K () o process_pgip_tree o XML.parse
  1016 
  1017 (* PGIP loop: process PGIP input only *)
  1018 
  1019 local
  1020 
  1021 exception XML_PARSE
  1022 
  1023 fun loop ready src =
  1024     let
  1025         val _ = if ready then issue_pgip (Ready ()) else ()
  1026         val pgipo =
  1027           (case try Source.get_single src of
  1028             SOME pgipo => pgipo
  1029           | NONE => raise XML_PARSE)
  1030     in
  1031         case pgipo of
  1032              NONE  => ()
  1033            | SOME (pgip,src') =>
  1034              let
  1035                  val ready' = (process_pgip_tree pgip)
  1036                                 handle PGIP_QUIT => raise PGIP_QUIT
  1037                                      | e => (handler (e,SOME src'); true)
  1038              in
  1039                  loop ready' src'
  1040              end
  1041     end handle e => handler (e,SOME src)  (* error in XML parse or Ready issue *)
  1042 
  1043 and handler (e,srco) =
  1044     case (e,srco) of
  1045         (XML_PARSE,SOME src) =>
  1046         panic "Invalid XML input, aborting" (* TODO: attempt recovery  *)
  1047       | (Interrupt,SOME src) =>
  1048         (Output.error_msg "Interrupt during PGIP processing"; loop true src)
  1049       | (Toplevel.UNDEF,SOME src) =>
  1050         (Output.error_msg "No working context defined"; loop true src)
  1051       | (e,SOME src) =>
  1052         (Output.error_msg (Toplevel.exn_message e); loop true src)
  1053       | (PGIP_QUIT,_) => ()
  1054       | (_,NONE) => ()
  1055 in
  1056   (* TODO: add socket interface *)
  1057 
  1058   val xmlP = XML.parse_comments |-- XML.parse_element >> single
  1059 
  1060   val tty_src = Source.set_prompt "" (Source.source Symbol.stopper xmlP NONE Source.tty)
  1061 
  1062   fun pgip_toplevel x = loop true x
  1063 end
  1064 
  1065 
  1066 (* Extra command for embedding prover-control inside document (obscure/debug usage). *)
  1067 
  1068 fun init_outer_syntax () =
  1069   OuterSyntax.improper_command "ProofGeneral.process_pgip" "(internal)" OuterKeyword.control
  1070     (OuterParse.text >> (Toplevel.no_timing oo
  1071       (fn txt => Toplevel.imperative (fn () => process_pgip_plain txt))));
  1072 
  1073 
  1074 (* init *)
  1075 
  1076 val initialized = ref false;
  1077 
  1078 fun init_pgip false = panic "No Proof General interface support for Isabelle/classic mode."
  1079   | init_pgip true =
  1080       (! initialized orelse
  1081         (setup_preferences_tweak ();
  1082          setup_proofgeneral_output ();
  1083          setup_messages ();
  1084          Output.no_warnings init_outer_syntax ();
  1085          setup_thy_loader ();
  1086          setup_present_hook ();
  1087          init_pgip_session_id ();
  1088          welcome ();
  1089          set initialized);
  1090         sync_thy_loader ();
  1091        change print_mode (cons proof_generalN o remove (op =) proof_generalN);
  1092        pgip_toplevel tty_src);
  1093 
  1094 
  1095 
  1096 (** Out-of-loop PGIP commands (for Emacs hybrid mode) **)
  1097 
  1098 local
  1099     val pgip_output_channel = ref Output.writeln_default
  1100 in
  1101 
  1102 (* Set recipient for PGIP results *)
  1103 fun init_pgip_channel writefn =
  1104     (init_pgip_session_id();
  1105      pgip_output_channel := writefn)
  1106 
  1107 (* Process a PGIP command.
  1108    This works for preferences but not generally guaranteed
  1109    because we haven't done full setup here (e.g., no pgml mode)  *)
  1110 fun process_pgip str =
  1111      setmp output_xml_fn (!pgip_output_channel) process_pgip_plain str
  1112 
  1113 end
  1114 
  1115 end;
  1116