Insert pgmltext element into responses in PGIP mode
authoraspinall
Fri Dec 10 22:25:31 2004 +0100 (2004-12-10)
changeset 1540050bbdabd7326
parent 15399 683d83051d6a
child 15401 ba28d103bada
Insert pgmltext element into responses in PGIP mode
src/Pure/proof_general.ML
     1.1 --- a/src/Pure/proof_general.ML	Fri Dec 10 16:57:01 2004 +0100
     1.2 +++ b/src/Pure/proof_general.ML	Fri Dec 10 22:25:31 2004 +0100
     1.3 @@ -214,7 +214,7 @@
     1.4  (*  FIXME: temporarily to support PG 3.4.  *)
     1.5   fun issue_pgip_maybe_decorated bg en resp attrs s = 
     1.6       if pgip_emacs_compatibility() then
     1.7 -      (*  in PGIP mode, but using escape characters as well.  *)
     1.8 +        (*  in PGIP mode, but using escape characters as well.  *)
     1.9  	writeln_default (enclose bg en (assemble_pgip resp attrs s))
    1.10       else 
    1.11  	issue_pgip resp attrs s
    1.12 @@ -235,7 +235,8 @@
    1.13  	 (if (!delay_msgs) then
    1.14  	      delayed_msgs := (resp,attrs,prefix_lines prfx s)::(!delayed_msgs) (* nb: no decs *)
    1.15  	  else 
    1.16 -	      issue_pgip_maybe_decorated bg en resp attrs (prefix_lines prfx s))
    1.17 +	      issue_pgip_maybe_decorated bg en resp attrs 
    1.18 +					 (XML.element "pgmltext" [] [prefix_lines prfx s]))
    1.19       else 
    1.20  	 decorated_output bg en prfx s;
    1.21  
    1.22 @@ -244,7 +245,7 @@
    1.23  
    1.24   fun end_delayed_msgs () = 
    1.25       (delay_msgs := false;
    1.26 -      map (fn (resp,attrs,s) => XML.element resp attrs [s]) (!delayed_msgs))
    1.27 +      map (fn (resp,attrs,s) => XML.element resp attrs [XML.element "pgmltext" [] [s]]) (!delayed_msgs))
    1.28  end
    1.29  
    1.30  local
    1.31 @@ -288,7 +289,7 @@
    1.32  		      (oct_char "364") (oct_char "365") "!!! ")
    1.33  
    1.34  
    1.35 -(* accumulate printed output in a single PGIP response *)
    1.36 +(* accumulate printed output in a single PGIP response (inside <pgmltext>) *)
    1.37  
    1.38  fun with_displaywrap (elt,attrs) dispfn =
    1.39      let 
    1.40 @@ -296,8 +297,8 @@
    1.41  	fun wlgrablines s = (lines:= (s :: (!lines)))
    1.42      in 
    1.43  	(setmp writeln_fn wlgrablines dispfn ();
    1.44 -	 (* FIXME: cat_lines here inefficient, should use stream output *)
    1.45 -         issue_pgip elt attrs (cat_lines (!lines)))
    1.46 +	 (* FIXME: XML.element here inefficient, should use stream output *)
    1.47 +         issue_pgip elt attrs (XML.element "pgmltext" [] (!lines)))
    1.48      end
    1.49  
    1.50  val emacs_notify = decorated_output (oct_char "360") (oct_char "361") "";