src/Pure/ProofGeneral/proof_general_pgip.ML
author aspinall
Sun Jan 07 14:05:44 2007 +0100 (2007-01-07 ago)
changeset 22028 c13f6b5bf2b8
parent 22014 4b70cbd96007
child 22042 64f8f5433f30
permissions -rw-r--r--
Be more chatty in PGIP file operations.
     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 end
    17 
    18 structure ProofGeneralPgip : PROOF_GENERAL_PGIP  =
    19 struct
    20 
    21 open Pgip;
    22 
    23 
    24 (* print modes *)
    25 
    26 val proof_generalN = "ProofGeneral";  (*token markup (colouring vars, etc.)*)
    27 val pgmlN = "PGML";                   (*XML escapes and PGML symbol elements*)
    28 val pgmlatomsN = "PGMLatoms";         (*variable kind decorations*)
    29 val thm_depsN = "thm_deps";           (*meta-information about theorem deps*)
    30 
    31 
    32 (* text output: print modes for xsymbol and PGML *)
    33 
    34 local
    35 
    36 fun xsym_output "\\" = "\\\\"
    37   | xsym_output s = if Symbol.is_raw s then Symbol.decode_raw s else s;
    38 
    39 fun xsymbols_output s =
    40   if Output.has_mode Symbol.xsymbolsN andalso exists_string (equal "\\") s then
    41     let val syms = Symbol.explode s
    42     in (implode (map xsym_output syms), real (Symbol.length syms)) end
    43   else Symbol.default_output s;
    44 
    45 (* XML immediately rendered pretty printer. Take care not to double escape *)
    46 fun pgml_sym s =
    47   (case Symbol.decode s of
    48     Symbol.Char s => XML.text s
    49   | Symbol.Sym sn => XML.element "sym" [("name", sn)] [XML.text s]
    50   | Symbol.Ctrl sn => XML.element "ctrl" [("name", sn)] [XML.text s] (* FIXME: no such PGML! *)
    51   | Symbol.Raw s => s);
    52 
    53 fun pgml_output str =
    54   let val syms = Symbol.explode str
    55   in (implode (map pgml_sym syms), real (Symbol.length syms)) end;
    56 
    57 in
    58 
    59 fun setup_xsymbols_output () =
    60   Output.add_mode Symbol.xsymbolsN
    61     (xsymbols_output, K xsymbols_output, Symbol.default_indent, Symbol.encode_raw);
    62 
    63 fun setup_pgml_output () =
    64   Output.add_mode pgmlN
    65     (pgml_output, K pgml_output, Symbol.default_indent, Symbol.encode_raw);
    66 
    67 end;
    68 
    69 
    70 (* token translations *)
    71 
    72 local
    73 
    74 val class_tag = "class"
    75 val tfree_tag = "tfree"
    76 val tvar_tag = "tvar"
    77 val free_tag = "free"
    78 val bound_tag = "bound"
    79 val var_tag = "var"
    80 val skolem_tag = "skolem"
    81 
    82 fun xml_atom kind x = XML.element "atom" [("kind", kind)] [XML.text x];
    83 
    84 fun tagit kind x =
    85   (xml_atom kind x, real (Symbol.length (Symbol.explode x)));
    86 
    87 fun free_or_skolem x =
    88   (case try Name.dest_skolem x of
    89     NONE => tagit free_tag x
    90   | SOME x' => tagit skolem_tag x');
    91 
    92 fun var_or_skolem s =
    93   (case Syntax.read_variable s of
    94     SOME (x, i) =>
    95       (case try Name.dest_skolem x of
    96         NONE => tagit var_tag s
    97       | SOME x' => tagit skolem_tag
    98           (setmp show_question_marks true Syntax.string_of_vname (x', i)))
    99   | NONE => tagit var_tag s);
   100 
   101 val proof_general_trans =
   102  Syntax.tokentrans_mode proof_generalN
   103   [("class", tagit class_tag),
   104    ("tfree", tagit tfree_tag),
   105    ("tvar", tagit tvar_tag),
   106    ("free", free_or_skolem),
   107    ("bound", tagit bound_tag),
   108    ("var", var_or_skolem)];
   109 
   110 in
   111 
   112 val _ = Context.add_setup (Theory.add_tokentrfuns proof_general_trans);
   113 
   114 end;
   115 
   116 
   117 (** assembling and issuing PGIP packets **)
   118 
   119 val pgip_refid  = ref NONE: string option ref;
   120 val pgip_refseq = ref NONE: int option ref;
   121 
   122 local
   123   val pgip_class  = "pg"
   124   val pgip_tag = "Isabelle/Isar"
   125   val pgip_id = ref ""
   126   val pgip_seq = ref 0
   127   fun pgip_serial () = inc pgip_seq
   128 
   129   fun assemble_pgips pgips =
   130     Pgip { tag = SOME pgip_tag,
   131            class = pgip_class,
   132            seq = pgip_serial(),
   133            id = !pgip_id,
   134            destid = !pgip_refid,
   135            (* destid=refid since Isabelle only communicates back to sender *)
   136            refid  = !pgip_refid,
   137            refseq = !pgip_refseq,
   138            content = pgips }
   139 in
   140 
   141 fun init_pgip_session_id () =
   142     pgip_id := getenv "HOSTNAME" ^ "/" ^ getenv "USER" ^ "/" ^
   143                getenv "ISABELLE_PID" ^ "/" ^ Time.toString (Time.now ())
   144 
   145 fun matching_pgip_id id = (id = !pgip_id)
   146 
   147 val output_xml_fn = ref writeln_default
   148 fun output_xml s = (!output_xml_fn) (XML.string_of_tree s);  (* TODO: string buffer *)
   149 
   150 fun issue_pgip_rawtext str =
   151     output_xml (PgipOutput.output (assemble_pgips [XML.Rawtext str]))
   152 
   153 fun issue_pgips pgipops =
   154     output_xml (PgipOutput.output (assemble_pgips (map PgipOutput.output pgipops)));
   155 
   156 fun issue_pgip pgipop =
   157     output_xml (PgipOutput.output (assemble_pgips [PgipOutput.output pgipop]));
   158 
   159 end;
   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     fun normalmsg area cat urgent s =
   174         let
   175             val content = XML.Elem("pgmltext",[],[XML.Rawtext s])
   176             val pgip = Normalresponse {area=area,messagecategory=cat,
   177                                        urgent=urgent,content=[content] }
   178         in
   179             queue_or_issue pgip
   180         end
   181 
   182     fun errormsg fatality s =
   183         let
   184               val content = XML.Elem("pgmltext",[],[XML.Rawtext s])
   185               val pgip = Errorresponse {area=NONE,fatality=fatality,
   186                                         content=[content],
   187                                         (* FIXME: pass in locations *)
   188                                         location=NONE}
   189         in
   190             queue_or_issue pgip
   191         end
   192 
   193     fun start_delay_msgs () = (set delay_msgs; delayed_msgs := [])
   194     fun end_delayed_msgs () = (reset delay_msgs; ! delayed_msgs)
   195 end;
   196 
   197 (* NB: all of the standard error/message functions now expect already-escaped text.
   198    FIXME: this may cause us problems now we're generating trees; on the other
   199    hand the output functions were tuned some time ago, so it ought to be
   200    enough to use Rawtext always above. *)
   201 
   202 fun setup_messages () =
   203  (writeln_fn := (fn s => normalmsg Message Normal false s);
   204   priority_fn := (fn s => normalmsg Message Normal true s);
   205   tracing_fn := (fn s => normalmsg  Message Tracing false s);
   206   info_fn := (fn s => normalmsg Message Information false s);
   207   debug_fn := (fn s => normalmsg Message Internal false s);
   208   warning_fn := (fn s => errormsg Warning s);
   209   error_fn := (fn s => errormsg Fatal s);
   210   panic_fn := (fn s => errormsg Panic s));
   211 
   212 
   213 (* immediate messages *)
   214 
   215 fun tell_clear_goals ()      = issue_pgip (Cleardisplay {area=Display})
   216 fun tell_clear_response ()   = issue_pgip (Cleardisplay {area=Message})
   217 fun tell_file_loaded path    = issue_pgip (Informfileloaded {url=PgipTypes.pgipurl_of_path path})
   218 fun tell_file_retracted path = issue_pgip (Informfileretracted {url=PgipTypes.pgipurl_of_path path})
   219 
   220 
   221 
   222 (** theory / proof state output **)
   223 
   224 local
   225 
   226 fun statedisplay prts =
   227     let 
   228         val display = Pretty.output (Pretty.chunks prts)
   229         (* TODO: add extra PGML markup for allow proof state navigation *)
   230         val statedisplay = XML.Elem("statedisplay",[], [XML.Rawtext display])
   231     in
   232         issue_pgip (Proofstate {pgml=[XML.Elem("pgml",[],[statedisplay])]})
   233     end
   234 
   235 fun print_current_goals n m st =
   236   case (Display.pretty_current_goals n m st) of 
   237    [] => tell_clear_goals()
   238  | prts => statedisplay prts
   239 
   240 fun print_state b st =
   241   case (Toplevel.pretty_state b st) of 
   242    [] => tell_clear_goals() 
   243   | prts => statedisplay prts
   244 
   245 in
   246 
   247 fun setup_state () =
   248   (Display.print_current_goals_fn := print_current_goals;
   249    Toplevel.print_state_fn := print_state);
   250 
   251 end;
   252 
   253 
   254 (* theory loader actions *)
   255 
   256 local
   257 
   258 fun trace_action action name =
   259   if action = ThyInfo.Update then
   260     List.app tell_file_loaded (ThyInfo.loaded_files name)
   261   else if action = ThyInfo.Outdate orelse action = ThyInfo.Remove then
   262     List.app tell_file_retracted (ThyInfo.loaded_files name)
   263   else ();
   264 
   265 in
   266   fun setup_thy_loader () = ThyInfo.add_hook trace_action;
   267   fun sync_thy_loader () = List.app (trace_action ThyInfo.Update) (ThyInfo.names ());
   268 end;
   269 
   270 
   271 (* get informed about files *)
   272 
   273 val thy_name = Path.implode o #1 o Path.split_ext o Path.base o Path.explode;
   274 
   275 val inform_file_retracted = ThyInfo.if_known_thy ThyInfo.remove_thy o thy_name;
   276 val inform_file_processed = ThyInfo.if_known_thy ThyInfo.touch_child_thys o thy_name;
   277 
   278 fun proper_inform_file_processed file state =
   279   let val name = thy_name file in
   280     if Toplevel.is_toplevel state andalso ThyInfo.known_thy name then
   281      (ThyInfo.touch_child_thys name;
   282       ThyInfo.pretend_use_thy_only name handle ERROR msg =>
   283        (warning msg; warning ("Failed to register theory: " ^ quote name);
   284         tell_file_retracted (Path.base (Path.explode file))))
   285     else raise Toplevel.UNDEF
   286   end;
   287 
   288 
   289 (* restart top-level loop (keeps most state information) *)
   290 
   291 val welcome = priority o Session.welcome;
   292 
   293 fun restart () =
   294     (sync_thy_loader ();
   295      tell_clear_goals ();
   296      tell_clear_response ();
   297      welcome ();
   298      raise Toplevel.RESTART)
   299 
   300 
   301 (* theorem dependency output *)
   302 local
   303 
   304 val spaces_quote = space_implode " " o map quote;
   305 
   306 fun thm_deps_message (thms, deps) =
   307     let
   308         val valuethms = XML.Elem("value",[("name", "thms")],[XML.Text thms])
   309         val valuedeps = XML.Elem("value",[("name", "deps")],[XML.Text deps])
   310     in
   311         issue_pgip (Metainforesponse {attrs=[("infotype", "isabelle_theorem_dependencies")],
   312                                       content=[valuethms,valuedeps]})
   313     end
   314 
   315 (* FIXME: check this uses non-transitive closure function here *)
   316 fun tell_thm_deps ths =
   317   if Output.has_mode thm_depsN then
   318     let
   319       val names = filter_out (equal "") (map PureThy.get_name_hint ths);
   320       val deps = filter_out (equal "")
   321         (Symtab.keys (fold Proofterm.thms_of_proof
   322           (map Thm.proof_of ths) Symtab.empty));
   323     in
   324       if null names orelse null deps then ()
   325       else thm_deps_message (spaces_quote names, spaces_quote deps)
   326     end
   327   else ();
   328 
   329 in
   330 
   331 fun setup_present_hook () =
   332   Present.add_hook (fn _ => fn res => tell_thm_deps (maps #2 res));
   333 
   334 end;
   335 
   336 (** lexicalstructure element with keywords (PGIP version of elisp keywords file) **)
   337 
   338 fun lexicalstructure_keywords () =
   339     let val commands = OuterSyntax.dest_keywords ()
   340         fun category_of k = if k mem commands then "major" else "minor"
   341          (* NB: we might filter to only include words like elisp case (OuterSyntax.is_keyword). *)
   342         fun keyword_elt (keyword,help,kind,_) =
   343             XML.Elem("keyword", [("word", keyword), ("category", category_of kind)],
   344                      [XML.Elem("shorthelp", [], [XML.Text help])])
   345         in
   346             (* Also, note we don't call init_outer_syntax here to add interface commands,
   347             but they should never appear in scripts anyway so it shouldn't matter *)
   348             Lexicalstructure {content = map keyword_elt (OuterSyntax.dest_parsers()) }
   349         end
   350 
   351 (* TODO: we can issue a lexicalstructure/keyword when the syntax gets extended dynamically;
   352    hooks needed in outer_syntax.ML to do that. *)
   353 
   354 
   355 (* Configuration: GUI config, proverinfo messages *)
   356 
   357 local
   358     val isabellewww = "http://isabelle.in.tum.de/"
   359     val staticconfig = "~~/lib/ProofGeneral/pgip_isar.xml"
   360     fun orenv v d = case getenv v of "" => d  | s => s
   361     fun config_file()  = orenv "ISABELLE_PGIPCONFIG" staticconfig
   362     fun isabelle_www() = orenv "ISABELLE_HOMEPAGE" isabellewww
   363 in
   364 fun send_pgip_config () =
   365     let
   366         val path = Path.explode (config_file())
   367         val ex = File.exists path
   368 
   369         val wwwpage =
   370             (Url.explode (isabelle_www()))
   371             handle ERROR _ =>
   372                    (Output.panic
   373                         ("Error in URL in environment variable ISABELLE_HOMEPAGE.");
   374                         Url.explode isabellewww)
   375 
   376         val proverinfo =
   377             Proverinfo { name = "Isabelle",
   378                          version = version,
   379                          instance = Session.name(),
   380                          descr = "The Isabelle/Isar theorem prover",
   381                          url = wwwpage,
   382                          filenameextns = ".thy;" }
   383     in
   384         if ex then
   385             (issue_pgip proverinfo;
   386              issue_pgip_rawtext (File.read path);
   387              issue_pgip (lexicalstructure_keywords()))
   388         else Output.panic ("PGIP configuration file \"" ^ config_file() ^ "\" not found")
   389     end;
   390 end
   391 
   392 
   393 
   394 
   395 (* Sending commands to Isar *)
   396 
   397 fun isarcmd s =
   398     s |> OuterSyntax.scan |> OuterSyntax.read
   399       (*|> map (Toplevel.position (Position.name "PGIP message") o #3)*)
   400       |> map #3
   401       |> Toplevel.>>>;
   402 
   403 (* TODO:
   404     - apply a command given a transition function, e.g. IsarCmd.undo.
   405     - fix position from path of currently open file [line numbers risk garbling though].
   406 *)
   407 
   408 (* load an arbitrary file (must be .thy or .ML) *)
   409 
   410 fun use_thy_or_ml_file file =
   411     let
   412         val (path,extn) = Path.split_ext (Path.explode file)
   413     in
   414         case extn of
   415             "" => isarcmd ("use_thy " ^ quote (Path.implode path))
   416           | "thy" => isarcmd ("use_thy " ^ quote (Path.implode path))
   417           | "ML" => isarcmd ("use " ^ quote file)
   418           | other => error ("Don't know how to read a file with extension " ^ quote other)
   419     end
   420 
   421 
   422 (******* PGIP actions *******)
   423 
   424 
   425 (* Responses to each of the PGIP input commands.
   426    These are programmed uniformly for extensibility. *)
   427 
   428 fun askpgip (Askpgip vs) =
   429     issue_pgip
   430         (Usespgip { version = PgipIsabelle.isabelle_pgip_version_supported,
   431                     pgipelems = PgipIsabelle.accepted_inputs })
   432 
   433 fun askpgml (Askpgml vs) =
   434     issue_pgip
   435         (Usespgml { version = PgipIsabelle.isabelle_pgml_version_supported })
   436 
   437 fun askprefs (Askprefs vs) =
   438     let
   439         fun preference_of {name, descr, default, pgiptype, get, set } =
   440             { name = name, descr = SOME descr, default = SOME default,
   441               pgiptype = pgiptype }
   442     in
   443         List.app (fn (prefcat, prefs) =>
   444                      issue_pgip (Hasprefs {prefcategory=SOME prefcat,
   445                                            prefs=map preference_of prefs}))
   446                  Preferences.preferences
   447     end
   448 
   449 fun askconfig (Askconfig vs) = () (* TODO: add config response *)
   450 
   451 local
   452     fun lookuppref pref =
   453         case AList.lookup (op =)
   454                           (map (fn p => (#name p,p))
   455                                (maps snd Preferences.preferences)) pref of
   456             NONE => error ("Unknown prover preference: " ^ quote pref)
   457           | SOME p => p
   458 in
   459 fun setpref (Setpref vs) =
   460     let
   461         val name = #name vs
   462         val value = #value vs
   463         val set = #set (lookuppref name)
   464     in
   465         set value
   466     end
   467 
   468 fun getpref (Getpref vs) =
   469     let
   470         val name = #name vs
   471         val get = #get (lookuppref name)
   472     in
   473         issue_pgip (Prefval {name=name, value=get ()})
   474     end
   475 end
   476 
   477 fun proverinit vs = restart ()
   478 
   479 fun proverexit vs = isarcmd "quit"
   480 
   481 fun startquiet vs = isarcmd "disable_pr"
   482 
   483 fun stopquiet vs = isarcmd "enable_pr"
   484 
   485 fun pgmlsymbolson vs =
   486     change print_mode (fn mode =>
   487                           remove (op =) Symbol.xsymbolsN mode @ [Symbol.xsymbolsN])
   488 
   489 fun pgmlsymbolsoff vs =
   490     change print_mode (remove (op =) Symbol.xsymbolsN)
   491 
   492 fun dostep (Dostep vs) =
   493     let
   494         val text = #text vs
   495     in
   496         isarcmd text
   497     end
   498 
   499 fun undostep (Undostep vs) =
   500     let
   501         val times = #times vs
   502     in
   503         isarcmd ("undos_proof " ^ Int.toString times)
   504     end
   505 
   506 fun redostep vs = isarcmd "redo"
   507 
   508 fun abortgoal vs = isarcmd "kill" (* was: ProofGeneral.kill_proof *)
   509 
   510 
   511 (*** PGIP identifier tables ***)
   512 
   513 fun setids t = issue_pgip (Setids {idtables = [t]})
   514 fun addids t = issue_pgip (Addids {idtables = [t]})
   515 fun delids t = issue_pgip (Delids {idtables = [t]})
   516 
   517 (*
   518  fun delallids ty =
   519      issue_pgip (Setids {idtables =
   520                         [{context=NONE,objtype=ty,ids=[]}]}) *)
   521 
   522 fun askids (Askids vs) =
   523     let
   524         val url = #url vs            (* ask for identifiers within a file *)
   525         val thyname = #thyname vs    (* ask for identifiers within a theory *)
   526         val objtype = #objtype vs    (* ask for identifiers of a particular type *)
   527 
   528         fun idtable ty ctx ids = {objtype=ty,context=ctx,ids=ids}
   529 
   530         val thms_of_thy = map fst o PureThy.thms_of o ThyInfo.get_theory
   531     in
   532 (*      case (url_attr,thyname,objtype) of
   533             (NONE,NONE,NONE) =>
   534 *)          (* top-level: return *)
   535 
   536         (* TODO: add askids for "file" here, which returns single theory with same name *)
   537         (* FIXME: objtypes on both sides *)
   538         case (thyname,objtype) of
   539            (* only files known in top context *)
   540            (NONE, NONE)               => setids (idtable ObjFile NONE (ThyInfo.names())) (*FIXME: uris?*)
   541          | (NONE, SOME ObjFile)        => setids (idtable ObjFile NONE (ThyInfo.names())) (* ditto *)
   542          | (SOME fi, SOME ObjFile)     => setids (idtable ObjTheory (SOME fi) [fi]) (* FIXME: lookup file *)
   543          | (NONE, SOME ObjTheory)      => setids (idtable ObjTheory NONE (ThyInfo.names()))
   544          | (SOME thy, SOME ObjTheory)  => setids (idtable ObjTheory (SOME thy) (ThyInfo.get_preds thy))
   545          | (SOME thy, SOME ObjTheorem) => setids (idtable ObjTheorem (SOME thy) (thms_of_thy thy))
   546          (* next case is both of above.  FIXME: cleanup this *)
   547          | (SOME thy, NONE) => (setids (idtable ObjTheory (SOME thy) (ThyInfo.get_preds thy));
   548                                 setids (idtable ObjTheorem (SOME thy) (thms_of_thy thy)))
   549          | (_, SOME ot) => error ("No objects of type "^(PgipTypes.name_of_objtype ot)^" are available here.")
   550     end
   551 
   552 local
   553   (* accumulate printed output in a single PGIP response (inside <pgmltext>) *)
   554   fun with_displaywrap pgipfn dispfn =
   555       let
   556           val lines = ref ([]: string list);
   557           fun wlgrablines s = lines := s :: ! lines;
   558       in
   559           setmp writeln_fn wlgrablines dispfn ();
   560           issue_pgip (pgipfn (!lines))
   561       end;
   562 in
   563 fun showid (Showid vs) =
   564     let
   565         val thyname = #thyname vs
   566         val objtype = #objtype vs
   567         val name = #name vs
   568         val topthy = Toplevel.theory_of o Toplevel.get_state
   569 
   570         fun idvalue objtype name strings =
   571             Idvalue { name=name, objtype=objtype,
   572                       text=[XML.Elem("pgmltext",[],map XML.Text strings)] }
   573 
   574         fun pthm thy name = print_thm (get_thm thy (Name name))
   575     in
   576         case (thyname, objtype) of
   577             (_,ObjTheory) =>
   578             with_displaywrap (idvalue ObjTheory name)
   579                              (fn ()=>(print_theory (ThyInfo.get_theory name)))
   580           | (SOME thy, ObjTheorem) =>
   581             with_displaywrap (idvalue ObjTheorem name)
   582                              (fn ()=>(pthm (ThyInfo.get_theory thy) name))
   583           | (NONE, ObjTheorem) =>
   584             with_displaywrap (idvalue ObjTheorem name)
   585                              (fn ()=>pthm (topthy()) name)
   586           | (_, ot) => error ("Cannot show objects of type "^(PgipTypes.name_of_objtype ot))
   587     end
   588 
   589 (*** Inspecting state ***)
   590 
   591 (* The file which is currently being processed interactively.
   592    In the pre-PGIP code, this was informed to Isabelle and the theory loader
   593    on completion, but that allows for circularity in case we read
   594    ourselves.  So PGIP opens the filename at the start of a script.
   595    We ought to prevent problems by modifying the theory loader to know
   596    about this special status, but for now we just keep a local reference.
   597 *)
   598 
   599 val currently_open_file = ref (NONE : pgipurl option)
   600 
   601 fun askguise vs =
   602     (* The "guise" is the PGIP abstraction of the prover's state.
   603        The <informguise> message is merely used for consistency checking. *)
   604     let
   605         val openfile = !currently_open_file
   606 
   607         val topthy = Toplevel.theory_of o Toplevel.get_state
   608         val topthy_name = Context.theory_name o topthy
   609 
   610         val opentheory = SOME (topthy_name()) handle Toplevel.UNDEF => NONE
   611 
   612         fun topproofpos () = try Toplevel.proof_position_of (Isar.state ());
   613         val openproofpos = topproofpos()
   614     in
   615         issue_pgip (Informguise { file = openfile,
   616                                   theory = opentheory,
   617                                   (* would be nice to get thm name... *)
   618                                   theorem = NONE,
   619                                   proofpos = openproofpos })
   620     end
   621 
   622 fun parsescript (Parsescript vs) =
   623     let
   624         val text = #text vs
   625         val systemdata = #systemdata vs
   626         val location = #location vs   (* TODO: extract position *)
   627 
   628         val _ = start_delay_msgs ()   (* gather parsing errs/warns *)
   629         val doc = PgipParser.pgip_parser text
   630         val errs = end_delayed_msgs ()
   631 
   632         val sysattrs = PgipTypes.opt_attr "systemdata" systemdata
   633         val locattrs = PgipTypes.attrs_of_location location
   634      in
   635         issue_pgip (Parseresult { attrs= sysattrs@locattrs,
   636                                   doc = doc,
   637                                   errs = map PgipOutput.output errs })
   638     end
   639 
   640 fun showproofstate vs = isarcmd "pr"
   641 
   642 fun showctxt vs = isarcmd "print_context"
   643 
   644 fun searchtheorems (Searchtheorems vs) =
   645     let
   646         val arg = #arg vs
   647     in
   648         isarcmd ("find_theorems " ^ arg)
   649     end
   650 
   651 fun setlinewidth (Setlinewidth vs) =
   652     let
   653         val width = #width vs
   654     in
   655         isarcmd ("pretty_setmargin " ^ Int.toString width) (* FIXME: conversion back/forth! *)
   656     end
   657 
   658 fun viewdoc (Viewdoc vs) =
   659     let
   660         val arg = #arg vs
   661     in
   662         isarcmd ("print_" ^ arg)   (* FIXME: isatool doc?.  Return URLs, maybe? *)
   663     end
   664 
   665 (*** Theory ***)
   666 
   667 fun doitem (Doitem vs) =
   668     let
   669         val text = #text vs
   670     in
   671         isarcmd text
   672     end
   673 
   674 fun undoitem vs =
   675     isarcmd "undo"
   676 
   677 fun redoitem vs =
   678     isarcmd "redo"
   679 
   680 fun aborttheory vs =
   681     isarcmd "kill"  (* was: "init_toplevel" *)
   682 
   683 fun retracttheory (Retracttheory vs) =
   684     let
   685         val thyname = #thyname vs
   686     in
   687         isarcmd ("kill_thy " ^ quote thyname)
   688     end
   689 
   690 
   691 (*** Files ***)
   692 
   693 (* Path management: we allow theory files to have dependencies in
   694    their own directory, but when we change directory for a new file we
   695    remove the path.  Leaving it there can cause confusion with
   696    difference in batch mode.
   697    NB: PGIP does not assume that the prover has a load path.
   698 *)
   699 
   700 local
   701     val current_working_dir = ref (NONE : string option)
   702 in
   703 fun changecwd_dir newdirpath =
   704    let
   705        val newdir = File.platform_path newdirpath
   706    in
   707        (case (!current_working_dir) of
   708             NONE => ()
   709           | SOME dir => ThyLoad.del_path dir;
   710         ThyLoad.add_path newdir;
   711         current_working_dir := SOME newdir)
   712    end
   713 end
   714 
   715 fun changecwd (Changecwd vs) =
   716     let
   717         val url = #url vs
   718         val newdir = PgipTypes.path_of_pgipurl url
   719     in
   720         changecwd_dir url
   721     end
   722 
   723 fun openfile (Openfile vs) =
   724   let
   725       val url = #url vs
   726       val filepath = PgipTypes.path_of_pgipurl url
   727       val filedir = Path.dir filepath
   728       val thy_name = Path.implode o #1 o Path.split_ext o Path.base
   729       val openfile_retract = Output.no_warnings (ThyInfo.if_known_thy ThyInfo.remove_thy) o thy_name;
   730   in
   731       case !currently_open_file of
   732           SOME f => raise PGIP ("<openfile> when a file is already open!\nCurrently open file: " ^
   733 				PgipTypes.string_of_pgipurl url)
   734         | NONE => (openfile_retract filepath;
   735                    changecwd_dir filedir;
   736 		   priority ("Working in file: " ^ PgipTypes.string_of_pgipurl url);
   737                    currently_open_file := SOME url)
   738   end
   739 
   740 fun closefile vs =
   741     case !currently_open_file of
   742         SOME f => (proper_inform_file_processed (File.platform_path f)
   743                                                 (Isar.state());
   744 		   priority ("Finished working in file: " ^ PgipTypes.string_of_pgipurl f);
   745                    currently_open_file := NONE)
   746       | NONE => raise PGIP ("<closefile> when no file is open!")
   747 
   748 fun loadfile (Loadfile vs) =
   749     let
   750         val url = #url vs
   751     in
   752         case !currently_open_file of
   753             SOME f => raise PGIP ("<loadfile> when a file is open!\nCurrently open file: " ^
   754 				  PgipTypes.string_of_pgipurl url)
   755           | NONE => use_thy_or_ml_file (File.platform_path url)
   756     end
   757 
   758 fun abortfile vs =
   759     case !currently_open_file of
   760         SOME f => (isarcmd "init_toplevel";
   761 		   priority ("Aborted working in file: " ^ 
   762 			     PgipTypes.string_of_pgipurl f);
   763                    currently_open_file := NONE)
   764       | NONE => raise PGIP ("<abortfile> when no file is open!")
   765 
   766 fun retractfile (Retractfile vs) =
   767     let
   768         val url = #url vs
   769     in
   770         case !currently_open_file of
   771             SOME f => raise PGIP ("<retractfile> when a file is open!")
   772           | NONE => (priority ("Retracting file: " ^ PgipTypes.string_of_pgipurl url);
   773 		     inform_file_retracted (File.platform_path url))
   774     end
   775 
   776 
   777 (*** System ***)
   778 
   779 fun systemcmd (Systemcmd vs) =
   780   let
   781       val arg = #arg vs
   782   in
   783       isarcmd arg
   784   end
   785 
   786 exception PGIP_QUIT;
   787 fun quitpgip vs = raise PGIP_QUIT
   788 
   789 fun process_input inp = case inp
   790  of Pgip.Askpgip _          => askpgip inp
   791   | Pgip.Askpgml _          => askpgml inp
   792   | Pgip.Askprefs _         => askprefs inp
   793   | Pgip.Askconfig _        => askconfig inp
   794   | Pgip.Getpref _          => getpref inp
   795   | Pgip.Setpref _          => setpref inp
   796   | Pgip.Proverinit _       => proverinit inp
   797   | Pgip.Proverexit _       => proverexit inp
   798   | Pgip.Startquiet _       => startquiet inp
   799   | Pgip.Stopquiet _        => stopquiet inp
   800   | Pgip.Pgmlsymbolson _    => pgmlsymbolson inp
   801   | Pgip.Pgmlsymbolsoff _   => pgmlsymbolsoff inp
   802   | Pgip.Dostep _           => dostep inp
   803   | Pgip.Undostep _         => undostep inp
   804   | Pgip.Redostep _         => redostep inp
   805   | Pgip.Forget _           => error "<forget> not implemented"
   806   | Pgip.Restoregoal _      => error "<restoregoal> not implemented"
   807   | Pgip.Abortgoal _        => abortgoal inp
   808   | Pgip.Askids _           => askids inp
   809   | Pgip.Showid _           => showid inp
   810   | Pgip.Askguise _         => askguise inp
   811   | Pgip.Parsescript _      => parsescript inp
   812   | Pgip.Showproofstate _   => showproofstate inp
   813   | Pgip.Showctxt _         => showctxt inp
   814   | Pgip.Searchtheorems _   => searchtheorems inp
   815   | Pgip.Setlinewidth _     => setlinewidth inp
   816   | Pgip.Viewdoc _          => viewdoc inp
   817   | Pgip.Doitem _           => doitem inp
   818   | Pgip.Undoitem _         => undoitem inp
   819   | Pgip.Redoitem _         => redoitem inp
   820   | Pgip.Aborttheory _      => aborttheory inp
   821   | Pgip.Retracttheory _    => retracttheory inp
   822   | Pgip.Loadfile _         => loadfile inp
   823   | Pgip.Openfile _         => openfile inp
   824   | Pgip.Closefile _        => closefile inp
   825   | Pgip.Abortfile _        => abortfile inp
   826   | Pgip.Retractfile _      => retractfile inp
   827   | Pgip.Changecwd _        => changecwd inp
   828   | Pgip.Systemcmd _        => systemcmd inp
   829   | Pgip.Quitpgip _         => quitpgip inp
   830 
   831 
   832 fun process_pgip_element pgipxml =
   833     case pgipxml of
   834         xml as (XML.Elem elem) =>
   835         (case Pgip.input elem of
   836              NONE => warning ("Unrecognized PGIP command, ignored: \n" ^
   837                               (XML.string_of_tree xml))
   838            | SOME inp => (process_input inp)) (* errors later; packet discarded *)
   839       | XML.Text t => ignored_text_warning t
   840       | XML.Rawtext t => ignored_text_warning t
   841 and ignored_text_warning t =
   842     if size (Symbol.strip_blanks t) > 0 then
   843            warning ("Ignored text in PGIP packet: \n" ^ t)
   844     else ()
   845 
   846 fun process_pgip_tree xml =
   847     (pgip_refid := NONE;
   848      pgip_refseq := NONE;
   849      (case xml of
   850           XML.Elem ("pgip", attrs, pgips) =>
   851           (let
   852                val class = PgipTypes.get_attr "class" attrs
   853                val dest  = PgipTypes.get_attr_opt "destid" attrs
   854                val seq = PgipTypes.read_pgipnat (PgipTypes.get_attr "seq" attrs)
   855                (* Respond to prover broadcasts, or messages for us. Ignore rest *)
   856                val processit =
   857                    case dest of
   858                        NONE =>    class = "pa"
   859                      | SOME id => matching_pgip_id id
   860            in if processit then
   861                   (pgip_refid :=  PgipTypes.get_attr_opt "id" attrs;
   862                    pgip_refseq := SOME seq;
   863                    List.app process_pgip_element pgips;
   864                    (* return true to indicate <ready/> *)
   865                    true)
   866               else
   867                   (* no response to ignored messages. *)
   868                   false
   869            end)
   870         | _ => raise PGIP "Invalid PGIP packet received")
   871      handle PGIP msg =>
   872             (Output.error_msg ((msg ^ "\nPGIP error occured in XML text below:\n") ^
   873                                (XML.string_of_tree xml));
   874              true))
   875 
   876 (* External input *)
   877 
   878 val process_pgip_plain = K () o process_pgip_tree o XML.tree_of_string
   879 
   880 end
   881 
   882 
   883 (* PGIP loop: process PGIP input only *)
   884 
   885 local
   886 
   887 exception XML_PARSE
   888 
   889 fun loop ready src =
   890     let
   891         val _ = if ready then issue_pgip (Ready ()) else ()
   892         val pgipo =
   893           (case try Source.get_single src of
   894             SOME pgipo => pgipo
   895           | NONE => raise XML_PARSE)
   896     in
   897         case pgipo of
   898              NONE  => ()
   899            | SOME (pgip,src') =>
   900              let
   901                  val ready' = (process_pgip_tree pgip)
   902                                 handle e => (handler (e,SOME src'); true)
   903              in
   904                  loop ready' src'
   905              end
   906     end handle e => handler (e,SOME src)  (* error in XML parse or Ready issue *)
   907 
   908 and handler (e,srco) =
   909     case (e,srco) of
   910         (XML_PARSE,SOME src) =>
   911         Output.panic "Invalid XML input, aborting"
   912       | (PGIP_QUIT,_) => ()
   913       | (Interrupt,SOME src) =>
   914         (Output.error_msg "Interrupt during PGIP processing"; loop true src)
   915       | (Toplevel.UNDEF,SOME src) =>
   916         (Output.error_msg "No working context defined"; loop true src)
   917       | (e,SOME src) =>
   918         (Output.error_msg (Toplevel.exn_message e); loop true src)
   919       | (_,NONE) => ()
   920 in
   921   (* TODO: add socket interface *)
   922 
   923   val xmlP = XML.scan_comment_whspc |-- XML.parse_elem >> single
   924 
   925   val tty_src = Source.set_prompt "" (Source.source Symbol.stopper xmlP NONE Source.tty)
   926 
   927   fun pgip_toplevel x = loop true x
   928 end
   929 
   930 
   931 local
   932 (* Extra command for embedding prover-control inside document (obscure/debug usage). *)
   933 
   934 val process_pgipP =
   935   OuterSyntax.improper_command "ProofGeneral.process_pgip" "(internal)" OuterKeyword.control
   936     (OuterParse.text >> (Toplevel.no_timing oo
   937       (fn txt => Toplevel.imperative (fn () => process_pgip_plain txt))));
   938 
   939 in
   940 
   941  fun init_outer_syntax () = OuterSyntax.add_parsers [process_pgipP];
   942 
   943 end
   944 
   945 
   946 
   947 (* init *)
   948 
   949 val initialized = ref false;
   950 
   951 fun init_pgip false =
   952       Output.panic "No Proof General interface support for Isabelle/classic mode."
   953   | init_pgip true =
   954       (! initialized orelse
   955         (setmp warning_fn (K ()) init_outer_syntax ();
   956           PgipParser.init ();
   957           setup_xsymbols_output ();
   958           setup_pgml_output ();
   959           setup_messages ();
   960           setup_state ();
   961           setup_thy_loader ();
   962           setup_present_hook ();
   963           init_pgip_session_id ();
   964           welcome ();
   965           set initialized);
   966         sync_thy_loader ();
   967        change print_mode (cons proof_generalN o remove (op =) proof_generalN);
   968        change print_mode (append [pgmlN, pgmlatomsN] o subtract (op =) [pgmlN, pgmlatomsN]);
   969        pgip_toplevel tty_src);
   970 
   971 
   972 
   973 (** Out-of-loop PGIP commands (for Emacs hybrid mode) **)
   974 
   975 local
   976     val pgip_output_channel = ref writeln_default
   977 in
   978 
   979 (* Set recipient for PGIP results *)
   980 fun init_pgip_channel writefn =
   981     (init_pgip_session_id();
   982      pgip_output_channel := writefn)
   983 
   984 (* Process a PGIP command.
   985    This works for preferences but not generally guaranteed
   986    because we haven't done full setup here (e.g., no pgml mode)  *)
   987 fun process_pgip str =
   988      setmp output_xml_fn (!pgip_output_channel) process_pgip_plain str
   989 
   990 end
   991 
   992 end;
   993