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