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