src/Pure/ProofGeneral/proof_general_pgip.ML
author wenzelm
Sat Dec 30 16:20:32 2006 +0100 (2006-12-30)
changeset 21970 1845e43aee93
parent 21969 a8bf1106cb7c
child 21972 1b68312c4cf0
permissions -rw-r--r--
removed 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 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 Nonfatal s);
   209   error_fn := (fn s => errormsg Fatal s);
   210   panic_fn := (fn s => errormsg Panic s))
   211 
   212 (* immediate messages *)
   213 
   214 fun tell_clear_goals ()      = issue_pgip (Cleardisplay {area=Display})
   215 fun tell_clear_response ()   = issue_pgip (Cleardisplay {area=Message})
   216 fun tell_file_loaded path    = issue_pgip (Informfileloaded {url=PgipTypes.pgipurl_of_path path})
   217 fun tell_file_retracted path = issue_pgip (Informfileretracted {url=PgipTypes.pgipurl_of_path path})
   218 
   219 
   220 
   221 (** theory / proof state output **)
   222 
   223 local
   224 
   225 fun statedisplay prts =
   226     let
   227         val display = Pretty.output (Pretty.chunks prts)
   228         val statedisplay = XML.Elem("statedisplay",[], [XML.Rawtext display])
   229     in
   230         issue_pgip (Proofstate {pgml=[XML.Elem("pgml",[],[statedisplay])]})
   231     end
   232 
   233 fun print_current_goals n m st =
   234   statedisplay (Display.pretty_current_goals n m st)
   235 
   236 fun print_state b st =
   237   statedisplay (Toplevel.pretty_state b st)
   238 
   239 in
   240 
   241 fun setup_state () =
   242   (Display.print_current_goals_fn := print_current_goals;
   243    Toplevel.print_state_fn := print_state);
   244       (*    Toplevel.prompt_state_fn := (fn s => suffix (special "372")
   245                                         (Toplevel.prompt_state_default s))); *)
   246 
   247 end;
   248 
   249 
   250 (* theory loader actions *)
   251 
   252 local
   253 
   254 fun trace_action action name =
   255   if action = ThyInfo.Update then
   256     List.app tell_file_loaded (ThyInfo.loaded_files name)
   257   else if action = ThyInfo.Outdate orelse action = ThyInfo.Remove then
   258     List.app tell_file_retracted (ThyInfo.loaded_files name)
   259   else ();
   260 
   261 in
   262   fun setup_thy_loader () = ThyInfo.add_hook trace_action;
   263   fun sync_thy_loader () = List.app (trace_action ThyInfo.Update) (ThyInfo.names ());
   264 end;
   265 
   266 
   267 (* get informed about files *)
   268 
   269 val thy_name = Path.implode o #1 o Path.split_ext o Path.base o Path.explode;
   270 
   271 val inform_file_retracted = ThyInfo.if_known_thy ThyInfo.remove_thy o thy_name;
   272 val inform_file_processed = ThyInfo.if_known_thy ThyInfo.touch_child_thys o thy_name;
   273 
   274 fun proper_inform_file_processed file state =
   275   let val name = thy_name file in
   276     if Toplevel.is_toplevel state andalso ThyInfo.known_thy name then
   277      (ThyInfo.touch_child_thys name;
   278       ThyInfo.pretend_use_thy_only name handle ERROR msg =>
   279        (warning msg; warning ("Failed to register theory: " ^ quote name);
   280         tell_file_retracted (Path.base (Path.explode file))))
   281     else raise Toplevel.UNDEF
   282   end;
   283 
   284 fun vacuous_inform_file_processed file state =
   285  (warning ("No theory " ^ quote (thy_name file));
   286   tell_file_retracted (Path.base (Path.explode file)));
   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      priority "Running new version of PGIP code.  In testing.";
   299      raise Toplevel.RESTART)
   300 
   301 
   302 (* theorem dependency output *)
   303 local
   304 
   305 val spaces_quote = space_implode " " o map quote;
   306 
   307 fun thm_deps_message (thms, deps) =
   308     let
   309         val valuethms = XML.Elem("value",[("name", "thms")],[XML.Text thms])
   310         val valuedeps = XML.Elem("value",[("name", "deps")],[XML.Text deps])
   311     in
   312         issue_pgip (Metainforesponse {attrs=[("infotype", "isabelle_theorem_dependencies")],
   313                                       content=[valuethms,valuedeps]})
   314     end
   315 
   316 (* FIXME: check this uses non-transitive closure function here *)
   317 fun tell_thm_deps ths =
   318   if Output.has_mode thm_depsN then
   319     let
   320       val names = filter_out (equal "") (map PureThy.get_name_hint ths);
   321       val deps = filter_out (equal "")
   322         (Symtab.keys (fold Proofterm.thms_of_proof
   323           (map Thm.proof_of ths) Symtab.empty));
   324     in
   325       if null names orelse null deps then ()
   326       else thm_deps_message (spaces_quote names, spaces_quote deps)
   327     end
   328   else ();
   329 
   330 in
   331 
   332 fun setup_present_hook () =
   333   Present.add_hook (fn _ => fn res => tell_thm_deps (maps #2 res));
   334 
   335 end;
   336 
   337 (** lexicalstructure element with keywords (PGIP version of elisp keywords file) **)
   338 
   339 fun lexicalstructure_keywords () =
   340     let val commands = OuterSyntax.dest_keywords ()
   341         fun category_of k = if k mem commands then "major" else "minor"
   342          (* NB: we might filter to only include words like elisp case (OuterSyntax.is_keyword). *)
   343         fun keyword_elt (keyword,help,kind,_) =
   344             XML.Elem("keyword", [("word", keyword), ("category", category_of kind)],
   345                      [XML.Elem("shorthelp", [], [XML.Text help])])
   346         in
   347             (* Also, note we don't call init_outer_syntax here to add interface commands,
   348             but they should never appear in scripts anyway so it shouldn't matter *)
   349             Lexicalstructure {content = map keyword_elt (OuterSyntax.dest_parsers()) }
   350         end
   351 
   352 (* TODO: we can issue a lexicalstructure/keyword when the syntax gets extended dynamically;
   353    hooks needed in outer_syntax.ML to do that. *)
   354 
   355 
   356 (* Configuration: GUI config, proverinfo messages *)
   357 
   358 local
   359     val isabellewww = "http://isabelle.in.tum.de/"
   360     val staticconfig = "~~/lib/ProofGeneral/pgip_isar.xml"
   361     fun orenv v d = case getenv v of "" => d  | s => s
   362     fun config_file()  = orenv "ISABELLE_PGIPCONFIG" staticconfig
   363     fun isabelle_www() = orenv "ISABELLE_HOMEPAGE" isabellewww
   364 in
   365 fun send_pgip_config () =
   366     let
   367         val path = Path.explode (config_file())
   368         val ex = File.exists path
   369 
   370         val wwwpage =
   371             (Url.explode (isabelle_www()))
   372             handle ERROR _ =>
   373                    (Output.panic
   374                         ("Error in URL in environment variable ISABELLE_HOMEPAGE.");
   375                         Url.explode isabellewww)
   376 
   377         val proverinfo =
   378             Proverinfo { name = "Isabelle",
   379                          version = version,
   380                          instance = Session.name(),
   381                          descr = "The Isabelle/Isar theorem prover",
   382                          url = wwwpage,
   383                          filenameextns = ".thy;" }
   384     in
   385         if ex then
   386             (issue_pgip proverinfo;
   387              issue_pgip_rawtext (File.read path);
   388              issue_pgip (lexicalstructure_keywords()))
   389         else Output.panic ("PGIP configuration file \"" ^ config_file() ^ "\" not found")
   390     end;
   391 end
   392 
   393 
   394 
   395 
   396 (* Sending commands to Isar *)
   397 
   398 fun isarcmd s =
   399     s |> OuterSyntax.scan |> OuterSyntax.read
   400       (*|> map (Toplevel.position (Position.name "PGIP message") o #3)*)
   401       |> map #3
   402       |> Toplevel.>>>;
   403 
   404 (* TODO:
   405     - apply a command given a transition function, e.g. IsarCmd.undo.
   406     - fix position from path of currently open file [line numbers risk garbling though].
   407 *)
   408 
   409 (* load an arbitrary file (must be .thy or .ML) *)
   410 
   411 fun use_thy_or_ml_file file =
   412     let
   413         val (path,extn) = Path.split_ext (Path.explode file)
   414     in
   415         case extn of
   416             "" => isarcmd ("use_thy " ^ quote (Path.implode path))
   417           | "thy" => isarcmd ("use_thy " ^ quote (Path.implode path))
   418           | "ML" => isarcmd ("use " ^ quote file)
   419           | other => error ("Don't know how to read a file with extension " ^ other)
   420     end
   421 
   422 
   423 (******* PGIP actions *******)
   424 
   425 
   426 (* Responses to each of the PGIP input commands.
   427    These are programmed uniformly for extensibility. *)
   428 
   429 fun askpgip (Askpgip vs) =
   430     issue_pgip
   431         (Usespgip { version = PgipIsabelle.isabelle_pgip_version_supported,
   432                     pgipelems = PgipIsabelle.accepted_inputs })
   433 
   434 fun askpgml (Askpgml vs) =
   435     issue_pgip
   436         (Usespgml { version = PgipIsabelle.isabelle_pgml_version_supported })
   437 
   438 fun askprefs (Askprefs vs) =
   439     let
   440         fun preference_of {name, descr, default, pgiptype, get, set } =
   441             { name = name, descr = SOME descr, default = SOME default,
   442               pgiptype = pgiptype }
   443     in
   444         List.app (fn (prefcat, prefs) =>
   445                      issue_pgip (Hasprefs {prefcategory=SOME prefcat,
   446                                            prefs=map preference_of prefs}))
   447                  Preferences.preferences
   448     end
   449 
   450 fun askconfig (Askconfig vs) = () (* TODO: add config response *)
   451 
   452 local
   453     fun lookuppref pref =
   454         case AList.lookup (op =)
   455                           (map (fn p => (#name p,p))
   456                                (maps snd Preferences.preferences)) pref of
   457             NONE => error ("Unknown prover preference: " ^ quote pref)
   458           | SOME p => p
   459 in
   460 fun setpref (Setpref vs) =
   461     let
   462         val name = #name vs
   463         val value = #value vs
   464         val set = #set (lookuppref name)
   465     in
   466         set value
   467     end
   468 
   469 fun getpref (Getpref vs) =
   470     let
   471         val name = #name vs
   472         val get = #get (lookuppref name)
   473     in
   474         issue_pgip (Prefval {name=name, value=get ()})
   475     end
   476 end
   477 
   478 fun proverinit vs = restart ()
   479 
   480 fun proverexit vs = isarcmd "quit"
   481 
   482 fun startquiet vs = isarcmd "disable_pr"
   483 
   484 fun stopquiet vs = isarcmd "enable_pr"
   485 
   486 fun pgmlsymbolson vs =
   487     change print_mode (fn mode =>
   488                           remove (op =) Symbol.xsymbolsN mode @ [Symbol.xsymbolsN])
   489 
   490 fun pgmlsymbolsoff vs =
   491     change print_mode (remove (op =) Symbol.xsymbolsN)
   492 
   493 fun dostep (Dostep vs) =
   494     let
   495         val text = #text vs
   496     in
   497         isarcmd text
   498     end
   499 
   500 fun undostep (Undostep vs) =
   501     let
   502         val times = #times vs
   503     in
   504         isarcmd ("undos_proof " ^ Int.toString times)
   505     end
   506 
   507 fun redostep vs = isarcmd "redo"
   508 
   509 fun abortgoal vs = isarcmd "ProofGeneral.kill_proof"
   510 
   511 
   512 (*** PGIP identifier tables ***)
   513 
   514 fun setids t = issue_pgip (Setids {idtables = [t]})
   515 fun addids t = issue_pgip (Addids {idtables = [t]})
   516 fun delids t = issue_pgip (Delids {idtables = [t]})
   517 
   518 (*
   519  fun delallids ty =
   520      issue_pgip (Setids {idtables =
   521                         [{context=NONE,objtype=ty,ids=[]}]}) *)
   522 
   523 fun askids (Askids vs) =
   524     let
   525         val url = #url vs            (* ask for identifiers within a file *)
   526         val thyname = #thyname vs    (* ask for identifiers within a theory *)
   527         val objtype = #objtype vs    (* ask for identifiers of a particular type *)
   528 
   529         fun idtable ty ctx ids = {objtype=ty,context=ctx,ids=ids}
   530 
   531         val thms_of_thy = map fst o PureThy.thms_of o ThyInfo.get_theory
   532     in
   533 (*      case (url_attr,thyname,objtype) of
   534             (NONE,NONE,NONE) =>
   535 *)          (* top-level: return *)
   536 
   537         (* TODO: add askids for "file" here, which returns single theory with same name *)
   538         (* FIXME: objtypes on both sides *)
   539         case (thyname,objtype) of
   540            (* only files known in top context *)
   541            (NONE, NONE)               => setids (idtable ObjFile NONE (ThyInfo.names())) (*FIXME: uris?*)
   542          | (NONE, SOME ObjFile)        => setids (idtable ObjFile NONE (ThyInfo.names())) (* ditto *)
   543          | (SOME fi, SOME ObjFile)     => setids (idtable ObjTheory (SOME fi) [fi]) (* FIXME: lookup file *)
   544          | (NONE, SOME ObjTheory)      => setids (idtable ObjTheory NONE (ThyInfo.names()))
   545          | (SOME thy, SOME ObjTheory)  => setids (idtable ObjTheory (SOME thy) (ThyInfo.get_preds thy))
   546          | (SOME thy, SOME ObjTheorem) => setids (idtable ObjTheorem (SOME thy) (thms_of_thy thy))
   547          (* next case is both of above.  FIXME: cleanup this *)
   548          | (SOME thy, NONE) => (setids (idtable ObjTheory (SOME thy) (ThyInfo.get_preds thy));
   549                                 setids (idtable ObjTheorem (SOME thy) (thms_of_thy thy)))
   550          | (_, SOME ot) => error ("No objects of type "^(PgipTypes.name_of_objtype ot)^" are available here.")
   551     end
   552 
   553 local
   554   (* accumulate printed output in a single PGIP response (inside <pgmltext>) *)
   555   fun with_displaywrap pgipfn dispfn =
   556       let
   557           val lines = ref ([]: string list);
   558           fun wlgrablines s = lines := s :: ! lines;
   559       in
   560           setmp writeln_fn wlgrablines dispfn ();
   561           issue_pgip (pgipfn (!lines))
   562       end;
   563 in
   564 fun showid (Showid vs) =
   565     let
   566         val thyname = #thyname vs
   567         val objtype = #objtype vs
   568         val name = #name vs
   569         val topthy = Toplevel.theory_of o Toplevel.get_state
   570 
   571         fun idvalue objtype name strings =
   572             Idvalue { name=name, objtype=objtype,
   573                       text=[XML.Elem("pgmltext",[],map XML.Text strings)] }
   574 
   575         fun pthm thy name = print_thm (get_thm thy (Name name))
   576     in
   577         case (thyname, objtype) of
   578             (_,ObjTheory) =>
   579             with_displaywrap (idvalue ObjTheory name)
   580                              (fn ()=>(print_theory (ThyInfo.get_theory name)))
   581           | (SOME thy, ObjTheorem) =>
   582             with_displaywrap (idvalue ObjTheorem name)
   583                              (fn ()=>(pthm (ThyInfo.get_theory thy) name))
   584           | (NONE, ObjTheorem) =>
   585             with_displaywrap (idvalue ObjTheorem name)
   586                              (fn ()=>pthm (topthy()) name)
   587           | (_, ot) => error ("Cannot show objects of type "^(PgipTypes.name_of_objtype ot))
   588     end
   589 
   590 (*** Inspecting state ***)
   591 
   592 (* The file which is currently being processed interactively.
   593    In the pre-PGIP code, this was informed to Isabelle and the theory loader
   594    on completion, but that allows for circularity in case we read
   595    ourselves.  So PGIP opens the filename at the start of a script.
   596    We ought to prevent problems by modifying the theory loader to know
   597    about this special status, but for now we just keep a local reference.
   598 *)
   599 
   600 val currently_open_file = ref (NONE : pgipurl option)
   601 
   602 fun askguise vs =
   603     (* The "guise" is the PGIP abstraction of the prover's state.
   604        The <informguise> message is merely used for consistency checking. *)
   605     let
   606         val openfile = !currently_open_file
   607 
   608         val topthy = Toplevel.theory_of o Toplevel.get_state
   609         val topthy_name = Context.theory_name o topthy
   610 
   611         val opentheory = SOME (topthy_name()) handle Toplevel.UNDEF => NONE
   612 
   613         fun topproofpos () = try Toplevel.proof_position_of (Isar.state ());
   614         val openproofpos = topproofpos()
   615     in
   616         issue_pgip (Informguise { file = openfile,
   617                                   theory = opentheory,
   618                                   (* would be nice to get thm name... *)
   619                                   theorem = NONE,
   620                                   proofpos = openproofpos })
   621     end
   622 
   623 fun parsescript (Parsescript vs) =
   624     let
   625         val text = #text vs
   626         val systemdata = #systemdata vs
   627         val location = #location vs   (* TODO: extract position *)
   628 
   629         val _ = start_delay_msgs ()   (* gather parsing errs/warns *)
   630         val doc = PgipParser.pgip_parser text
   631         val errs = end_delayed_msgs ()
   632 
   633         val sysattrs = PgipTypes.opt_attr "systemdata" systemdata
   634         val locattrs = PgipTypes.attrs_of_location location
   635      in
   636         issue_pgip (Parseresult { attrs= sysattrs@locattrs,
   637                                   doc = doc,
   638                                   errs = map PgipOutput.output errs })
   639     end
   640 
   641 fun showproofstate vs = isarcmd "pr"
   642 
   643 fun showctxt vs = isarcmd "print_context"
   644 
   645 fun searchtheorems (Searchtheorems vs) =
   646     let
   647         val arg = #arg vs
   648     in
   649         isarcmd ("find_theorems " ^ arg)
   650     end
   651 
   652 fun setlinewidth (Setlinewidth vs) =
   653     let
   654         val width = #width vs
   655     in
   656         isarcmd ("pretty_setmargin " ^ Int.toString width) (* FIXME: conversion back/forth! *)
   657     end
   658 
   659 fun viewdoc (Viewdoc vs) =
   660     let
   661         val arg = #arg vs
   662     in
   663         isarcmd ("print_" ^ arg)   (* FIXME: isatool doc?.  Return URLs, maybe? *)
   664     end
   665 
   666 (*** Theory ***)
   667 
   668 fun doitem (Doitem vs) =
   669     let
   670         val text = #text vs
   671     in
   672         isarcmd text
   673     end
   674 
   675 fun undoitem vs =
   676     isarcmd "ProofGeneral.undo"
   677 
   678 fun redoitem vs =
   679     isarcmd "ProofGeneral.redo"
   680 
   681 fun aborttheory vs =
   682     isarcmd "init_toplevel"
   683 
   684 fun retracttheory (Retracttheory vs) =
   685     let
   686         val thyname = #thyname vs
   687     in
   688         isarcmd ("kill_thy " ^ quote thyname)
   689     end
   690 
   691 
   692 (*** Files ***)
   693 
   694 (* Path management: we allow theory files to have dependencies in
   695    their own directory, but when we change directory for a new file we
   696    remove the path.  Leaving it there can cause confusion with
   697    difference in batch mode.
   698    NB: PGIP does not assume that the prover has a load path.
   699 *)
   700 
   701 local
   702     val current_working_dir = ref (NONE : string option)
   703 in
   704 fun changecwd_dir newdirpath =
   705    let
   706        val newdir = File.platform_path newdirpath
   707    in
   708        (case (!current_working_dir) of
   709             NONE => ()
   710           | SOME dir => ThyLoad.del_path dir;
   711         ThyLoad.add_path newdir;
   712         current_working_dir := SOME newdir)
   713    end
   714 end
   715 
   716 fun changecwd (Changecwd vs) =
   717     let
   718         val url = #url vs
   719         val newdir = PgipTypes.path_of_pgipurl url
   720     in
   721         changecwd_dir url
   722     end
   723 
   724 fun openfile (Openfile vs) =
   725   let
   726       val url = #url vs
   727       val filepath = PgipTypes.path_of_pgipurl url
   728       val filedir = Path.dir filepath
   729       val thy_name = Path.implode o #1 o Path.split_ext o Path.base
   730       val openfile_retract = Output.no_warnings (ThyInfo.if_known_thy ThyInfo.remove_thy) o thy_name;
   731   in
   732       case !currently_open_file of
   733           SOME f => raise PGIP ("<openfile> when a file is already open! ")
   734         | NONE => (openfile_retract filepath;
   735                    changecwd_dir filedir;
   736                    currently_open_file := SOME url)
   737   end
   738 
   739 fun closefile vs =
   740     case !currently_open_file of
   741         SOME f => (proper_inform_file_processed (File.platform_path f)
   742                                                 (Isar.state());
   743                    currently_open_file := NONE)
   744       | NONE => raise PGIP ("<closefile> when no file is open!")
   745 
   746 fun loadfile (Loadfile vs) =
   747     let
   748         val url = #url vs
   749     in
   750         case !currently_open_file of
   751             SOME f => raise PGIP ("<loadfile> when a file is open!")
   752           | NONE => use_thy_or_ml_file (File.platform_path url)
   753     end
   754 
   755 fun abortfile vs =
   756     case !currently_open_file of
   757         SOME f => (isarcmd "init_toplevel";
   758                    currently_open_file := NONE)
   759       | NONE => raise PGIP ("<abortfile> when no file is open!")
   760 
   761 fun retractfile (Retractfile vs) =
   762     let
   763         val url = #url vs
   764     in
   765         case !currently_open_file of
   766             SOME f => raise PGIP ("<retractfile> when a file is open!")
   767           | NONE => inform_file_retracted (File.platform_path url)
   768     end
   769 
   770 
   771 (*** System ***)
   772 
   773 fun systemcmd (Systemcmd vs) =
   774   let
   775       val arg = #arg vs
   776   in
   777       isarcmd arg
   778   end
   779 
   780 exception PGIP_QUIT;
   781 fun quitpgip vs = raise PGIP_QUIT
   782 
   783 fun process_input inp = case inp
   784  of Pgip.Askpgip _          => askpgip inp
   785   | Pgip.Askpgml _          => askpgml inp
   786   | Pgip.Askprefs _         => askprefs inp
   787   | Pgip.Askconfig _        => askconfig inp
   788   | Pgip.Getpref _          => getpref inp
   789   | Pgip.Setpref _          => setpref inp
   790   | Pgip.Proverinit _       => proverinit inp
   791   | Pgip.Proverexit _       => proverexit inp
   792   | Pgip.Startquiet _       => startquiet inp
   793   | Pgip.Stopquiet _        => stopquiet inp
   794   | Pgip.Pgmlsymbolson _    => pgmlsymbolson inp
   795   | Pgip.Pgmlsymbolsoff _   => pgmlsymbolsoff inp
   796   | Pgip.Dostep _           => dostep inp
   797   | Pgip.Undostep _         => undostep inp
   798   | Pgip.Redostep _         => redostep inp
   799   | Pgip.Forget _           => error "<forget> not implemented"
   800   | Pgip.Restoregoal _      => error "<restoregoal> not implemented"
   801   | Pgip.Abortgoal _        => abortgoal inp
   802   | Pgip.Askids _           => askids inp
   803   | Pgip.Showid _           => showid inp
   804   | Pgip.Askguise _         => askguise inp
   805   | Pgip.Parsescript _      => parsescript inp
   806   | Pgip.Showproofstate _   => showproofstate inp
   807   | Pgip.Showctxt _         => showctxt inp
   808   | Pgip.Searchtheorems _   => searchtheorems inp
   809   | Pgip.Setlinewidth _     => setlinewidth inp
   810   | Pgip.Viewdoc _          => viewdoc inp
   811   | Pgip.Doitem _           => doitem inp
   812   | Pgip.Undoitem _         => undoitem inp
   813   | Pgip.Redoitem _         => redoitem inp
   814   | Pgip.Aborttheory _      => aborttheory inp
   815   | Pgip.Retracttheory _    => retracttheory inp
   816   | Pgip.Loadfile _         => loadfile inp
   817   | Pgip.Openfile _         => openfile inp
   818   | Pgip.Closefile _        => closefile inp
   819   | Pgip.Abortfile _        => abortfile inp
   820   | Pgip.Retractfile _      => retractfile inp
   821   | Pgip.Changecwd _        => changecwd inp
   822   | Pgip.Systemcmd _        => systemcmd inp
   823   | Pgip.Quitpgip _         => quitpgip inp
   824 
   825 
   826 fun process_pgip_element pgipxml =
   827     case pgipxml of
   828         xml as (XML.Elem elem) =>
   829         (case Pgip.input elem of
   830              NONE => warning ("Unrecognized PGIP command, ignored: \n" ^
   831                               (XML.string_of_tree xml))
   832            | SOME inp => (process_input inp)) (* errors later; packet discarded *)
   833       | XML.Text t => ignored_text_warning t
   834       | XML.Rawtext t => ignored_text_warning t
   835 and ignored_text_warning t =
   836     if size (Symbol.strip_blanks t) > 0 then
   837            warning ("Ignored text in PGIP packet: \n" ^ t)
   838     else ()
   839 
   840 fun process_pgip_tree xml =
   841     (pgip_refid := NONE;
   842      pgip_refseq := NONE;
   843      (case xml of
   844           XML.Elem ("pgip", attrs, pgips) =>
   845           (let
   846                val class = PgipTypes.get_attr "class" attrs
   847                val dest  = PgipTypes.get_attr_opt "destid" attrs
   848                val seq = PgipTypes.read_pgipnat (PgipTypes.get_attr "seq" attrs)
   849                (* Respond to prover broadcasts, or messages for us. Ignore rest *)
   850                val processit =
   851                    case dest of
   852                        NONE =>    class = "pa"
   853                      | SOME id => matching_pgip_id id
   854            in if processit then
   855                   (pgip_refid :=  PgipTypes.get_attr_opt "id" attrs;
   856                    pgip_refseq := SOME seq;
   857                    List.app process_pgip_element pgips;
   858                    (* return true to indicate <ready/> *)
   859                    true)
   860               else
   861                   (* no response to ignored messages. *)
   862                   false
   863            end)
   864         | _ => raise PGIP "Invalid PGIP packet received")
   865      handle PGIP msg =>
   866             (Output.error_msg ((msg ^ "\nPGIP error occured in XML text below:\n") ^
   867                                (XML.string_of_tree xml));
   868              true))
   869 
   870 (* External input *)
   871 
   872 val process_pgip_plain = K () o process_pgip_tree o XML.tree_of_string
   873 
   874 end
   875 
   876 
   877 (* PGIP loop: process PGIP input only *)
   878 
   879 local
   880 
   881 exception XML_PARSE
   882 
   883 fun loop ready src =
   884     let
   885         val _ = if ready then issue_pgip (Ready ()) else ()
   886         val pgipo =
   887           (case try Source.get_single src of
   888             SOME pgipo => pgipo
   889           | NONE => raise XML_PARSE)
   890     in
   891         case pgipo of
   892              NONE  => ()
   893            | SOME (pgip,src') =>
   894              let
   895                  val ready' = (process_pgip_tree pgip)
   896                                 handle e => (handler (e,SOME src'); true)
   897              in
   898                  loop ready' src'
   899              end
   900     end handle e => handler (e,SOME src)  (* error in XML parse or Ready issue *)
   901 
   902 and handler (e,srco) =
   903     case (e,srco) of
   904         (XML_PARSE,SOME src) =>
   905         Output.panic "Invalid XML input, aborting"
   906       | (PGIP_QUIT,_) => ()
   907       | (Interrupt,SOME src) =>
   908         (Output.error_msg "Interrupt during PGIP processing"; loop true src)
   909       | (Toplevel.UNDEF,SOME src) =>
   910         (Output.error_msg "No working context defined"; loop true src)
   911       | (e,SOME src) =>
   912         (Output.error_msg (Toplevel.exn_message e); loop true src)
   913       | (_,NONE) => ()
   914 in
   915   (* TODO: add socket interface *)
   916 
   917   val xmlP = XML.scan_comment_whspc |-- XML.parse_elem >> single
   918 
   919   val tty_src = Source.set_prompt "" (Source.source Symbol.stopper xmlP NONE Source.tty)
   920 
   921   fun pgip_toplevel x = loop true x
   922 end
   923 
   924 
   925 (* additional outer syntax for Isar *)
   926 (* da: TODO: perhaps we can drop this superfluous syntax now??
   927    Seems cleaner to support the operations directly above in the PGIP actions.
   928  *)
   929 
   930 local structure P = OuterParse and K = OuterKeyword in
   931 
   932 val undoP = (*undo without output*)
   933   OuterSyntax.improper_command "ProofGeneral.undo" "(internal)" K.control
   934     (Scan.succeed (Toplevel.no_timing o IsarCmd.undo));
   935 
   936 val redoP = (*redo without output*)
   937   OuterSyntax.improper_command "ProofGeneral.redo" "(internal)" K.control
   938     (Scan.succeed (Toplevel.no_timing o IsarCmd.redo));
   939 
   940 (* ProofGeneral.kill_proof still used above *)
   941 val kill_proofP =
   942   OuterSyntax.improper_command "ProofGeneral.kill_proof" "(internal)" K.control
   943     (Scan.succeed (Toplevel.no_timing o IsarCmd.kill_proof_notify tell_clear_goals));
   944 
   945 (* FIXME: Not quite same as commands used above *)
   946 val inform_file_processedP =
   947   OuterSyntax.improper_command "ProofGeneral.inform_file_processed" "(internal)" K.control
   948     (P.name >> (fn file => Toplevel.no_timing o
   949       Toplevel.init_empty (vacuous_inform_file_processed file) o
   950       Toplevel.kill o
   951       Toplevel.init_empty (proper_inform_file_processed file)));
   952 
   953 val inform_file_retractedP =
   954   OuterSyntax.improper_command "ProofGeneral.inform_file_retracted" "(internal)" K.control
   955     (P.name >> (Toplevel.no_timing oo
   956       (fn file => Toplevel.imperative (fn () => inform_file_retracted file))));
   957 
   958 (* This one can actually be used for Daniel's interface scripting idea: generically!! *)
   959 val process_pgipP =
   960   OuterSyntax.improper_command "ProofGeneral.process_pgip" "(internal)" K.control
   961     (P.text >> (Toplevel.no_timing oo
   962       (fn txt => Toplevel.imperative (fn () => process_pgip_plain txt))));
   963 
   964 fun init_outer_syntax () = OuterSyntax.add_parsers
   965  [undoP, redoP, kill_proofP, inform_file_processedP, inform_file_retractedP, process_pgipP];
   966 
   967 end;
   968 
   969 
   970 (* init *)
   971 
   972 val initialized = ref false;
   973 
   974 fun init_pgip false =
   975       Output.panic "No Proof General interface support for Isabelle/classic mode."
   976   | init_pgip true =
   977       (! initialized orelse
   978         (setmp warning_fn (K ()) init_outer_syntax ();
   979           setup_xsymbols_output ();
   980           setup_pgml_output ();
   981           setup_messages ();
   982           setup_state ();
   983           setup_thy_loader ();
   984           setup_present_hook ();
   985           init_pgip_session_id ();
   986           welcome ();
   987           set initialized);
   988         sync_thy_loader ();
   989        change print_mode (cons proof_generalN o remove (op =) proof_generalN);
   990        change print_mode (append [pgmlN, pgmlatomsN] o subtract (op =) [pgmlN, pgmlatomsN]);
   991        pgip_toplevel tty_src);
   992 
   993 
   994 
   995 (** Out-of-loop PGIP commands (for Emacs hybrid mode) **)
   996 
   997 local
   998     val pgip_output_channel = ref writeln_default
   999 in
  1000 
  1001 (* Set recipient for PGIP results *)
  1002 fun init_pgip_channel writefn =
  1003     (init_pgip_session_id();
  1004      pgip_output_channel := writefn)
  1005 
  1006 (* Process a PGIP command.
  1007    This works for preferences but not generally guaranteed
  1008    because we haven't done full setup here (e.g., no pgml mode)  *)
  1009 fun process_pgip str =
  1010      setmp output_xml_fn (!pgip_output_channel) process_pgip_plain str
  1011 
  1012 end
  1013 
  1014 end;
  1015