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