src/Pure/ProofGeneral/proof_general_pgip.ML
changeset 21649 40e6fdd26f82
parent 21646 c07b5b0e8492
child 21655 01b2d13153c8
     1.1 --- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Tue Dec 05 01:17:32 2006 +0100
     1.2 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Tue Dec 05 13:56:43 2006 +0100
     1.3 @@ -11,8 +11,9 @@
     1.4  sig
     1.5    val init_pgip: bool -> unit		  (* main PGIP loop with true; fail with false *)
     1.6  
     1.7 -  val process_pgip: string -> unit        (* process a command; only good for preferences *)
     1.8 -  val init_pgip_session_id: unit -> unit  (* call before using process_pgip *)
     1.9 +  (* These two are just to support the semi-PGIP Emacs mode *)
    1.10 +  val init_pgip_channel: (string -> unit) -> unit 
    1.11 +  val process_pgip: string -> unit     
    1.12  end
    1.13  
    1.14  structure ProofGeneralPgip : PROOF_GENERAL_PGIP  =
    1.15 @@ -146,10 +147,11 @@
    1.16  
    1.17  fun matching_pgip_id id = (id = !pgip_id)
    1.18  
    1.19 -val output_xml = writeln_default o XML.string_of_tree;  (* FIXME: use string buffer *)
    1.20 +val output_xml_fn = ref writeln_default  
    1.21 +fun output_xml s = (!output_xml_fn) (XML.string_of_tree s);  (* TODO: string buffer *)
    1.22  
    1.23  fun issue_pgip_rawtext str = 
    1.24 -    output_xml (PgipOutput.output (assemble_pgips [XML.Text str])) (* FIXME: don't escape!! *)
    1.25 +    output_xml (PgipOutput.output (assemble_pgips [XML.Rawtext str]))
    1.26  
    1.27  fun issue_pgips pgipops =
    1.28      output_xml (PgipOutput.output (assemble_pgips (map PgipOutput.output pgipops)));
    1.29 @@ -865,7 +867,9 @@
    1.30  			       (XML.string_of_tree xml));
    1.31  	     true))
    1.32  
    1.33 -val process_pgip = K () o process_pgip_tree o XML.tree_of_string
    1.34 +(* External input *)
    1.35 +
    1.36 +val process_pgip_plain = K () o process_pgip_tree o XML.tree_of_string
    1.37  
    1.38  end
    1.39  
    1.40 @@ -963,7 +967,7 @@
    1.41  val process_pgipP =
    1.42    OuterSyntax.improper_command "ProofGeneral.process_pgip" "(internal)" K.control
    1.43      (P.text >> (Toplevel.no_timing oo
    1.44 -      (fn txt => Toplevel.imperative (fn () => process_pgip txt))));
    1.45 +      (fn txt => Toplevel.imperative (fn () => process_pgip_plain txt))));
    1.46  
    1.47  fun init_outer_syntax () = OuterSyntax.add_parsers
    1.48   [undoP, redoP, kill_proofP, context_thy_onlyP, try_context_thy_onlyP,
    1.49 @@ -999,7 +1003,26 @@
    1.50  fun init_pgip false = Output.panic "PGIP not supported for Isabelle/classic mode."
    1.51    | init_pgip true = (init_setup (); pgip_toplevel tty_src);
    1.52  
    1.53 -fun write_keywords s = ()  (* NB: do nothing *)
    1.54 +
    1.55 +
    1.56 +(** Out-of-loop PGIP commands (for Emacs hybrid mode) **)
    1.57 +
    1.58 +local
    1.59 +    val pgip_output_channel = ref writeln_default
    1.60 +in
    1.61 +
    1.62 +(* Set recipient for PGIP results *)
    1.63 +fun init_pgip_channel writefn =
    1.64 +    (init_pgip_session_id();  
    1.65 +     pgip_output_channel := writefn)				  
    1.66 +
    1.67 +(* Process a PGIP command. 
    1.68 +   This works for preferences but not generally guaranteed 
    1.69 +   because we haven't done full setup here (e.g., no pgml mode)  *)
    1.70 +fun process_pgip str =
    1.71 +     setmp output_xml_fn (!pgip_output_channel) process_pgip_plain str
    1.72 +
    1.73 +end
    1.74  
    1.75  end;
    1.76