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