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